next up previous contents index
Next: Computational Content Up: Evaluation Previous: The Reduction Strategy

Properties of the Evaluator

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.gif 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.

Richard Eaton
Thu Sep 14 08:45:18 EDT 1995