The Book

Implementing Mathematics with The Nuprl Proof Development System

See title page for important information about this reference

next up previous contents
Next: Proof Tactics Up: Index Previous: Proofs   Contents

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 $A\vert B$ using the intro rule for disjoint union we must prove either $A$ or $B$ as a subgoal. Assuming we prove $B$ and assuming $b$ is the term inductively extracted from the proof of $B$ then inr($b$) becomes the term extracted from the proof of $A\vert B$, for inr($\ldots$) is the extraction form for the right intro rule for disjoint unions. Note that if $b$ is in type $B$ then inr($b$) is in $A\vert B$, so the extraction makes sense. Similarly, if we prove something of the form x:$A\vert B$ » $T$ using the elim rule for disjoint union on the hypothesis, then Nuprl generates two subgoals. The first requires us to show that if $A$ is true (i.e., $y:A$ appears in the hypothesis list) then $T$ is true. The second requires us to show that if $B$ is true (i.e., $z:B$ appears in the hypothesis list) then $T$ is true. If $y.ta$ is the term extracted from the the first subgoal ($y.ta$ is a term with $y$ a free variable whose type is $A$; recall that $y$ represents our assumption of the truth of $A$ in the first subgoal) and $z.tb$ is the term extracted from the second subgoal, then decide($x; y.ta; z.tb$) is the term extracted from the proof of x:$A\vert B$ » $T$. Note that if $x$ corresponds to inl($a$) for some $a$ in $A$ then from the computation rules the extracted term is equivalent to $ta[a/y]$; since $y.ta$ proves $T$ under the assumption of $A$ and $A$ holds (since $a$ is in $A$) the extracted term works as desired. Similarly, the term behaves properly if $x$ has value inr($b$) for some $b$ in $B$; 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($\ldots$) form, which is extracted from proofs which use induction via the elim rule on integers. decide($\ldots$) 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 $t$ one evaluates a special Nuprl term, term_of($t$), which constructs the extracted term of $t$ 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 $U_{i}$. 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 term5.1 $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.

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 $id$ = $term$. Entering a binding results in the evaluation of the term and the resulting value being bound to $id$ 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 $\uparrow\!\!\mbox{D}$.

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 $\backslash$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 $name$ eval $place$ 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.

Figure 5.1: The Noncanonical Forms
\begin{figure}\hrule \begin{displaymath}\begin{array}{ll} \mbox{\tt${\bf e}_1$+... ...$;$t_2$)} & \mbox{} \end{array}\end{displaymath} \vspace{2pt}\hrule \end{figure}

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 $k_n$ to denote the canonical int term whose value is $n$. As an example consider the rule for addition:

\begin{displaymath}\mbox{\tt$k_n$+$k_m$} \Rightarrow k_{n+m} \end{displaymath}

We use $\Rightarrow$ 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.
Figure 5.2: The Nonarithmetic Reduction Rules
\begin{figure}\hrule \begin{displaymath}\begin{array}{@{\!}l@{\Rightarrow }ll} ... ...rm if}\; a\neq b & \end{array}\end{displaymath} \vspace{2pt} \hrule \end{figure}
These rules embody the content of the computation rules of the Nuprl logic. One somewhat anomalous term is the term_of( $theorem\mbox{-}name$) 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.2Because 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 ($\backslash$$x$.<($\backslash$$y$.0)($x$),3>)(4) reduces to <($\backslash$$y$.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 ($\backslash$$x.x$($x$))($\backslash$$x.x$($x$)). The only applicable rule is the application rule, but an application of that rule leaves us with the same term.5.4However, 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 $t$, if one can find a closed type $T$ such that the theorem $t$ in $T$ is provable, then the evaluator will reduce $t$ to a canonical term $k$ and furthermore the theorem $t$ = $k$ in $T$ 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($n$) returns the unique integer $i$ such that if $n<0$ then $i=0$ and otherwise $i^2 \leq n<(i+1)^2$. 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 $x$ and applying the rootf function to $x$. 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 $\backslash$x.decide(term_of(Thm1)(x); u.0;v.1). This function gives $0$ if $x$ is a square and $1$ otherwise.

The second theorem has a trivial proof. We simply use the fact that $P$ vel ~$P$ holds for any proposition $P$ and take rootf(x)*rootf(x)=x in int as $P$. However, there is no interesting computational content to this result; we do not obtain from it a procedure to decide whether $x$ 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 $x$ and $y$, 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 $e1$ 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, $e2$, for each instance of its use in $e3$ (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 ($\backslash$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 $\uparrow\!\!\mbox{D}$.


Footnotes

... term5.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 ($\backslash$x.(x+x))($t$), where $t$ is very expensive to evaluate. Under the strategy described above, the value of $t$ 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 $t[t'/x]$ in the rules above, $t'$ will be evaluated at most once and will be evaluated only if there is a free occurrence of $x$ in $t$.
... 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.
next up previous contents
Next: Proof Tactics Up: Index Previous: Proofs   Contents