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