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.

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

Evaluation

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.

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

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

We use to indicate that the term on the left (the

The Reduction Strategy

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

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

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
.

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