The reduction rules define how a noncanonical term may be reduced. Figure 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 .
Figure: The Nonarithmetic Reduction Rules
These rules embody the content of the computation rules
of the Nuprl
One somewhat anomalous term is the term_of() term.
This term evaluates to the term extracted from
the given theorem.