The Nuprl project at Cornell University constitutes a significant advance in machine-assisted theorem proving. This book gives a global description of the project. Despite the number of authors, the book is not just a collection of individual papers. It has been edited into a clear and well-organized treatise.
Nuprl is an interactive system that supports theorem proving in the typed lambda calculus. Nuprl proofs are constructive, which means that a theorem of the form “object x exists” is closely related to an algorithm that can compute x. Thus Nuprl also supports the development of algorithms along with their correctness proofs.
Nuprl is highly interactive. It can automatically generate much of the tedious detail of a proof, but it does not attempt to prove entire theorems in a batch mode. Instead, it helps the user to keep track of the interesting parts of a proof, maintains libraries of relevant information, and checks the user’s inputs for validity. Nuprl also uses the metalanguage ML for expressing tactics, algorithms that attempt to fill in the details of a proof or to transform one proof into another.
Nuprl exploits the inherently computational nature of constructive mathematics. For example, the user can state a theorem that says that an object exists that has certain properties. The user and Nuprl can then work together to prove this theorem. Finally, a function that computes the object can be extracted automatically from the constructive proof. The book contains several examples of this process. A typical example begins with a statement that for all positive integers x there exists a unique integer y that is the largest integer less than or equal to the square root of x. This is stated in Nuprl by
>> all x:int. x>=0 => some y:int. y2*y <= x < (y + 1)2 * (y + 1):9F:Y
The proof proceeds by induction. The base case is trivial, and the inductive step operates by assuming that the square root of x−1 is y0 and then showing that the square root of x is either y0 or y0 + 1. The decision is made by comparing x with (y0 + 1)2. After going through the rather lengthy formal proof, the user can then ask the system to prove that a specific integer x has a square root. That proof is constructive, and it will construct the square root.
The authors list four goals for their book: they intend it to be (1) a tutorial on the new mathematical techniques, (2) a user manual, (3) an overview of an ongoing research project, and (4) a presentation of new research results. These goals are all met quite successfully. However, this book is not introductory; it requires some background in mathematical logic and set theory. In addition, the book’s diverse goals lead to an uneven style. Parts of it are very readable, other parts are concise and technical, while some sections are mainly aimed at someone who can interact with Nuprl while reading the book. However, these are not really drawbacks. Nuprl is inherently interactive, a major improvement over older batch-oriented theorem provers. In order to convey the spirit of such a system, the authors must show some detailed examples, complete with interactive commands, in addition to describing the underlying theory.
The book is organized into three parts. Part 1 is a tutorial that explains the typed lambda calculus and shows how to carry out proofs and evaluations in Nuprl. Part 2 is a system reference manual. This will be most useful to people who are actually using the program. Part 3 presents more advanced material and gives several extended examples of theories developed in Nuprl.
The authors have explained the material clearly, although some sections are very concise. In addition, the book has been carefully edited, and there are few typographical errors. Many of the examples are snapshots taken from real interactions with Nuprl, edited to be more readable. The bibliography is quite long, giving many useful pointers to the literature on constructive mathematics and automated theorem proving systems. Unfortunately the bibliography is not annotated, so it is left to the reader to decide which references would be interesting.
This book is essential reading for anyone interested in current research on the application of mathematical logic to programming and vice versa. It is not an introductory tutorial covering these fields.
