Skip to main content
PRL Project

The Book

Implementing Mathematics with The Nuprl Proof Development System

See title page for important information about this reference

next up previous contents
Next: Introduction to Type Theory Up: Index Previous: Contents   Contents


Overview

Brief Description of Nuprl

Problem solving is a significant part of science and mathematics and is the most intellectually significant part of programming. Solving a problem involves understanding the problem, analyzing it, exploring possible solutions, writing notes about intermediate results, reading about relevant methods, checking results, and eventually assembling a solution. Nuprl is a computer system which provides assistance with this activity. It supports the interactive creation of proofs, formulas, and terms in a formal theory of mathematics; with it one can express concepts associated with definitions, theorems, theories, books and libraries. Moreover, the theory is sensitive to the computational meaning of terms, assertions and proofs, and the system can carry out the actions used to define that computational meaning. Thus Nuprl includes a programming language, but in a broader sense it is a system for implementing mathematics.

Highlights of Nuprl

One of the salient features of Nuprl is that the logic and the system take account of the computational meaning of assertions and proofs. For instance, given a constructive existence proof the system can use the computational information in the proof to build a representation of the object which demonstrates the truth of the assertion. Such proofs can thus be used to provide data for further computation or display. Moreover, a proof that for any object $x$ of type $A$ we can build an object $y$ of type $B$ satisfying relation $R(x,y)$ implicitly defines a computable function $f$ from $A$ to $B$. The system can build $f$ from the proof, and it can evaluate $f$ on inputs of type $A$. For example, given any mapping $f$ of a nonempty set $A$ onto a finite set $B$ of smaller but nonzero cardinality, one can say that there will be two points of $A$ mapped to the same point of $B$. From a proof of this statement the system can extract a function which given specific $A$, $B$ and $f$ produces two points of $A$ mapped to the same point of $B$. This function expresses the computational content of the theorem and can be evaluated.

As a computer system Nuprl supports an interactive environment for text editing, proof generation and function evaluation. The interaction is oriented around a computer terminal with a screen and a mouse, for our intention is to provide a medium for doing mathematics different from that provided by paper and blackboard. Eventually such a medium may support a variety of input devices and may provide communication with other users and systems; the essential point, however, is that this new medium is active, whereas paper, for example, is not. This enables the interactive style of proof checking that characterizes Nuprl; in this system it is impossible to develop an incorrect proof.

Nuprl also possesses some of the characteristics of an intelligent computer system in that it provides its users with a facility for writing proof-generating programs in a metalanguage, ML. The implementation of the logic codes into Nuprl certain primitive mathematical knowledge in the form of rules for generating proofs and in the form of certain defined types in ML. As people use Nuprl they create libraries of mathematical facts, definitions and theorems; they can also create libraries of ML programs which use these results and other ML programs to generate proofs of theorems. In a very real sense, as Nuprl is used its capacity for providing help in proving theorems increases. By virtue of this property, Nuprl possesses aspects of an intelligent system.

The system design exhibits several key characteristics. The style of the logic is based on the stepwise refinement paradigm for problem solving in that the system encourages the user to work backward from goals to subgoals until one reaches what is known. Indeed, the system derives its name, Proof Refinement Logic,1.1 from this method of presentation. The logic has a constructive semantics in that the meaning of propositions is given by rules of use and in terms of computation. We discuss these features in more detail later.

In a larger sense the Nuprl system serves as a tool for experimenting with ways of applying computer power to solving problems and to generating exact explanations of solutions, especially in the realm of computational mathematics. Because the difficult part of computer programming is precisely in problem solving and in explaining algorithmic solutions, we think that a system of this kind will eventually have a lasting impact on our ability to produce reliable and understandable programs.

Motivations

In high school algebra solutions to most problems can be checked by simple computation; for instance, one can easily verify by substitution and reduction that 17 is a root of $x^3-16x^2-19x+34$. Those who are pleased with the certainty of such solutions may also hope to find ways of checking solutions to more abstract problems (such as showing that $\sqrt{2}^{\sqrt{2}}$ is irrational) computationally. The idea that computers can check proofs is a step toward achieving this ambition [McCarthy 62,deBruijn 80], and there are several interesting implementations of this idea [Suppes 81,Weyhrauch 80,Constable, Johnson, & Eichenlaub 82,Gordon, Milner, & Wadsworth 79]. The computer system described here represents another approach to this problem.

Someone who has struggled for hours or perhaps days to untangle the details of a complex mathematical argument will understand the dream of building a computer system which helps fill in the details and keeps track of the proof obligations that must be met at the critical points of an argument. There are computer systems which do this, and it is possible in principle to solve problems in a system of this kind which are beyond the patience and capability of an unaided human being, as K. Mulmuley has already demonstrated in LCF [Mulmuley 84]. Nuprl uses some of the mechanisms of LCF which make this possible, namely the metalanguage ML in which the user writes programs to provide help with the details.

People who have spent hours or days getting a mathematical construction such as Gauss' construction of a regular 17-gon exactly right will know the desire to watch this mathematical construction ``come to life.'' Nuprl was built to meet such aspirations. Every construction described in Nuprl's mathematics can, in principle, be executed mechanically. In particular, Nuprl can execute functions and thus serve as a programming language in the usual sense.

Anyone who has tried to write a mathematical paper or system consisting of several interacting theorems and constructions will appreciate having a uniform notation for discourse and a facility for creating an encyclopedia of results in this notation. The Bourbaki effort [Bourbaki 68] manifests such aspirations on a grand scale, and Nuprl is a step toward realizing this goal. It supports a particular mathematical theory, constructive type theory, whose primitive concepts can serve as building blocks for nearly any mathematical concept. Thus Nuprl provides a uniform language for expressing mathematics. This is a characteristic that distinguishes Nuprl from most other proof-checking or theorem-generating systems.

Anyone who has written a heuristic procedure such as one for playing games or finding proofs and who has seen it do more than was expected will understand the dream of using a computer system which can provide unexpected help in proving theorems. It is easy to extrapolate to dreams of machines offering critical help in solving real problems. Substantial effort has been put into ``theorem-proving'' programs which attempt to provide just such help, usually in a specific domain of mathematics. While Nuprl is not a theorem-proving program in the usual sense, it is a tool for exploring this kind of heuristic programming. Users may express a variety of procedures which search for proofs or attempt to fill in details of a proof. The system has already provided interesting experiences of unexpected behavior by finishing proofs ``on its own.''

People who have experienced the new electronic medium created by computers may imagine how mathematics will be conducted in it. We see electronic mail and electronic text editing. We see systems like the Cornell Program Synthesizer [Teitelbaum & Reps 81] that help users specify objects such as programs directly in terms of their structure, leaving the system to generate the textual description. We can imagine these ideas being applied to the creation of mathematical objects such as functions and proofs and their textual descriptions. In this case, because mathematical structure can be extremely complex, one can imagine the computer providing considerable assistance in producing objects as well as help in displaying the text and giving the reader access to the underlying structure in various ways. Nuprl offers such capabilities, the most striking among which are the help the system provides in writing formal text (see chapter 3) and in reading and generating highly structured objects such as proofs and function terms. As with all aspects of Nuprl there is much to be done to achieve the goals that motivated the design, but in every case the system as it stands makes a contribution. We hope it will show the way to building better systems of this kind.


The Nuprl Logical Language

An algorithm to add two integers can be expressed in Nuprl as $\backslash x.\backslash y.x+y$. In general, if $b(x)$ is an expression such as $x*2$ or $\backslash y.x+y$ in the variable $x$, then $\backslash x.b(x)$ is the function of one argument which on input $a$ computes the value $b(a)$, where $b(a)$ stands for the expression $b$ with each occurrence of $x$ replaced by $a$. Application of the function is expressed by $(\backslash x.b(x))(a) = b(a)$; for example, $(\backslash x.x*2)(2) = 2*2 = 4$. We speak of $\backslash x.b(x)$ as the abstraction of $b(x)$ with respect to $x$. This notation is essentially the same as Church's lambda notation, which is systematized in the lambda calculus [Church 51]. The form $\backslash x.b(x)$ is a visual approximation to $\lambda x.b(x)$ of the lambda calculus. Our notation is also very close to that used in ML [Gordon, Milner, & Wadsworth 79] except that type information about the variable can be included in the ML form. This marks a significant departure from the Algol-like languages as well, for in these languages the type information is given with the parameters of a function. For example, one would write ${\bf function}(x:{\bf int}){\bf int}$ in the heading of an Algol function definition to show that the function maps integers to integers.

In Nuprl, as in the work of H.B. Curry [Curry, Feys, & Craig 58,Curry, Hindley, & Seldin 72], a type discipline is imposed on algorithms to describe their properties. Thus, when we say that $\backslash x.x+1$ is a function from integers to integers, we are saying that when an integer $n$ is supplied as an argument to this algorithm, then $n+1$ will denote a specific integer value. In general, meaning is given to a function term $\backslash x.b(x)$ by saying that it has type $A\rightarrow B$ for some type $A$ called the domain and some type $B$ called the range. The type $A\rightarrow B$ denotes functions which on input $a$ from $A$ produce a value in $B$. The fact that the functions always return a value is sometimes emphasized by calling them total functions.

The type structure hierarchy of Nuprl resembles that of Principia Mathematica, the ancestor of all type theories. The hierarchy manifests itself in an unbounded cumulative hierarchy of universes, $U_{1}$, $U_{2}$, ..., where by cumulative hierarchy we mean that $U_{i}$ is in $U_{i+1}$ and that every element of $U_{i}$ is also an element of $U_{i+1}$. Universes are themselves types,1.2and every type occurs in a universe. In fact, $A$ is a type if and only if it belongs to a universe. Conversely all the elements of a universe are types.

It is pedagogically helpful to think of the other Nuprl types in five stages of decreasing familiarity. The most familiar types and type constructors are similar to those found in typed programming languages such as Algol 68, ML or Pascal. These include the atomic types int, atom and void along with the three basic constructors: cartesian product, disjoint union and function space.1.3If $A$ and $B$ are types, then so is their cartesian product, $A$#$B$, their disjoint union, $A$|$B$, and the functions from $A$ to $B$, $A$->$B$.

The second stage of understanding includes the dependent function and dependent product constructors, which are written as $x$:$A$->$B$ and $x$:$A$#$B$, respectively, in Nuprl. The dependent function space is used in AUTOMATH and the dependent product was suggested by logicians studying the correspondence between propositions and types; see Scott [Scott 70] and Howard [Howard 80]. These types will be explained in detail later, but the intuitive idea is simple. In a dependent function space represented by $x$:$A$->$B$, the range type, $B$, is indexed by the domain type, $A$. This is exactly like the indexed product of a family of sets in set theory, which is usually written as $(\Pi x\in A)B(x)$ (see [Bourbaki 68]). In the dependent product represented by $x$:$A$#$B$, the type of the second member of a pair can depend on the value of the first. This is exactly the indexed disjoint sum of set theory, which is usually written as $(\Sigma x\in A)B(x)$ (see [Bourbaki 68]).

The third stage of understanding includes the quotient and set types introduced in [Constable 85]. The set type is written $\{$$x$:$A$|$B$$\}$ and allows Nuprl to express the notions of constructive set and of partial function. The quotient type allows Nuprl to capture the idea of equivalence class used extensively in algebra to build new objects.

The fourth stage includes propositions considered as types. The atomic types of this form are written $a$ = $b$ in $A$ and express the proposition that $a$ is equal to $b$ in type $A$. A special case of this is $a$ = $a$ in $A$, written also as $a$ in $A$. These types embody the propositions-as-types principle discovered by H. B. Curry [Curry, Feys, & Craig 58], W. Howard [Howard 80], N. G. deBruijn [deBruijn 80] and H. Lauchli [Lauchli 70] and used in AUTOMATH [deBruijn 80,Jutting 79]. This principle is also central to P. Martin-Löf's Intuitionistic type theories [Martin-Löf 82,Martin-Löf 73].

The fifth stage includes the recursive types and the type of partial functions as presented by Constable and N. P. Mendler [Constable & Mendler 85]. These are discussed in chapter 12, but they have not been completely implemented so we do not use them in examples taken directly from the computer screen. These are the only concepts in this book not taken directly from the 1984 version of the system.

The logical language is interesting on its own. It is built around tested logical notions from H. Curry, A. Church, N. deBruijn, B. Russell, D. Scott, E. Bishop, P. Martin-Löf and ourselves among others and as such forms part of a well-known and thoroughly studied tradition in logic and philosophy. However, this tradition has not until now entered the realm of usable formal systems and automated reasoning in the same way as the first-order predicate calculus. Thus the design and construction of this logic is a major part of Nuprl, and becoming familiar with it will be a major step for our readers. We recommend in addition to this account the forthcoming book of B. Nordström, K. Petersson and J. Smith, the paper ``Constructive Validity'' [Scott 70], the paper ``Constructive Mathematics and Computer Programming'' [Martin-Löf 82] and ``Constructive Mathematics as a Programming Logic'' [Constable 85]. An extensive guide to the literature appears in the references. We hope that this account will be sufficient to allow readers to use the system, which in the end may be its own best tutor.


Components of the Nuprl System

General

The Nuprl system has six major components: a window manager, a text editor, a proof editor, a library module, a command module and a function evaluator. Interaction with Nuprl takes place in the context of three languages--the command language, which is extremely simple, the object language, which is the mathematical language of the system, and the metalanguage, which is a programming language with data types referring to the object language. The command language is used to initiate editing, use the library and initiate executions in the object and metalanguages, to name a few of its functions. The object language is a constructive theory of types. The metalanguage is the programming language ML from the Edinburgh LCF system modified to suit Nuprl.

The window manager provides the interface for the interactive creation of certain kinds of linguistic objects called definitions, theorems, proofs and libraries on a terminal screen. Windows offer views of objects; using these views the user can navigate through the object, stopping to modify it, to copy parts of it to other windows or to insert parts into it from other windows, etc. Three special windows provide for editing theorems, viewing the library and entering commands.


Definitions

The definition facility allows one to develop new notations in the form of templates which can be invoked when entering text. This feature provides a flexible way to introduce new notation. For instance, we might have defined a function, abs(x), which computes the absolute value of a number, but we might like to display it in the text as |x|. This can be accomplished by defining a template. The format is |<x:number>| == abs(<x>), where the left-hand side of == is the template and the right-hand side is the value (the angle brackets are used to designate the parameter).

Proof Editing

The proof-editing facility supports top-down construction of proofs. Goals are written as sequents; they have the form $x_1$:$H_1$,$\ldots$,$x_n$:$H_n$ » $G$, where the $H_i$ are the hypotheses and $G$ is the conclusion. To prove a goal, the user selects a rule for making progress toward achieving this goal, and the system responds with a list of subgoals. For example, if the goal is prove $A$&$B$ and the rule selected is ``and introduction,'' the system generates the following subgoals.
  1. prove $A$
  2. prove $B$

Proofs can be thought of as finite trees, where each node corresponds to the application of a logical rule. A proof can be read to the desired level of detail by descending into subtrees whose structure is interesting and passing over others.


Evaluation

The evaluation mechanism allows us to regard Nuprl as a functional programming language. For example, the multiplication function in Nuprl notation is $\backslash$x.$\backslash$y.(x*y), and one can evaluate ($\backslash$x.$\backslash$y.(x*y))(2)(3) to obtain the value 6. Of course, one can define much more complex data such as infinite precision real numbers and functions on them such as multiplication (see section 11.6). In this case we might also evaluate the form ($\backslash$x.$\backslash$y.mult(x,y))(e)(pi)(50), which might print the first 50 digits of the infinite precision multiplication of the transcendental numbers $e$ and $\pi$.

The evaluation mechanism can also use a special form, term_of($t$), where $t$ is a theorem. The term_of operation extracts the constructive meaning of a theorem. Thus if we have proved a theorem named $t$ of the form for all $x$ of type $A$ there is a $y$ of type $B$ such that $R(x,y)$ then term_of($t$) extracts a function mapping any $a$ in $A$ to a pair consisting of an element from $B$, say $b$, and a proof, say $p$, of $R(a,b)$. By selecting the first element of this pair we can build a function $f$ from $A$ to $B$ such that $R(x,f(x))$ for all $x$ in $A$. The system also provides a mechanism for naming and storing executable terms in the library.

Programming Modes

The term_of operation enables two new modes of programming in Nuprl in addition to the conventional mode of writing function terms. To program in the first new mode one writes proof outlines, $p$, which contain the computational information necessary for term_of($p$) to be executable. The second mode is a refinement of the first in which complete proofs, $cp$, are supplied as arguments to term_of. In this case one knows that the program meets its specification, so this mode might be called ``verified programming''.

Physical Characteristics

The system described here is written in about 60,000 lines of Lisp. It runs in Zetalisp on Symbolics Lisp Machines and in Franz Lisp under Unix 4.2BSD. There are also several thousand lines of ML programs included in the basic system. We have been using it since June 1984 principally to test the ideas behind its design but also to begin accumulating a small library of formal algorithmic mathematics. It can be used as a programming environment, and to a limited extent it has seen such service. But unlike its simpler predecessor, Lambda-prl [Nuprl Staff 83], it has not been provided with a compiler nor an optimizer, so it can be very inefficient. We hope that in due course there will be facilities to make it run acceptably fast. The system is in fact growing, but the major thrust over the next year is to substantially enhance its deductive power and its user-generated knowledge in the form of libraries of definitions, theorems and proof methods (see section 1.9 for some of our detailed plans).

The ``Feel'' of the System

Nuprl is an example of an entity which is more than the sum of its parts. It is more than a proof checker or proof-generating editor. It is more than an evaluator for a rich class of functional expressions and more than a system for writing heuristic procedures to find proofs in a specific foundational theory. The integration of these parts creates a new kind of system. One can sense new possibilities arising from this combination both in the system as it exists now and in its potential for growth.

We find that Nuprl as it runs today serves not only as a new tool for writing programs and program specifications but also as a tool for writing nearly any kind of mathematics. Working in the Nuprl environment results in a distinctive style of mathematics--a readable yet formal algorithmic style. The style in turn suggests new mathematical substance such as our treatment of recursive types and partial functions [Constable & Mendler 85]. Nuprl also offers a coherent way to organize and teach a collection of concepts that are important in computer science.

As we extrapolate the course of Nuprl's development we see the emergence of a new kind of ``intelligent'' system. The mechanisms for the accumulation of mathematical knowledge in the form of definitions, theorems and proof techniques are already in place, and as more of this knowledge is accumulated the system exhibits a more widely usable brand of formal mathematics. Furthermore, since the tactic mechanism gives the system access to the contents of its libraries, one can envision altering the system so that it generates and stores information about itself. In this sense Nuprl is an embryonic intelligent system.

This Document

Scope

More than just a user's manual for a specific system, this book serves as an introduction to a very expressive foundational theory for mathematics and computer science, a theory which brings together many diverse ideas in modern computing theory. The book is also an introduction to formal logic in general and to constructive logic in particular, and it introduces new methods of program development and verification.

This book also describes a computer system for doing mathematics. The system provides a medium distinct from the traditional paper and blackboard, an active medium that can detect errors, implement tedious steps of argument or computation and carry out suggestions for building proofs. In Nuprl a new level of precision is made useful.

This book also introduces an ongoing enterprise and a new area of research. It presents a first example of the kind of system that we believe will become significant in the next decade. There is clearly much to be done in this area, and this document will make readers aware of certain open problems and challenging tasks.

Organization

This book includes a tutorial, a reference manual and a summary of research conducted on, and in, the system. The tutorial spans chapters 2 to 6. Chapter 2 presents a systematic foundational explanation of the mathematical theory underlying the Nuprl system, and it attempts to make the basic notions clear and self-evident. Chapter 3, with its collection of examples of statements in Nuprl, serves as the most concrete introduction to the system, and indeed certain readers may wish to start there. Chapter 4 introduces the reader to the Nuprl proof theory, again with lots of examples, and chapter 5 illustrates the system's function in the context of programming. Chapter 6 presents the metalanguage and the concept of tactics.

The reference section of this book comprises chapters 7 through 9. Chapter 7 details the organization of the system and contains a summary of commands and techniques users will find handy. Chapter 8 contains a brief account of the theoretical underpinnings of the system and gives a summary of the rules and ML constructors and destructors associated with the logic. Chapter 9 provides a detailed explanation of tactics.

The remaining chapters in this book consist of information and research results which will be of interest to the advanced user. Chapter 10 contains several recommendations about theory development which should prove extremely helpful for heavy users of Nuprl. Chapter 11 lays out a library of mathematical results we have obtained using the system, while chapter 12 presents recent developments in the logic which should be implemented by September 1985.

The remainder of this chapter discusses the place of Nuprl in computer science research, specifically its relationship to logic, semantics, programming methodology, automated reasoning and intelligent systems. For those readers interested in research, this will provide both a motivation and a framework for further reading.

Research Topics

Programming Languages

As a programming language Nuprl is similar to functional programming languages with a rich type structure such as Edinburgh ML. However, the type structure of Nuprl is richer than that of any existing programming language in that it allows dependent functions and products as well as sets, quotients and universes. Moreover, our approach to type checking enables the user to design automatic type-checking algorithms which extend those of other type systems. There are interesting connections between concepts in Nuprl and various new ideas being suggested for programming languages; see for example Russell  [Donahue & Demers 79], Pebble [Burstall & Lampson 84] and Standard ML [Milner 85].

Presently Nuprl is only interpreted, so it is much slower than languages with compilers. However, for a simpler subsystem, Lambda-prl, an optimizing compiler has been implemented (see [Sasaki 85]). There are many challenging issues here for people interested in building a new kind of optimizing compiler, as, for instance, the fact that programs usually occur in the context of their specifications means that there is more information available for good optimizations than is typically the case.

Nuprl is also a formal logical theory, so one would expect a connection with logic programming and with PROLOG [Clocksin & Mellish 81]. In fact it is possible to express some aspects of PROLOG in a subset of Nuprl and to use a linear resolution tactic to execute specifications in this subset. Nuprl does not optimize such a proof tactic, however, so the execution would be slower than in existing PROLOG evaluators. Moreover, the usual way to use theorem-proving power computationally in Nuprl involves proving a theorem of the form

for all $x$ of type $A$ there is a $y$ of type $B$ such that $R(x,y)$
and then extracting a program from this proof. Thus in Nuprl a theorem prover is used more as a compiler than as an evaluator.


Semantics

From a semantic point of view the logic of Nuprl is like set theory in that it is a foundational theory of mathematics [Aczel 78,Barwise 75,Friedman 73,McCarty 84,Myhill 75]. We can try to explain the basic intuitions behind the theory to the point that the rules become self-evident; chapter 2 attempts this. We can also relate this theory to other foundational theories such as classical set theory. On the other hand it is just as meaningful and interesting to attempt to understand classical set theory in terms of type theory and to relate this theory to other apparently simpler ones such as constructive number theory (see [Beeson 83,Beeson 85]).

For computer scientists it is especially interesting to relate this theory to the theory of domains [Scott 76,Stoy 77] because both are attempts to give a mathematically rigorous account of computation. Thus, while it is not necessary to provide a ``denotational semantics'' for Nuprl as the basis for reasoning about it, one might do so to compare approaches. It is also reasonable to use Nuprl to give a constructive denotational semantics for programming languages; this topic is discussed briefly in chapter 11.

Methodology and Verification

Nuprl embodies a particular programming methodology and carries it to the level of complete formalization and implementation. However, one can use the system and employ the methods at various levels of rigor. It is possible to program in Nuprl in a freewheeling manner with no attention to correctness; it is also possible to state only some properties that a program will satisfy and to present only the barest sketch of an argument that the program meets these specifications. On the other hand, in the same system one can also tighten control over the program step by step and level by level until there is a completely finished machine-checked proof that the program meets its specifications. In a sense the entire book illustrates this methodology, but in chapter 11 there are examples which relate our methods to those of the more popularly exposited school of E. W. Dijkstra, C. A. R. Hoare, E. C. R. Hehner, D. Gries and others [Dijkstra 76,Hoare 72,Gries 81,Hehner 79].

Environments

The editing facilities of this system were inspired in part by those of the Cornell Program Synthesizer [Teitelbaum & Reps 81] and by AVID [Krafft 81], the system which first applied these ideas in the setting of proof synthesis. We have been using these editors in the Lambda-prl system since 1983. We know how to use them effectively, and while we have not seen demonstrated a better way of generating proofs, based on our experience with these systems we now understand feasible ways to improve them significantly. Research on this topic is under way in our group.

Theorem Proving

Mathematical texts consist not only of definitions and theorems but also of proof techniques. To formalize mathematics one must formalize these methods as well. In Nuprl this is done by expressing proof methods as programs in the ML programming language. We think of ML as formalizing the computational part of the metalanguage. One of the research topics of our group concerns the complete formalization of the metalanguage (see [Knoblock 86]).

This approach to formalization brings with it a method of mechanizing reasoning in Nuprl, for as users write more and more elaborate proof-building methods the system can do more of the work of finding proofs. This approach to ``theorem proving'' continues the tradition of our earlier work on PL/CV [Constable, Johnson, & Eichenlaub 82,Constable & O'Donnell 78] and follows in the spirit of the Edinburgh LCF project, which spawned ML. The style of formalization extends the AUTOMATH [deBruijn 80] approach to presenting proofs, an approach which relies mainly on a very high-level language for writing proofs. As more and more complex tactics are built this line of research comes closer to the mainstream work in automated theorem proving  [Andrews 71,Bibel 80,Bledsoe 77,Boyer & Moore 79,Loveland 78,Weyhrauch 80,Wos et al. 84]. It is conceivable that one would write a tactic which is so ambitious that it would be classified as a ``theorem prover''.

Although we have written many useful tactics and although the system provides a nontrivial level of deductive support, none of our methods can presently be classified as theorem provers. We are, however, exploring some interesting new methods such as analogy tactics and ``expert reasoners'' which we think will be contributions to the subject of automated reasoning.


Program Synthesis

The Nuprl system acts as a program synthesizer in the following sense. Given a computationally meaningful assertion (e.g., a ``program specification'') and an applicable proof tactic which produces at least the executable parts of a proof of the assertion, the Nuprl extractor will produce from the proof a program. If the proof is complete then the program meets the specification. In this sense we have written a variety of program-synthesizing tactics. Several interesting comparisons can be drawn between these techniques and those based on classical methods, as in [Manna & Waldinger 80,Manna & Waldinger 85].


Artificial Intelligence

The language of Nuprl has been described as a ``logic for artificial intelligence'' [Turner 84]. The Nuprl system can be viewed as an intelligent system, and many of the things we do with it and to it might be characterized as improving its ``intelligence''. As we develop more ``expert reasoners'' similar to those for equality and arithmetic, for example, we certainly increase the deductive power of the system, especially as we allow them to cooperate [Nelson & Oppen 79]. The natural growth path for a system like Nuprl tends toward increased ``intelligence''. This is obvious when we think about adding definitions, theorems and methods to the library. It is less obvious and more noteworthy that other changes move it in this direction as well. For example, it is helpful if the system is aware of what is in the library and what users are doing with it. It is good if the user knows when to invoke certain tactics, but once we see a pattern to this activity, it is easy and natural to inform the system about it. Hence there is an impetus to give the system more knowledge about itself. This is related to recent themes in the field of artificial intelligence  [Bundy 83,Charniak & McDermott 85,Davis & Lenat 82].

Related Work

Close Relatives

The literature most closely related to this comes from Martin-Löf [Martin-Löf 73,Martin-Löf 82] and the Swedish computer scientists at Goteborg who are concerned with making type theory a usable formalism [Nordstrom 81,Nordstrom & Petersson 83,Nordstrom & Smith 84]. The AUTOMATH work at Eindhoven in The Netherlands is also closely related [deBruijn 80,Jutting 79,van Daalen 80,Zucker 75], as is the work at INRIA [Coquand & Huet 85]. In fact, deBruijn's ideas are direct predecessors of those in Martin-Löf's writings with intermediate refinements from Scott [Scott 70]. One can see in deBruijn's work the influence of his fellow mathematician and countryman, L. E. J. Brouwer, the founder of Intuitionism [Brouwer 23]. We will examine some of these influences below as well as trace the influence of more recent research such as the work of J. L. Bates [Bates 79] and Constable [Constable 71,Constable & Zlatin 84,Constable 85].

Intuitionism and Type Theory

In his 1907 doctoral thesis [Brouwer 23] Brouwer advanced the view that the basis of mathematics and of logic is found in the capacity of human beings to carry out mental constructions. On the method of proof by contradiction he says, ``The words of your mathematical demonstration merely accompany a mathematical construction that is effected without words. At the point where you enounce the contradiction, I simply perceive that the construction no longer goes, that the required structure cannot be imbedded in the given basic structure. And when I make this observation, I do not think of a principium contradictionis.''

In the 1960's the mathematician E. Bishop carried out a sweeping development of mathematics along the lines conceived by Brouwer. Bishop's works, and those of his followers [Bishop 67,Bishop & Bridges 85,,Bridges 79,Chan 74], have started a modern school of constructive mathematics that we believe is in harmony with the influence of computing in mathematics, an influence seen in many quarters [Nepeivoda 82,,Goto 79,Takasu 78]. In Bishop's words [Bishop 67], ``The positive integers and their arithmetic are presupposed by the very nature of our intelligence.... Every mathematical statement ultimately expresses the fact that if we perform certain computations within the set of positive integers, we shall get certain results.... Thus even the most abstract mathematical statement has a computational basis.''

Very different views of mathematics were put forward by G. Frege [Frege 1879] and by Russell [Russell 08,Whitehead & Russell 25], as they attempted to reduce ``mathematical'' ideas to ``logical'' ideas. We shall not consider the philosophical points here, but we note that Frege gave us the predicate calculus in Begriffssschrift and that Russell and Whitehead gave us Principia Mathematica, a formal system of mathematics based on type theory.

Nuprl can be seen as expressing the philosophical ideas of Brouwer and Bishop in a language closely related to the type theory of Russell. Types prescribe constructions; some of these constructions are recognized as the meaning of propositions.

Theoretical Background

In 1930 the Intuitionist mathematician A. Heyting [Heyting 30] presented a set of rules that characterized Intuitionistic logic and differentiated it from classical logic. In addition he formulated Intuitionistic first-order number theory (based on Peano's famous axioms) as the classical theory without the law of the excluded middle. (The Intuitionistic theory is often called Heyting arithmetic.)

In 1945 the logician S. C. Kleene proposed his well-known realizability interpretation of Intuitionistic logic and number theory [Kleene 45]. He showed that any function definable in Heyting arithmetic is Turing computable. This raised the possibility that formal systems of Intuitionistic logic could be used as programming languages. A specific proposal for this was made by Constable [Constable 71] as part of a study of very high-level programming languages and by Bishop [Bishop 70] as part of his study of constructive analysis [Bishop 67]. In 1976 Constable together with his students M. J. O'Donnell, S. D. Johnson, D.B. Krafft and D.R. Zlatin developed a new kind of formal system called programming logic [Constable 77,Constable & O'Donnell 78,Constable, Johnson, & Eichenlaub 82] which interpreted programs as constructive proofs and allowed execution of these proofs. This system is called PL/CV.

The propositions-as-types principle [Curry, Feys, & Craig 58,Howard 80] offered a new way to interpret constructive logic and extract its constructive content. These ideas came to us from [Stenlund 72,Martin-Löf 73] and were applied in the PL/CV setting in version V3 [Constable & Zlatin 84,Stansifer 85]. They were further refined by Bates [Bates 79] and became the basis for the actual Nuprl system [Bates & Constable 85,Bates & Constable 83].

Much of our recent theoretical work has focused on the Nuprl system. In his Ph.D. thesis R. W. Harper [Harper 85] investigated the relative consistency of Nuprl with Martin-Löf's theories, and he established the theoretical basis for automating equality reasoning in Nuprl. S. F. Allen has studied a rigorous semantic account of type theory; some of his ideas appear in chapter 8. Mendler and Constable have studied recursive types and partial functions[Constable & Mendler 85]; some of these results appear in chapter 12.

Systems Background

In 1979 Bates [Bates 79] proposed the notion of refinement logic and an interactive style of doing proofs in such a logic (see also  [Kay & Goldberg 77,Smullyan 68,Toledo 75]). At the same time our experience with the Cornell Program Synthesizer of R. Teitelbaum and T. Reps [Teitelbaum & Reps 81] directly influenced our thinking about proof editors. Some of these ideas were first tested by Krafft for the PL/CV logic in a system called AVID [Krafft 81]. Bates also proposed specific ways to extract executable code from constructive proofs that would be efficient enough for use in a programming system. In 1982 a specific system of this kind was designed and implemented by the Prl group at Cornell [Bates & Constable 85,Nuprl Staff 83]; that system is Lambda-prl.

The Lambda-prl system was designed to interact with the metalanguage ML from the Edinburgh LCF project [Gordon, Milner, & Wadsworth 79].1.4The Lambda-prl system also incorporated decision procedures from the PL/CV project; indeed the early Lambda-prl style of automated reasoning is a synthesis of the ideas from AUTOMATH, PL/CV and LCF. Now a distinctive new style is emerging, a style which will be reported in the work of some of the authors of this monograph.

The Nuprl logic itself was designed as an attempt to present the Cornell version of constructive type theory in the setting a of refinement-style logic. The result of this design is embodied in the system and in this document.

Footnotes

...1.1
Nuprl is version ``nu'' of our Proof Refinement Logics. Earlier versions were ``micro'' and ``lambda'' [Nuprl Staff 83].
... types,1.2
The concept of a universe in this role, to organize the hierarchy of types, is suggested in [Artin, Grothendieck, & Verdier 72] and was used by Martin-Löf [Martin-Löf 73]. This is a means of achieving a predicative type structure as opposed to an impredicative one as in Girard [Girard 71] or Reynolds [Reynolds 83].
...1.3
In the discussion which follows we will use typewriter font to signify actual Nuprl text and $mathematical$ font for metavariables.
...ML.1.4
This is one result of a joint Cornell/Edinburgh study of programming logics and automated reasoning begun in 1981-82 and continuing with joint studies of type theory and polymorphism.
next up previous contents
Next: Introduction to Type Theory Up: Index Previous: Contents   Contents
PRL Home
Introduction
The Nuprl book
Origins of the PRL Project
Goals
Dynamics of the Project
Mathematical Expression in Nuprl
Cross Links to Math & CS Fields
Knowledge Base
Math Library
Publications
Projects
CRASH
Nuprl/FDL System
EventML Software
Seminar
People
Wiki
The Book
Lectures
Other Groups


Website feedback
PRL Project   |   Computer Science Department   |   Cornell University
nuprl@cs.cornell.edu   |   320 Gates Hall, Ithaca, NY 14853   |   © 2014 Cornell University
site admin | Prof Constable's Library