next up previous contents index
Next: The Reduction Strategy Up: Evaluation Previous: Using the Evaluator

The Reduction Rules

The reduction  rules define how a noncanonical term may be reduced. Figure gif gives a list of the noncanonical forms. The variables denoted by a (possibly subscripted) e indicate so-called argument  places, which must be occupied by canonical terms of the appropriate type before any sense can be made of the term. In the rules which follow we will use to denote the canonical int term whose value is n. As an example consider the rule for addition:

We use to indicate that the term on the left (the redex ) reduces to the term on the right (the contractum ). Note that the form of the contractum depends on the values of the canonical terms appearing in the argument places of the redex. This is a property of all the rules. The rules for the other arithmetic operators are almost identical and can be obtained by replacing both occurrences of + with the appropriate operator. The rest of the rules are listed in figure gif.

Figure: The Nonarithmetic Reduction Rules

         These rules embody the content of the computation rules of the Nuprl logic. One somewhat anomalous term is the term_of() term. This term evaluates to the term extracted from the given theorem.

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