Also see Extracting Witnesses for newer supplementary material.

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

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

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

Also see Extracting Witnesses for newer supplementary material.

Thu Sep 14 08:45:18 EDT 1995