next up previous contents index
Next: Term Extraction Up: No Title Previous: Example from Elementary


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.

Richard Eaton
Thu Sep 14 08:45:18 EDT 1995