A User-Level Introduction to the Nuprl Proof Development System
This document is intended to introduce the key elements of the Nuprl Proof Development Sys tem (Nuprl, for short) from the perspective of a Nuprl user, as opposed to the perspective of someone intimately involved in developing or extending Nuprl. As such, it may be more appropriate than other Kuprl-related documents for readers who are primarily concerned with uses of Nuprl and not fine details of Nuprl's mathematical foundation. It introduces and illustrates key Kuprl concepts -such as types, terms, displayforms, and tacticsin the framework of a model of calculational predicate logic inference. 1 Preface and Context The bulk of this document is a (lightly edited) chapter from the doctoral dissertation [2]. Unlike other documents introducing key elements of the Nuprl Proof Development System (Nuprl, for short) [8, 121, it was not written by an author whose primary concern was further developing the underlying Nuprl system per se. Instead, it was written in the context of a project that applied Nuprl to formally represent a kind of human reasoning. That is, it was written by a user of Nuprl, not primarily a developer, for readers more attuned to uses of Nuprl than to fine details of its foundation. Before presenting this introduction to Nuprl concepts, we present a concise description of its context, the research from which it emerged. The remainder of this section is an extremely brief overview of the ideas in [2]; interested readers are strongly encouraged to read the less-brief overviews in the introductory material of the dissertation itself. The research explores a new, interdisciplinary approach to cognitive modeling of highlevel inference, combining complementary ideas from applied logic, artificial intelligence, and cognitive science. The dissertation describes an application of this approach to a particular inference task: the stylized method for theorem proving in calculational predicate logic (described in the undergraduate-level textbook [Ill), a variant of classical first-order predicate logic. Theorems are proved in calculational logic by applying a chain of equality-preserving rewrites; for instance, expression A = B could be proved by rewriting -4 t o B or by Theorem Change of Dummy. Provided -occurs( " y " , " R , P" ) and function f has an inverse, (*x I R : P ) = (*y I R[x := f .y] : P[x := f .y]) . Proof. We start with the right side of (*x I R : P ) = (*y I R[x := f.y] : P[x := f.y]) and show it is equal to the left side. (*y 1 R[x := f.y] : P[x := f.y]) = (One-point rule (8.14) -Quantification over x has to be introduced. The Onepoint rule is the only theorem that can be applied at first.) (*y I R[x:= f.y] : (*x 1 x = f . y : P ) ) = (Nesting (8.20) -Moving dummy x t o the outside gets us closer to the final form.) (*x, y I R[x := f.y] A x = f.y : P ) = (Substitution (3.84a) R[x := f.y] must be removed at some point. This substitution makes it possible.) (*x,y I R[x:=x] A x = f . y : P ) = ( R[x := x] E R ; Nesting, -occurs( " y " , " f in ) -Now we can get a quantification in x alone.) (*x I R:(*y I x = f . y : P ) ) = ( x = f .y y = f-' .x T h i s step prepares for the elimination of y using the One-point rule.) (*x I R : (3 I = f l .2 : P ) ) = (One-point rule (8.14)) (*z 1 R : P[y := f-'.XI) = (Definition of textual substitution loccurs( " y " , " P " ) ) (*x I R : P ) Figure 1: Proof of Theorem Change of Dummy. rewriting the entire expression to a previously proved theorem. Calculational logic supports schematic reasoning via nletalinguistic operations (such as textual substitution) as well as traditional logical reasoning, all without resorting to a higherorder logic. In particular, it supports reasoning about a general quantifier form -i.e., a general form that can be instantiated into universal quantification, existential quantification, and other quantifier-like accumulation operations (such as sums or products over sets)that is seen in Figure 1, a calculational proof of a theorem about a familiar property of bound variables. The unusual (* . . .) syntax represents that general quantifier form; the variable next to the * (e.g., x in (*x.. .) ) is bound in that expression. The theorem holds for any instantiation, including both existential and universal quantifiers. (A full explanation of the proof is beyond the scope of this paper. See [2] or [ l l ] for details.) Because of this metalinguistic character, we interpret calculational logic as a metalogic; theorems such as Change Of Dummy (Figure 1) are meta-level theorems about theoremhood in some object-level logic. We occasionally refer to this fact in the sections that follow, but it is of only secondary importance to our introduction to Nuprl. Readers interested in further details should see [2] or [3]. To implement a Nuprl model of how people perform calculational logic inference, we implemented three distinct levels of mathematics. One level consists of the programs that simulate the inference processes people use we return to that level shortly. We also implemented two distinct levels of logical language. Calculational logic employs metalinguistic operations; the semantics of metalanguage variables and expressions is described with respect t o a lower-level object language. Thus, we implemented the metalanguage that actually appears in proofs like Figure 1 as well as a simple object language to use in implementing the semantics of our metalanguage. We call our formalized metalanguage the data language, because it is the language that people actually use for the calculational logic of [ll] it is the data that guided our implementation. Expressions of the data language may be called data expressions. It was not trivial to identify and formalize a data language adequate for the material in [ll] that we covered, but details of that process are beyond the scope of this paper. Again, interested readers can see the dissertation [2] or the stand-alone paper [3] for further information. As part of formalizing a semantics for our data language, we implemented a recursive type OE of object language expressions (object expressions, for short). Neither the details of type OE nor the object language itself is relevant in this paper. Readers should simply understand the role of OE: variables (and expressions) in the data language may be of type OE. To further explain the role of metalanguage in our formalization of calculational logic, consider the syn~bol + . It has two meanings in our Nuprl implementation. As a symbol in the data language, it is an object-language implication constructor: an operator that, on two arguments of type OE, returns an expression of type OE. (There are, of course, several OEconstructors in the data language, as mentioned in section 2.3.) The other meaning is as standard logical implication on data language expressions: an operator that, given two truth-valued expressions in the data language, returns a truth value. For readers unfamiliar with metalogic, this bears repeating: For one meaning, the symbol stands for a function that returns object expressions; for the other meaning, it stands for a function that returns truth values. (Context disambiguates which meaning of the symbol is intended at any time.) We refer to such metalinguistic constructions later in the paper. Additional explanation of the underlying ideas can be found in [2] and [3], but readers need not fully grasp these ideas to utilize this paper as an introduction to Nuprl. To implement the actual inference models, we used Nuprl's tactic system (based on [lo]). The practice of using tactics in automated reasoning allows fully formalized mathematical inference to be expressed and manipulated a t a level of abstraction away from primitive logical rules. Tactics are intended to capture high-level inferences, including those that people might naturally make in constructing a proof, and cognitive modeling of logical inference seems like a natural application for tactic-based automated reasoning systems. We apply Nuprl for precisely that reason. (We discuss tactics further in section 3.2.) The Nuprl proof development system provided a platform for implementing our model of calculational logic inference. This paper is an overview of Nuprl, intended both as an introduction for the uninitiated and, for readers familiar with Nuprl, a brief summary of the Nuprl features most important for the model in [2]. In the text that follows, we use the word "implementer" to refer to a user of Nuprl, i.e., one (such as the author) who uses Nuprl to formalize and implement a mathematical language and/or system of inference. For history of Nuprl and a more complete introduction, see [8] and [12]. 2 Implementing Mathematics in Nuprl In this section, we introduce some important features of Nuprl that we used in implementing the data language. Our definitions were essentially built from Nuprl's type system and expressed by Nuprl t e r m s , so we briefly discuss types and terms. We also introduce Nuprl's system of d i s p l a y forms, which preserves the useful distinction between mathematical concepts and notation; for many Nuprl objects, their display forms -which describe how the objects are to be displayed in various contextsare defined separately from the objects themselves. We exploit display forms in several important ways. We do not yet consider concepts particular to definitions of calculational logic inference methods or other meta-level programs in this section. We discuss them in the next section.