next up previous contents index
Next: Using the Evaluator Up: Computation Previous: Term Extraction


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

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