Note that by giving the semantics of the normal evaluation, we are at the
same time defining a relation where
and
are lambda
terms and
evaluates to
. Gunter uses the convention
for
. We are given the inductive definition of
by giving
its informal definition.
It had been pointed out that the right hand side of the latter equation is not necessarily smaller than the left hand side. Thus, what guarantees that ET holds? The answer is that we know that the derivation tree, as the one given in the above example, is finite, and we can prove things by induction on the height of the derivation tree.
Furthermore, we can define a function Val which gives
under the same conditions.
To make Val a total function, we restrict the domain of Val to the set of all lambda terms that converge, that is,
We can easily prove that Val is a total function by induction on the
height of the derivation tree of .