Also see Evaluation for newer supplementary material.
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.