The evaluator makes no use of type information
and thus, because of the application reduction rule, has embedded in it
an interpreter for the untyped lambda calculus.
It is well known that there are terms in the untyped lambda calculus for
which there are no terminating reduction sequences,
or, in Nuprl
terminology, which have no canonical form.
For example, consider the term (
(x))(
(x)).
The only applicable rule is the application rule,
but an application of that rule leaves us with the same term.
However, we are mainly interested in terms which have some type in the system.
The above term has instances of self--application and therefore cannot be typed
in a predicative logic such as Nuprl
.
For terms which can be typed we stand on firmer ground.
It is a metamathematical property of the system that for any closed
term t, if one can find a closed type T such that the theorem
t in T is provable, then the evaluator will reduce
t to a canonical term k and
furthermore the theorem t = k in T is provable.
As each application of a reduction rule corresponds to the use of a
computation rule,
it is not hard to imagine how such a proof would proceed, given the
sequence of reduction rules applied.