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|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|B, for inr() 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|B, so the extraction makes sense. Similarly, if we prove something of the form x:A|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., appears in the hypothesis list) then T is true. The second requires us to show that if B is true (i.e., appears in the hypothesis list) then T is true. If is the term extracted from the the first subgoal ( 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 is the term extracted from the second subgoal, then decide() is the term extracted from the proof of x:A|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 ; since 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() 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 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 . 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>)