# The Book

*Implementing Mathematics with The Nuprl Proof Development System*

# Computation

We may view Nuprl as a programming language in which the proofs are programs which are ``translated'' into terms and ``run'' via an evaluator. Proving the truth of a statement in the system is equivalent to showing that the type corresponding to the statement is inhabited, and proving that a type is inhabited in a constructive setting requires that the user specify how an object of the type be built. Implicitly associated with each Nuprl proof, then, is a term whose type is specified by the main assertion being proved. This term exhibits the properties specified by the assertion it corresponds to; if we think of a programming problem as being a list of specifications, then a proof that the specifications can be met defines an algorithm which solves the problem, and the associated term becomes the computational realization of the algorithm. The system also supplies a means for evaluating these terms. Given a term the evaluator attempts to find a value corresponding to the term. For more on the correspondence between proofs and programs see [Bates & Constable 85] and [Sasaki 85].

In this chapter we consider Nuprl as a programming tool. We describe generally the way in which the system extracts terms from proofs and computes the values of terms, and we conclude the chapter with an example which demonstrates the workings of the extractor and the evaluator.

# Term Extraction

A proof of a theorem in the Nuprl system implicitly provides directions for constructing a witness for the truth of the theorem. These directions arise from the fact that every Nuprl rule has associated with it an*extraction form*, a term template which yields a term when various parameters to the form are instantiated with terms. These forms may give rise either to canonical or noncanonical terms depending on the nature of the rule corresponding to the form. Figure 5.1 lists the noncanonical forms, while the canonical forms and the extraction form corresponding to each proof rule are listed in chapter 8.

A proof gives rise to a term in that each rule used in the proof
produces an extract form whose parameters are instantiated
with the terms
inductively extracted from the subgoals generated by the rule invocation.
For example, if we wish to prove a theorem of the form using the
`intro` rule for disjoint union we must prove either or as
a subgoal.
Assuming we prove and assuming is the term inductively extracted
from the proof of then `inr()` becomes the term extracted
from the proof of , for `inr()` is the extraction form
for the right `intro` rule for disjoint unions.
Note that if is in type then `inr()` is in , so the
extraction makes sense.
Similarly, if we prove something of the form
`x: » `
using the `elim` rule for disjoint union on the hypothesis,
then Nuprl generates two subgoals.
The first requires us to show that if is true (i.e., appears in
the hypothesis list)
then is true.
The second requires us to show that if is true (i.e., appears in
the hypothesis list)
then is true.
If is the term extracted from the the first subgoal
( is a term with a free variable whose type is ;
recall that represents our assumption of the truth of in the
first subgoal)
and is the term extracted from the second subgoal,
then
`decide()`
is the term extracted from the proof of
`x: » `.
Note that if corresponds to `inl()` for some in
then from the computation rules the extracted term is equivalent to
; since proves under the assumption of
and holds (since is in ) the extracted term works as
desired.
Similarly, the term behaves properly if has value `inr()`
for some in ; thus this extraction form is justified.

One should note that certain standard
programming constructs have
analogs as Nuprl terms.
In particular, recursive definition corresponds to the `ind()`
form, which is extracted from proofs which use induction via the `elim`
rule on integers.
`decide()` represents a kind of if-then-else
construct,
while the functional terms extracted from proofs using functional `intro`
correspond to function constructs in a standard programming language.

To display the term corresponding to a theorem one evaluates a special
Nuprl term, `term_of()`, which
constructs the extracted term of in a
recursive fashion.
Briefly, the extraction form of the top refinement rule becomes the outermost
form of the term being constructed.
The parameters of the form then become the terms constructed from the subgoals
generated by the refinement rule.

Many Nuprl rules require the user to prove that a type is
well-formed,
i.e., that the type resides in some universe .
These subgoals, when proved, yield the extraction term
`axiom`
and are usually ignored by `term_of` as it builds the term for
a theorem.

We should note here that one can manipulate canonical and noncanonical terms explicitly in the system. For example, the following definition defines an absolute value function.

abs(<x:int>) == less (<x>; 0; -<x>; <x>)We may now use

`abs`as a definition in the statement and proof of theorems. This capability adds a great deal of flexibility to the system.

#

Evaluation

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

^{5.1}the evaluator attempts to find a canonical term such that and 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.

## Using the Evaluator

The EVAL mechanism may be run interactively by typing the command`eval`in the command window. This command replaces the

`P>`prompt with the

`E>`prompt. Two kinds of expressions may be entered after this prompt: Nuprl terms and bindings. Every expression must be terminated by

`;;`and may extend for any number of lines. Entering a term results in that term being evaluated and its value being displayed. A binding has the form

`let =`. Entering a binding results in the evaluation of the term and the resulting value being bound to in the EVAL environment and this value being displayed. The EVAL environment persists from one invocation of

`eval`to the next. An EVAL session is terminated by .

For example, suppose we have a theorem named `bruce` with main goal

>> x:int -> y:int # (x=y in int)proved so that the extracted term is

`x.<x,axiom>`. We could have the following session with the evaluator.

... ... |P>eval | |E>let p1 = \x.spread(x;u,v.u);; | |\x.spread(x;u,v.u) | |E>let t = term_of(bruce);; | |\x.<x,axiom> | |E>t(17);; | |<17,axiom> | |E>p1(t(17));; | |17 | ... ...

The Nuprl command `create eval ` creates a library
object that can contain any number of bindings (all terminated by
`;;`).
The library objects created in this way are edited using ted and so
may contain def refs.
Checking an EVAL object augments the EVAL environment by
evaluating the bindings it contains.
All EVAL objects in a library are evaluated when the library is loaded.

## The Reduction Rules

The reduction rules define how a noncanonical term may be reduced. Figure 5.1 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 . 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 5.2. 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.

##

The Reduction Strategy

As noted in the introduction to this chapter
the evaluation process consists of the repeated selection of a redex
and the application of the appropriate reduction rule to it
until the term is in canonical form.
To make this process definite we need to specify which redex is chosen
if there is more than one possibility.
The goal of this choice should be that as few reductions as necessary are done
to bring the term into canonical form.
Now, whether or not a term is in canonical form depends only on the outer
structure of the term.
For example, the term `inl(spread(<1,2>;u,v.u))`is considered to be in canonical form even though it contains a redex. Thus, to minimize the number of reductions needed the choice is made to reduce the outermost redex.

^{5.2}Because of the position of the argument places in noncanonical forms, this amounts to choosing the leftmost redex when the term is written out in linear fashion. Under this strategy the term

`(.<(.0)(),3>)(4)`reduces to

`<(.0)(4),3>`after a single application of the application reduction rule, whereas under an innermost or rightmost strategy it would reduce to

`<0,3>`. This illustrates the lazy nature of this strategy.

^{5.3}

## Properties of the Evaluator

The evaluator makes no use of type information and thus, because of the application reduction rule, has embedded in it an interpreter for the untyped lambda calculus. It is well known that there are terms in the untyped lambda calculus for which there are no terminating reduction sequences, or, in Nuprl terminology, which have no canonical form. For example, consider the term`(())(())`. The only applicable rule is the application rule, but an application of that rule leaves us with the same term.

^{5.4}However, we are mainly interested in terms which have some type in the system. The above term has instances of self-application and therefore cannot be typed in a predicative logic such as Nuprl. For terms which can be typed we stand on firmer ground. It is a metamathematical property of the system that for any closed term , if one can find a closed type such that the theorem

`in`is provable, then the evaluator will reduce to a canonical term and furthermore the theorem

`= in`is provable. As each application of a reduction rule corresponds to the use of a computation rule, it is not hard to imagine how such a proof would proceed, given the sequence of reduction rules applied.

# Computational Content

Not all theorems are interesting computationally, of course. Recall the`rootf`function defined in the preceding chapter;

`rootf()`returns the unique integer such that if then and otherwise . Now consider the following two theorems, where

`square(x)`is defined as

`rootf(x)*rootf(x)=x in int`.

Thm1 >>all x:int. square(x) | ~ square(x). Thm2 >>all x:int. square(x) vel ~ square(x).The first theorem can be proved by introducing and applying the

`rootf`function to . We can prove that either

`rootf(x)*rootf(x)=x in int`or not by using the arithmetic rule,

`arith`; the proof yields a decision procedure identifying which case holds. From a proof of

`Thm1`, then, we can extract a function which will decide whether an integer is a square, namely

`x.decide(term_of(Thm1)(x); u.0;v.1)`. This function gives if is a square and otherwise.

The second theorem has a trivial proof. We simply use the fact that
` vel ~` holds for any proposition and take `rootf(x)*rootf(x)=x in int`
as . However, there is no interesting computational content to this
result; we do not obtain from it a procedure to decide whether is a
square. (The interested reader should prove this theorem and display
its computational content.)

# An Example

The following is a small proof in Nuprl with the extraction clauses
shown explicitly. The system does not produce the comments `(* *)`;
we include them for illustrative purposes only.
In the interest of condensing the presentation we also elide hypothesis lists wherever possible.

,------------------------------------------------------------, |EDIT THM thm | |------------------------------------------------------------| |* top (* term_of(thm) extracted *) | |>> all x,y:int.(x=y in int)|some z:int.~(z=0 in int)#(x+z=y | | in int | | | |BY quantifier (* ext \x.\y.e1 (quantifier tactic does | | intro twice) *) | |1* 1. x:(int) | | 2. y:(int) | | >> ((x=y in int)|some z:int.~(z=0 in int)#(x+z=y in int))| | (* ext e1 *) | |2* >> (int) in U1 | | | |3* >> (int) in U1 | '------------------------------------------------------------' |

The rule `quantifier` is a *tactic*, a
user-defined rule of inference,
which successively applies the `intro` rule to each
universal quantifier;
in this case it performs two applications. This tactic was written by
a user of the system and must be loaded as an ML object to be used;
in general it would not be available.
See the following chapter for more on tactics.
The extracted term is a function
which, given any values for and , will give a proof of the body; this
corresponds to the intuitive meaning of `all` and justifies its definition
as a dependent function. Note that is the term extracted
from the first subgoal; the next window shows the proof of this subgoal.

,------------------------------------------------------------, |EDIT THM thm | |------------------------------------------------------------| |* top 1 (* e1 extracted *) | |1...2. | |>> ((x=y in int)|some z:int.~(z=0 in int)#(x+z=y in int)) | | | |BY seq (x=y in int)|~(x=y in int) new E (* ext \E.e3(e2) *) | | | |1* 1...2. | | >> (x=y in int)|~(x=y in int) (* ext e2 *) | | | |2* 1...2. | | 3. E:(x=y in int)|~(x=y in int) | | >> ((x=y in int)|some z:int.~(z=0 in int)#(x+z=y in int))| | (* ext e3 *) | '------------------------------------------------------------' |

The `seq` rule extracts a function which in effect substitutes
the proof of the `seq` term, , for each instance of its
use in (under the name `E`).

,------------------------------------------------------------, |EDIT THM thm | |------------------------------------------------------------| |* top 1 1 (* e2 extracted *) | |1...2. | |>> (x=y in int)|~(x=y in int) | | | |BY arith (* ext int_eq(x;y;inl(axiom);inr(axiom)) *) | | | |1* 1...2. | | >> x in int | | | |2* 1...2. | | >> y in int | | | |3* 1...2. | | >> x in int | | | |4* 1...2. | | >> y in int | '------------------------------------------------------------' |

The `arith` decision procedure produces the
`int_eq` term, a
decision
procedure for equality on the integers.

,------------------------------------------------------------, |EDIT THM thm | |------------------------------------------------------------| |* top 1 2 (* e3 extracted *) | |1...2. | |3. E:(x=y in int)|~(x=y in int) | |>> ((x=y in int)|some z:int.~(z=0 in int)#(x+z=y in int)) | | | |BY elim 3 (* ext decide(E;l.e4;r.e5) *) | | | |1* 1...3. | | 4. l:(x=y in int) | | >> ((x=y in int)|some z:int.~(z=0 in int)#(x+z=y in int))| | (* ext e4 *) | |2* 1...3. | | 4. r:~(x=y in int) | | >> ((x=y in int)|some z:int.~(z=0 in int)#(x+z=y in int))| | (* ext e5 *) | '------------------------------------------------------------' |

The `elim` rule for disjoint unions produces a `decide`
term.
In the next frame the term `l` is
extracted from the first subgoal because our goal is exactly `l`
(the actual proof of this subgoal is not shown but is carried out using
the rule `hyp 4`).

,------------------------------------------------------------, |EDIT THM thm | |------------------------------------------------------------| |* top 1 2 1 (* e4 extracted *) | |1...3. | |4. l:(x=y in int) | |>> ((x=y in int)|some z:int.~(z=0 in int)#(x+z=y in int)) | | | |BY intro left (* ext inl(e6) *) | | | |1* 1...4. | | >> (x=y in int) (* ext e6==l (follows by hyp 4) *) | | | |2* 1...4. | | >> some z:int.~(z=0 in int)#(x+z=y in int) in U1 | '------------------------------------------------------------' |

In the next frame `r` is extracted for the same reason as `l`
is above.

,------------------------------------------------------------, |EDIT THM thm | |------------------------------------------------------------| |* top 1 2 2 (* e5 extracted *) | |1...3. | |4. r:~(x=y in int) | |>> ((x=y in int)|some z:int.~(z=0 in int)#(x+z=y in int)) | | | |BY intro right (* ext inr(e7) *) | | | |1* 1...4. | | >> some z:int.~(z=0 in int)#(x+z=y in int) (ext e7 *) | | | |2* 1...4. | | >> ((x=y in int)) in U1 | '------------------------------------------------------------' |

In the next frame, since `some` is defined to be a dependent product
we extract a pair consisting of an element of the integers, `y-x`, and
a proof, *e8*, that the proposition is true for this element.
This corresponds to the desired meaning of `some`.

,------------------------------------------------------------, |EDIT THM thm | |------------------------------------------------------------| |* top 1 2 2 1 (* e7 extracted *) | |1...3. | |4. r:~(x=y in int) | |>> some z:int.~(z=0 in int)#(x+z=y in int) | | | |BY intro y-x (* ext <y-x,e8> *) | | | |1* 1...4. | | >> y-x in (int) | | | |2* 1...4. | | >> ((y-x=0 in int)->void)#(x+y-x=y in int) (* ext e8 *)| | | |3* 1...4. | | 5. z:(int) | | >> (~(z=0 in int)#(x+z=y in int)) in U1 | '------------------------------------------------------------' |

The product `intro` produces a pair
consisting of proofs of the two
subgoals. Although the proof is not shown here, subgoal 2 can be seen
to follow trivially by `arith`.

,------------------------------------------------------------, |EDIT THM thm | |------------------------------------------------------------| |* top 1 2 2 1 2 (* e8 extracted *) | |1...3. | |4. r:~(x=y in int) | |>> ((y-x=0 in int)->void)#(x+y-x=y in int) (* ext <e9,e10>*)| | | |BY intro | | | |1* 1...4. | | >> (y-x=0 in int)->void (* ext e9 *) | | | |2* 1...4. | | >> x+y-x=y in int (* ext e10==axiom (follows by arith)*)| '------------------------------------------------------------' |

In the next frame we see that
hypotheses 4 and 5 contradict each other. The system somewhat
arbitrarily extracts `(v0.any(v0))(r(axiom))`
from this (we could extract anything
we desired from a contradiction).

,------------------------------------------------------------, |EDIT THM thm | |------------------------------------------------------------| |* top 1 2 2 1 2 1 (* e9 extracted *) | |1...3. | |4. r:~(x=y in int) | |>> (y-x=0 in int)->void | | | |BY intro new f (* ext \f.e11 *) | | | |1* 1...4. | | 5. f:y-x=0 in int | | >> void (* ext e11==(\v0.any(v0))(r(axiom)) | | (from a contradiction)*)| | | |2* 1...4. | | >> (y-x=0 in int) in U1 | '------------------------------------------------------------' |

We could now have the following session with the evaluator. What follows has additional *white space* (spaces and carriage returns) to improve readability.

,------------------------------------------------------------, |P>eval | |E>term_of(thm);; | |\x.\y.(\E.decide(E;l.inl(l); | | r.inr(<y-x,<\f.(\v0.any(v0))(r(axiom)),axiom>>))) | | (int_eq(x;y ;inl(axiom);inr(axiom))) | |E>term_of(thm)(7)(7);; | |inl(axiom) | |E>term_of(thm)(7)(10);; | |inr(<10-7,<\f.(\v0.any(v0))(axiom(axiom)),axiom>>) | |E>let p1 = \x.spread(x;u,v.u);; | |\x.spread(x;u,v.u) | |E>let d = \y.decide(y;u.p1(u);u.p1(u));; | |\y.decide(y;u.p1(u);u.p1(u)) | |E>d(term_of(thm)(7)(10));; | |3 | '------------------------------------------------------------' |

To terminate an `eval` session type
.

#### Footnotes

- ... term
^{5.1} - A
*closed*term is a term containing no free variables. - ... redex.
^{5.2} - This corresponds to head reductions, normal-order evaluation or call-by-name parameter passing semantics.
- ... strategy.
^{5.3} - One might
complain that for certain terms this strategy would cause more work
than necessary to be performed.
For instance, consider the term
`(x.(x+x))()`, where is very expensive to evaluate. Under the strategy described above, the value of would be computed twice. As the language we are dealing with is*functional*we know that this is unnecessary, and under the actual implementation of the evaluator it would in fact be evaluated only once. In general, for any substitution in the rules above, will be evaluated at most once and will be evaluated only if there is a free occurrence of in . - ... term.
^{5.4} - The evaluator will try to reduce this term and in doing so will run until something intervenes, such as exhausting available memory.