The Nuprl
terms
define a simple functional programming language
whose reduction rules are given by the computation
rules of the Nuprl
theory.
By definition
canonical terms have
outermost forms which
cannot be reduced and, as such, represent the values of the
theory.
On the other hand the outermost forms of
noncanonical terms can be reduced.
The Nuprl
evaluator gives the user the means
to compute the values of
terms.
Given a closed term
t the evaluator attempts to find a canonical term k
such that t and k denote the same value.
The form of the term guides this search process.
Briefly, the evaluator successively chooses a noncanonical subterm in appropriate
form and replaces it with a term closer to canonical form.
It is this process of replacing such a term with another
which we call reducing
the term; the form of the replacement is given by the
reduction rules,
which are in turn derived from the computation rules of the Nuprl
logic.
A given term may contain many noncanonical subterms, so some strategy for choosing the subterm to be reduced is essential. It may not be necessary to reduce all the noncanonical subterms, as a canonical term can contain noncanonical subterms. The strategy chosen is a lazy strategy in that it chooses a minimal number of reductions needed to reduce the term to canonical form. The evaluator cannot always succeed since there are terms which have no canonical form. However, the evaluator will succeed on any term which can be assigned a type.