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

Thu Sep 14 08:45:18 EDT 1995