In this file will be found Chapter 4 (the logic) and Chapter 12 (the reference guide) of the second edition of A Computational Logic Handbook, Boyer and Moore, Academic Press, 1997, distributed by permission of Academic Press. 1. A Precise Description of the Logic @label(LOGIC) 2. Apologia Traditionally, logicians keep their formal systems as simple as possible. This is desirable because logicians rarely use the formal systems themselves. Instead, they stay in the metatheory and (informally) prove results about their systems. The system described here is intended to be used to prove interesting theorems. Furthermore, we want to offer substantial mechanical aid in constructing proofs, as a means of eliminating errors. These pragmatic considerations have greatly influenced the design of the logic itself. The set of variable and function symbols is influenced by conventions of half a dozen different Lisp systems. The set of axioms is unnecessarily large from the purely logical viewpoint. For example, it includes axioms for both the natural numbers and ordered pairs as distinct classes of objects. We found certain formalization problems cumbersome when one of these classes is embedded in the other, as is common in less pragmatically motivated logics. Furthermore, the distinction between the two classes makes it easier for us to provide mechanical assistance appropriate to the particular domain. Similarly, a general purpose quantifier over finite domains is provided, even though recursively defined functions suffice. We provide an interpreter for the logic in the logic-at the cost of complicating both the notation for constants and the axioms to set up the necessary correspondence between objects in the logic and the term structure of the language- so that certain useful forms of metatheoretic reasoning can be carried out in the logic. Our induction principle is very complicated in comparison to those found in many other logics; but it is designed to be directly applicable to many problems and to produce simple proofs. To achieve our goal of providing assistance in the proof of interesting theorems it must be possible, indeed, convenient, to state interesting theorems. This requires that we allow the user to extend the logic to introduce new objects and concepts. Logically speaking, the main theorem and all the intermediate lemmas are proved in the single final theory. But practically speaking, the theory ``evolves'' over time as the user repeatedly extends it and derives intermediate results. We provide three ``extension'' principles-the ``shell principle'' for introducing new, inductively-defined data types, the ``definitional principle'' for defining new recursive functions, and the ``constraint principle'' for introducing functions that are undefined but constrained to have certain properties. Our extension principles, while complicated, are designed to be sound, easy to use and to mechanize, and helpful in guiding the discovery of proofs. While the logic is complicated compared to most mathematical logics, it is simple compared to most programming languages and many specification languages. If our presentation of it makes it seem ``too complicated'' it is perhaps merely that we are presenting all of the details. 3. Outline of the Presentation In presenting our logic we follow the well-established tradition of incremental extension. We begin by defining a very simple syntax, called the formal syntax, of the language. A much richer syntax, called the extended syntax, which contains succinct abbreviations for constants such as numbers, lists, and trees, is defined only after we have axiomatized the primitive data types of the logic. Using the formal syntax we present the axioms and rules of inference for propositional calculus with equality, the foundation of our theory. Next we embed propositional calculus and equality in the term structure of the logic by defining functional analogues of the propositional operators. We then present the shell principle and use it to add the axioms for natural numbers, ordered pairs, literal atoms, and negative integers. At this point we have enough formal machinery to explain and illustrate the extended formal syntax. We then present our formalization of the ordinals up to epsilon-0. The ``less-than'' relation on these ordinals plays a crucial role in our principles of mathematical induction and recursive definition. Next we add axioms defining many useful functions. Then we embed the semantics of the theory in the theory by axiomatizing an interpreter for the logic as a function. In order to do this it is necessary to set up a correspondence between the terms in the formal syntax and certain constants in the logic, called the ``quotations'' of those terms. Roughly speaking, the quotation of a term is a constant in the logic whose value under the interpreter is equal to the term. We complete the set of axioms by defining our general purpose quantifier function, which, much like the ``mapping'' functions of Lisp, includes among its arguments objects denoting terms which are evaluated with the interpreter. Finally, we state the principles of inductive proof and recursive definition. We frequently pause during the presentation to illustrate the concepts discussed. However, we do not attempt to motivate the development or explain ``how'' certain functions ``work'' or the role they play in the subsequent development. We assume that the reader interested in such asides will have first read the primer, Chapter 2. Familiarity with the primer is completely unnecessary to follow the precise development of the theory. We classify our remarks into eight categories: - Terminology: In paragraphs with this label we define syntactic notions that let us state our axioms or syntactic conventions precisely. The concept defined is italicized. - Abbreviation: In paragraphs with this label we extend the previously agreed upon syntax by explaining how some string of characters is, henceforth, to be taken as shorthand for another. - Example: We illustrate most of the terminology and abbreviations in paragraphs with this label. Technically, these paragraphs contain no new information, but they serve as a way for the reader to check his understanding. - Axiom or Defining Axiom: A formula so labelled is an axiom of our system. Axioms of the latter sort are distinguished because they uniquely define a function. - Shell Definition: A paragraph so labelled schematically specifies a set of axioms of our system. - Extension Principle: A paragraph so labelled describes a principle which permits the sound introduction of new function symbols and axioms. - Rule of Inference: A paragraph so labelled describes a rule of inference of our system. - Note: Assorted remarks, such as alternative views, are collected in paragraphs with this label. 4. Formal Syntax @label(formal-symbol) Terminology. A finite sequence of characters, s, is a symbol if and only if s is nonempty, each character in s is a member of the set {A B C D E F G H I J K L M N O P Q R S T U V W X Y Z 0 1 2 3 4 5 6 7 8 9 $ ^ & * _ - + = ~ { } ? < >}, and the first character of s is a letter, i.e., in the set {A B C D E F G H I J K L M N O P Q R S T U V W X Y Z}. Examples. PLUS, ADD1, and PRIME-FACTORS are symbols. *1*TRUE, 123, A/B, and #.FOO are not symbols. Terminology. The variable symbols and function symbols of our language are the symbols other than T, F, and NIL. Terminology. Associated with every function symbol is a nonnegative integer called the arity of the symbol. The arity indicates how many argument terms must follow each application of the function symbol. The arity of each function symbol in the Ground Zero logic is given in the table below. We also include brief descriptive comments in the hopes that they will make subsequent examples more meaningful. Table 4.1 symbol arity comment ------------------------------------------------------------------------------ ADD1 1 successor function for natural numbers ADD-TO-SET 2 adds an element to a list if not present AND 2 logical and APPEND 2 list concatenation APPLY-SUBR 2 application of primitive fn to arguments APPLY$ 2 application of fn to arguments ASSOC 2 association list lookup BODY 1 body of a fn definition CAR 1 first component of ordered pair CDR 1 second component of ordered pair CONS 2 constructs ordered pairs COUNT 1 size of an object DIFFERENCE 2 natural difference of two natural numbers EQUAL 2 equality predicate EVAL$ 3 interpreter for the logic FALSE 0 false object FALSEP 1 predicate for recognizing FALSE FIX 1 coerces argument to 0 if not numeric FIX-COST 2 increments cost if argument is non-F FOR 6 general purpose quantifier FORMALS 1 list of formal arguments of a function GEQ 2 greater than or equal on natural numbers GREATERP 2 greater than on natural numbers IDENTITY 1 identity function IF 3 if-then-else IFF 2 if and only if IMPLIES 2 logical implication LEQ 2 less than or equal on natural numbers LESSP 2 less than on natural numbers LISTP 1 recognizes ordered pairs LITATOM 1 recognizes literal atoms MAX 2 maximum of two natural numbers MEMBER 2 membership predicate MINUS 1 constructs negative of a natural number NEGATIVEP 1 recognizes negatives NEGATIVE-GUTS 1 absolute value of a negative NLISTP 1 negation of LISTP NOT 1 logical negation NUMBERP 1 recognizes natural numbers OR 2 logical or ORDINALP 1 recognizes ordinals ORD-LESSP 2 less than on ordinals up to epsilon-0 PACK 1 constructs a LITATOM from ASCII codes PAIRLIST 2 pairs corresponding elements PLUS 2 sum of two natural numbers QUANTIFIER-INITIAL-VALUE 1 initial value of a quantifier QUANTIFIER-OPERATION 3 operation performed by quantifier QUOTIENT 2 natural quotient of two natural numbers REMAINDER 2 mod STRIP-CARS 1 list of CARs of argument list SUB1 1 predecessor function on natural numbers SUBRP 1 recognizes primitive function symbols SUM-CDRS 1 sum of CDRs of elements of argument list TIMES 2 product of two natural numbers TRUE 0 true object TRUEP 1 recognizes TRUE UNION 2 union of two lists UNPACK 1 explodes a LITATOM into ASCII codes V&C$ 3 determines value and cost of an expr V&C-APPLY$ 2 determines value and cost of fn application ZERO 0 0 ZEROP 1 recognizes 0 and nonnatural numbers ------------------------------------------------------------------------------ The arity of each user-introduced function symbol is declared when the symbol is first used as a function symbol. Terminology. A term is either a variable symbol or else is a sequence consisting of a function symbol of arity n followed by n terms. Note. Observe that we have defined a term as a tree structure rather than a character sequence. Of interest is how we display such trees. Terminology. To display a symbol, we merely write down the characters in it. To display a term that is a variable symbol, we display the symbol. To display a non-variable term with function symbol fn and argument terms t , 1 ..., t , we write down an open parenthesis, a display of fn, a nonempty string n of spaces and/or carriage returns, a display of t , a nonempty string of 1 spaces and/or carriage returns, ..., a display of t and a close parenthesis. n Note. In the first edition of this handbook, we permitted comments in the display of formal terms. In the second edition, we have disallowed comments in formal terms. Comments are permitted in the extended syntax, which is the syntax used throughout the book (once that syntax is defined) and in the implementation. Thus, the only effect of this change is to delay the precise description of the comment convention until we present the extended syntax. Examples. The following are (displays of) terms: (ZERO) (ADD1 X) (PLUS (ADD1 X) (ZERO)) (IF B (ZERO) (ADD1 X)) (IF B (ZERO) (ADD1 X)) Terminology. Our axioms are presented as formulas in propositional calculus with equality. The formulas are constructed from terms, as defined above, using the equality symbol and the symbols for ``or'' and ``not''. More precisely, an atomic formula is any string of the form t1=t2, where t1 and t2 are terms. A formula is either an atomic formula, or else of the form ~ (form1), where form1 is a formula, or else of the form (form1 \/ form2), where form1 and form2 are both formulas. Parentheses are omitted when no ambiguity arises. Abbreviations. We abbreviate ~ (t1 = t2) by (t1 /= t2). If form1 and form2 are formulas then (form1 -> form2) is an abbreviation for (~ (form1) \/ form2) and (form1 /\ form2) is an abbreviation for ~ (~ (form1) \/ ~ (form2)). 4.1. Terminology about Terms Terminology. To talk about terms, it is convenient to use so-called ``metavariables'' that are understood by the reader to stand for certain variables, function symbols, or terms. In this book we use lower case words to denote metavariables. Example. If f denotes the function symbol PLUS, and t denotes the term (ADD1 Y), then (f t X) denotes the term (PLUS (ADD1 Y) X). Terminology. If i is a nonnegative integer, then we let Xi denote the variable symbol whose first character is X and whose other characters are the decimal representation of i. Example. If i is 4, Xi is the variable symbol X4. Terminology. A term t is a call of fn with arguments a , ..., a iff t has 1 n the form (fn a ... a ). 1 n Terminology. If a term t is a call of fn we say fn is the top function symbol of t. A function symbol fn is called in a term t iff either t is a call of fn or t is a nonvariable term and fn is called in an argument of t. The set of subterms of a term t is {t} if t is a variable symbol and otherwise is the union of {t} together with the union of the subterms of the arguments of t. The variables of a term t is the set of variable subterms of t. Examples. The term (PLUS X Y) is a call of PLUS with arguments X and Y. PLUS is called in (IF A (PLUS X Y) B). The set of subterms of (PLUS X Y) is {(PLUS X Y) X Y}. The set of variables of (PLUS X Y) is {X Y}. 4.2. Terminology about Theories Notes. Theories evolve over time by the repeated application of extension principles. For example, to construct our logic we start with propositional calculus with equality and extend it by adding the axioms for the natural numbers. Then we extend it again to get ordered pairs and again to get symbols... We eventually start adding axioms defining functions such as Peano sum, product, etc. When we stop, the user of the theorem prover starts by invoking the extension principles to add his own data types and concepts. Each extension principle preserves the consistency of the original logic, provided certain ``admissibility'' requirements are met. In order to describe these requirements it is necessary that we be able to talk clearly about the sequence of steps used to create the ``current'' extension. @label(can-be-proved) Terminology. Formula t can be proved directly from a set of axioms A if and only if t may be derived from the axioms in A by applying the rules of inference of propositional calculus with equality and instantiation (see page @pageref(pc+eq)) and the principle of induction (see page @pageref(INDUCTION)). Terminology. There are four kinds of axiomatic acts: (a) an application of the shell principle (page @pageref(shells)), (b) an application of the principle of definition (page @pageref(defns)), (c) an application of the constraint principle, and (d) the addition of an arbitrary formula as an axiom. Terminology. Each such act adds a set of axioms. The axioms added by an application of the first three acts are described in the relevant subsections. The axioms added by the addition of an arbitrary formula is the singleton set consisting of the formula. Terminology. A history h is a finite sequence of axiomatic acts such that either (a) h is empty or (b) h is obtained by concatenating to the end of a history h' an axiomatic act that is ``admissible'' under h'. An arbitrary axiom is admissible under any h'. The specification of the shell and definitional principles define ``admissibility'' in those instances. Terminology. The axioms of a history h is the union of the axioms added by each act in h together with the axioms described in this chapter. Terminology. We say a formula t is a theorem of history h iff t can be proved directly from the axioms of h. Terminology. A function symbol fn is new in a history h iff fn is called in no axiom of h (except for the propositional, reflexivity, and equality axioms of page @pageref(equality-axioms)), fn is not a CAR/CDR symbol (see below), and fn is not in the set {CASE COND F LET LIST LIST* NIL QUOTE T}. Terminology. We say a symbol fn is a CAR/CDR symbol if there are at least three characters in fn, the first character in fn is C, the last character is R, and each other character is either an A or a D. Examples. The symbol CADDR is a CAR/CDR symbol. We will eventually introduce an abbreviation that ``defines'' such symbols to stand for nests of CARs and CDRs. Because CADDR is a CAR/CDR symbol it is not new. The definitional principle requires that the function symbol defined be ``new.'' Hence, it is impossible to define CADDR. Similarly, it is impossible to define nine other perfectly acceptable symbols, CASE, COND, F, LET, LIST, LIST*, NIL, QUOTE, and T. All of these prohibited symbols will be involved in our abbreviation conventions. 5. Embedded Propositional Calculus and Equality @label(pc+eq) Notes. Our logic is a quantifier-free first order extension of propositional calculus with equality, obtained by adding axioms and rules of inference. Any classical formalization of propositional calculus and equality will suit our purposes. So that this book is self-contained we have included as the first subsection below, one such formalization, namely that of Shoenfield [7]. We then add axioms to define the functional analogues of the propositional operators and the equality relation. This effectively embeds propositional calculus and equality into the term structure of the logic. That is, we can write down and reason about terms that contain propositional connectives, equality, and case analysis. For example, we can write (IF (EQUAL N 0) 1 (TIMES N (FACT (SUB1 N)))) which is a term equal to 1 if N is 0 and equal to (TIMES N (FACT (SUB1 N))) otherwise. The ability to write such terms is very convenient later when we begin defining recursive functions. 5.1. Propositional Calculus with Equality Shoenfield's system consists of one axiom schema and four inference rules. A Propositional Axiom is any formula of the form Axiom Schema. (~ (a) \/ a). The four rules of inference are Rules of Inference. Expansion: derive (a \/ b) from b; Contraction: derive a from (a \/ a); Associativity: derive ((a \/ b) \/ c) from (a \/ (b \/ c)); and Cut: derive (b \/ c) from (a \/ b) and (~ (a) \/ c). To formalize equality we also use Shoenfield's approach, which involves three axiom schemas. A Reflexivity Axiom is any formula of the form Axiom Schema. (a = a). For every function symbol fn of arity n we add an Equality Axiom for fn. @label(equality-axioms) Axiom Schema. ((X1=Y1) -> (... -> ((Xn=Yn) -> (fn X1 ... Xn) = (fn Y1 ... Yn))...)) Finally, we add Axiom. ((X1=Y1) -> ((X2=Y2) -> ((X1=X2) -> (Y1=Y2)))). This axiom is the only instance we need of Shoenfield's ``equality axiom (schema) for predicates.'' Note. Finally, we add the rule of inference that any instance of a theorem is a theorem. To make this precise we first define substitution. Terminology. A finite set s of ordered pairs is said to be a substitution provided that for each ordered pair < v, t> in s, v is a variable, t is a term, and no other member of s has v as its first component. The result of substituting a substitution s into a term or formula x (denoted x/s) is the term or formula obtained by simultaneously replacing, for each < v, t> in s, each occurrence of v as a variable in x with t. We sometimes say x/s is the result of instantiating x with s. We say that x' is an instance of x if there is a substitution s such that x' is x/s. Example. If s is {< X, (ADD1 Y)> < Y, Z> < G, FOO>} then s is a substitution. If p is the term (PLUS X (G Y X)) then p/s is the term (PLUS (ADD1 Y) (G Z (ADD1 Y))). Note that even though the substitution contains the pair < G, FOO> the occurrence of G in p was not replaced by FOO since G does not occur as a variable in p. Rule of Inference. Instantiation: Derive a/s from a. 5.2. The Axioms for TRUE, FALSE, IF, and EQUAL Abbreviation. We will abbreviate the term (TRUE) with the symbol T and the term (FALSE) with the symbol F. Axiom 1. T /= F Axiom 2. X = Y -> (EQUAL X Y) = T Axiom 3. X /= Y -> (EQUAL X Y) = F Axiom 4. X = F -> (IF X Y Z) = Z Axiom 5. X /= F -> (IF X Y Z) = Y. 5.3. The Propositional Functions Defining Axiom 6. (TRUEP X) = (EQUAL X T) Defining Axiom 7. (FALSEP X) = (EQUAL X F) Defining Axiom 8. (NOT P) = (IF P F T) Defining Axiom 9. (AND P Q) = (IF P (IF Q T F) F) Defining Axiom 10. (OR P Q) = (IF P T (IF Q T F)) Defining Axiom 11. (IMPLIES P Q) = (IF P (IF Q T F) T) Abbreviation. When we refer to a term t as a formula, one should read in place of t the formula t /= F. Example. The term (IMPLIES (AND (P X) (Q Y)) (R X Y)), if used where a formula is expected (e.g., in the allegation that it is a theorem), is to be read as (IMPLIES (AND (P X) (Q Y)) (R X Y)) /= F. Given the foregoing axioms and the rules of inference of propositional calculus and equality, the above formula can be shown equivalent to ((P X) /= F /\ (Q Y) /= F) -> (R X Y) /= F which we could abbreviate ((P X) /\ (Q Y)) -> (R X Y). Note. The definitional principle, to be discussed later, permits the user of the logic to add new defining axioms under admissibility requirements that ensure the unique satisfiability of the defining equation. The reader may wonder why we did not invoke the definitional principle to add the defining axioms above-explicitly eliminating the risk that they render the system inconsistent. In fact, we completely avoid use of the definitional principle in this presentation of the logic. There are two reasons. First, the definitional principle also adds an axiom (the non-SUBRP axiom) that connects the defined symbol to the interpreter for the logic-an axiom we do not wish to have for the primitives. Second, the admissibility requirements of the definitional principle are not always met in the development of the logic. 6. The Shell Principle and the Primitive Data Types @label(shells) Note. The shell principle permits the extension of the logic by the addition of a set of axioms that define a new data type. Under the conditions of admissibility described, the axioms added are guaranteed to preserve the consistency of the logic. The axioms are obtained by instantiating a set of axiom schemas described here. In order to describe the axiom schemas it is first necessary to establish several elaborate notational conventions. We then define the shell principle precisely. Then we invoke the shell principle to obtain the axioms for the natural numbers, the ordered pairs, the literal atoms, and the negative integers. 6.1. Conventions Terminology. We say t is the fn nest around b for s iff t and b are terms, fn is a function symbol of arity 2, s is a finite sequence of terms, and either (a) s is empty and t is b or (b) s is not empty and t is (fn t t ) where t 1 2 1 is the first element of s and t is the fn nest around b for the remaining 2 elements of s. When we write (fn t ... t ) o* b where a term is expected, it 1 n is an abbreviation for the fn nest around b for t , ..., t . 1 n Note. In the first edition used ``(fn t ... t )@b'' to denote what we now 1 n denote with ``(fn t ... t ) o* b.'' We changed from ``@'' to `` o* '' in the 1 n second edition because the ``@'' character is now permitted to occur in the extended syntax, in conjunction with backquote notation. Examples. The OR nest around F for A, B, and C is the term (OR A (OR B (OR C F))), which may also be written (OR A B C) o* F. Terminology. Each application of the shell principle introduces several ``new'' function symbols. The invocation explicitly names one symbol as the constructor and another as the recognizer. Zero or more other symbols are named as accessors, and one may be named as the base function symbol for that shell. Terminology. The constructor function symbols of a history h consists exactly of the constructor function symbols of applications of the shell principle in h. The recognizer function symbols of a history h is the union of {TRUEP FALSEP} with the set consisting exactly of the recognizer function symbols of the applications of the shell principle in h. The base function symbols of a history h is the union of {TRUE FALSE} with the set consisting exactly of the base function symbols of the applications of the shell principle in h for which a base function symbol was supplied. Terminology. We say r is the type of fn iff either (a) r is given as the type of fn in Table @ref(truep-table) or (b) fn is a constructor or base function symbol introduced in the same axiomatic act in which r was the recognizer function symbol. Table 6-1: @tag(truep-table) fn type of fn ------------------------------------------------------------------------------ TRUE TRUEP FALSE FALSEP ------------------------------------------------------------------------------ Terminology. A type restriction over a set of function symbols s is a nonempty finite sequence of symbols where the first symbol is either the word ONE-OF or NONE-OF and each of the remaining is an element of s. Terminology. A function symbol fn satisfies a type restriction (flg s ... 1 s ) iff either flg is ONE-OF and fn is among the s or flg is NONE-OF and fn n i is not among the s . i Terminology. We say t is the type restriction term for a type restriction (flg r ... r ) and a variable symbol v iff flg is ONE-OF and t is (OR (r v) 1 n 1 ... (r v)) o* F or flg is NONE-OF and t is (NOT (OR (r v) ... (r v)) o* n 1 n F). Examples. Let tr be (ONE-OF LISTP LITATOM). Then tr is a type restriction 1 1 over the set {NUMBERP LISTP LITATOM}. The function symbol LISTP satisfies tr 1 but the function symbol NUMBERP does not. The type restriction term for tr 1 and X1 is (OR (LISTP X1) (OR (LITATOM X1) F)). Let tr be (NONE-OF NUMBERP). 2 Then tr is a type restriction over the set {NUMBERP LISTP LITATOM}. The 2 function symbol LISTP satisfies tr but the function symbol NUMBERP does not. 2 The type restriction term for tr and X2 is (NOT (OR (NUMBERP X2) F)). 2 6.2. The Shell Principle Extension Principle. Shell Principle The axiomatic act Shell Definition. Add the shell const of n arguments with (optionally, base function base,) recognizer function r, accessor functions ac , ..., ac , 1 n type restrictions tr , ..., tr , and 1 n default functions dv , ..., dv , 1 n is admissible under the history h provided (a) const is a new function symbol of n arguments, (base is a new function symbol of no arguments, if a base function is supplied), r, ac , ..., ac 1 n are new function symbols of one argument, and all the above function symbols are distinct; (b) each tr is a type restriction over the recognizers i of h together with the symbol r; (c) for each i, dv is either base or one of the i base functions of h; and (d) for each i, if dv is base then r satisfies tr i i and otherwise the type of dv satisfies tr . i i If the tr are not specified, they should each be assumed to be (NONE-OF). i If admissible, the act adds the axioms shown below. In the special case that no base is supplied, T should be used for all occurrences of (r (base)) below, and F should be used for all terms of the form (EQUAL x (base)) below. (1) (OR (EQUAL (r X) T) (EQUAL (r X) F)) (2) (r (const X1 ... Xn)) (3) (r (base)) (4) (NOT (EQUAL (const X1 ... Xn) (base))) (5) (IMPLIES (AND (r X) (NOT (EQUAL X (base)))) (EQUAL (const (ac X) ... (ac X)) 1 n X)) For each i from 1 to n, the following formula (6) (IMPLIES trt i (EQUAL (ac (const X1 ... Xn)) i Xi)) where trt is the type restriction term for tr and Xi. i i For each i from 1 to n, the following formula (7) (IMPLIES (OR (NOT (r X)) (OR (EQUAL X (base)) (AND (NOT trt ) i (EQUAL X (const X1 ... Xn))))) (EQUAL (ac X) (dv ))) i i where trt is the type restriction term for tr and Xi. i i For each recognizer, r', in the recognizer functions of h the formula (8) (IMPLIES (r X) (NOT (r' X))) (9) (IMPLIES (r X) (EQUAL (COUNT X) (IF (EQUAL X (base)) (ZERO) (ADD1 (PLUS (COUNT (ac X)) 1 ... (COUNT (ac X))) o* (ZERO))))) n (10) The SUBRP axiom for each of the symbols const, base (if supplied), r, ac , ..., ac . 1 n We define the ``SUBRP axiom'' on page @pageref(subrp-axiom). @label(renumbering-of-shell-axioms) Note. In the first edition, the shell principle included two additional axioms, there labeled (8) and (9), which were in fact derivable from axiom (10) of the first edition. Their deletion from the second edition has caused renumbering of the subsequent axioms. 6.3. Natural Numbers-Axioms 12.n @label(ADD1) Shell Definition. Add the shell ADD1 of one argument with base function ZERO, recognizer function NUMBERP, accessor function SUB1, type restriction (ONE-OF NUMBERP), and default function ZERO. Note. In Appendix II we explicitly list the axioms added by this invocation of the shell principle. Each axiom has a number of the form 12.n, where n indicates the corresponding axiom schema of the shell principle. Axiom 13. (NUMBERP (COUNT X)) Axiom 14. (EQUAL (COUNT T) (ZERO)) Axiom 15. (EQUAL (COUNT F) (ZERO)) Defining Axiom 16. (ZEROP X) = (OR (EQUAL X (ZERO)) (NOT (NUMBERP X))) Defining Axiom 17. (FIX X) = (IF (NUMBERP X) X (ZERO)) Defining Axiom 18. (PLUS X Y) = (IF (ZEROP X) (FIX Y) (ADD1 (PLUS (SUB1 X) Y))) 6.4. Ordered Pairs-Axioms 19.n Shell Definition. Add the shell CONS of two arguments with recognizer function LISTP, accessor functions CAR and CDR, and default functions ZERO and ZERO. Notes. This invocation of the shell principle is, strictly speaking, inadmissible because there are axioms about CONS, CAR, and CDR in the SUBRP axioms added on behalf of the preceding shell. We ignore this inadmissibility and add the corresponding axioms anyway. In Appendix II we explicitly list the axioms added by this invocation of the shell principle. Each axiom has a number of the form 19.n, where n indicates the corresponding axiom schema of the shell principle. 6.5. Literal Atoms-Axioms 20.n @label(PACK) Shell Definition. Add the shell PACK of one argument with recognizer function LITATOM, accessor function UNPACK, and default function ZERO. Notes. This invocation of the shell principle is, strictly speaking, inadmissible because there are axioms about PACK in the SUBRP axioms added on behalf of the preceding shells. We ignore this inadmissibility and add the corresponding axioms anyway. In Appendix II we explicitly list the axioms added by this invocation of the shell principle. Each axiom has a number of the form 20.n, where n indicates the corresponding axiom schema of the shell principle. 6.6. Negative Integers-Axioms 21.n @label(MINUS) Shell Definition. Add the shell MINUS of one argument with recognizer function NEGATIVEP, accessor function NEGATIVE-GUTS, type restriction (ONE-OF NUMBERP), and default function ZERO. Note. In Appendix II we list explicitly the axioms added by this invocation of the shell principle. Each axiom has a number of the form 21.n, where n indicates the corresponding axiom schema of the shell principle. 7. Explicit Value Terms @label[explicit-values] Note. This section is technically an aside in the development of the logic. We define a particularly important class of terms in the logic, called the ``explicit value terms.'' Intuitively, the explicit value terms are the ``canonical constants'' in the logic. It is almost the case that every constant term-every variable-free term-can be mechanically reduced to a unique, equivalent explicit value. The only terms not so reducible are those involving (at some level in the definitional hierarchy) undefined functions, constrained functions, or calls of metafunctions such as V&C$. Thus, the explicit value terms are the terms upon which we can ``compute'' in the logic. They are the basis for our encoding of the terms as objects in the logic, and elaborate syntactic conventions are adopted in the extended syntax to permit their succinct expression. th Terminology. We say tr is the i type restriction for a constructor function th symbol fn of arity n iff 1 < = i < = n, and tr is the i type restriction specified in the axiomatic act in which fn was introduced. Examples. The first type restriction for ADD1 is (ONE-OF NUMBERP). The second type restriction for CONS is (NONE-OF). Terminology. We say t is an explicit value term in a history h iff t is a term and either (a) t is a call of a base function symbol in h, or (b) t is a call of a constructor function symbol fn in h on arguments a , ..., a and for 1 n each 1 < = i < = n, a is an explicit value term in h and the type of the top i th function symbol of a satisfies the i type restriction for the constructor i function fn. We frequently omit reference to the history h when it is obvious by context. Examples. The following are explicit value terms: (ADD1 (ADD1 (ZERO))) (CONS (PACK (ZERO)) (CONS (TRUE) (ADD1 (ZERO)))) The term (ADD1 X) is not an explicit value, since X is neither a call of a base function symbol nor a call of a constructor. The term (ADD1 (TRUE)) is not an explicit value, because the top function symbol of (TRUE) does not satisfy the type restriction, (ONE-OF NUMBERP), for the first argument of ADD1. 8. The Extended Syntax @label(extended-syntax) Note on the Second Edition. The second edition of this handbook extends the syntax of the first edition by adding - the Common Lisp convention for writing comments both with semicolon and with balanced occurrences of #| and |#; - more of Common Lisp's notation for writing integers, including binary, octal and hexadecimal notation, e.g., #B1000 as an abbreviation of 8; - Common Lisp's ``backquote'' notation, so that `(A ,@X B) is an abbreviation of (CONS 'A (APPEND X (CONS 'B NIL))); - COND and CASE, which permit the succinct abbreviations of commonly used nests of IF-expressions; - LIST*, which permits the succinct abbreviation of commonly used nests of CONS-expressions; and - LET, which permits the ``binding'' of ``local variables'' to values, permitting the succinct abbreviation of terms involving multiple occurrences of identical subterms. To explain the new integer notation and the backquote notation in a way that is (we believe) perfectly accurate and permits their use ``inside QUOTEs'' it was necessary to redevelop the foundation of the syntax as it was presented in the first edition. In particular, in the second edition we start with a class of structures larger than the first edition's ``s-expressions''-structures which include such utterances as `(,X). Because the foundation changed, virtually all of the first edition's Section 4.7 (pages 112-124), has changed. But the new syntax is strictly an extension of the old; every well-formed term in the old ``extended syntax'' is well-formed in the new and abbreviates the same formal term. So despite the relatively massive change to the description, the impact of the second edition is only to add and fully document the features noted above. In the first edition, Appendix I contained a formalization of the old syntax and abbreviation conventions; however, that formalization was developed independently of the informal description of the syntax (though the two were carefully scrutinized for consistency). In this edition we have undertaken in Appendix I to formalize not just the syntax and abbreviation conventions but this particular informal description of them. Thus, virtually every concept defined informally in this section (and in Section @ref(for-syntax)) is defined formally in Appendix I. Readers who are struggling with the problem of formalizing some system-and here we do not mean to limit ourselves just to formal languages-might benefit from a comparative study of this section and Appendix I. Here we describe in the mathematician's precise English a collection of concepts that we there render formally. Finally, to aid the new user in trying to understand our abbreviation conventions, we have included the machine readable text of Appendix I among our standard example files, as file examples/basic/parser.events. By noting this library one can execute the formal concepts. Comments in the file give some tips for making experimentation convenient. Notes. The extended syntax differs from the formal syntax only in that it permits certain abbreviations. That is, every term in the formal syntax is also a term in the extended syntax, but the extended syntax admits additional well-formed utterances that are understood to stand for certain formal terms. These abbreviations primarily concern notation for shell constants such as numbers, literal atoms, and lists. In addition, the extended syntax provides some abbreviations for commonly used function nests and for the general purpose bounded quantifier function FOR. We delay the presentation of the quantifier abbreviations until after we have axiomatized FOR (see section @ref(quant), page @pageref(quant)) but discuss all other aspects of the extended syntax in this section. We define the extended syntax in six steps. 1. We define a set of tree structures called ``token trees'' that includes the formal terms and some other structures as well. 2. We explain how token trees are displayed. 3. We identify three nested subsets of the token trees: the ``readable'' token trees, the ``s-expressions,'' and the ``well-formed'' s-expressions. 4. We define a mapping, called ``readmacro expansion,'' from the readable token trees to s-expressions. 5. We define a mapping, called ``translation,'' from the well-formed s-expressions to formal terms. 6. Finally, we make the convention that a readable token tree may be used as a term in the extended syntax provided its readmacro expansion is well-formed. Such a token tree abbreviates the translation of its readmacro expansion. For example, the token tree we display as (LIST* X #B010 '(0 . 1)) is readable. Its readmacro expansion is (LIST* X 2 (QUOTE (0 . 1))). This s-expression is well-formed. Its translation is the formal term: (CONS X (CONS (ADD1 (ADD1 (ZERO))) (CONS (ZERO) (ADD1 (ZERO))))). Thus, (LIST* X #B010 '(0 . 1)) may be used as a term in the extended syntax and abbreviates the CONS-nest above. The token tree (LIST* X ,A) is not readable, because it violates rules on the use of the ``the comma escape from backquote.'' The token tree (EQUAL `(,X . ,Y)) is readable. However, its readmacro expansion is (EQUAL (CONS X Y)), which is not well-formed, because the function symbol EQUAL requires two arguments. We apologize to readers expecting a definition of our syntax presented in a formal grammar (e.g., BNF). We have three reasons for proceeding in this fashion. First, despite the apparent simplicity of our syntax, it has extremely powerful and complicated provisions for describing structures. These provisions allow a natural embedding of the language into its constants, which facilitates the definition of a formal metatheory in the logic, as carried out in the final sections of this chapter. Thus, much of the verbiage here devoted to syntax can be thought of as devoted to the formal development of the metatheory. Second, we not only wish to specify the legal expressions in the extended syntax but also to map them to terms in the formal syntax. We think it unlikely that an accurate formal presentation of our syntax and its meaning would be any more clear than the informal but precise one offered here; furthermore, it would be much less accessible to most readers. Finally, this presentation is closely related to the actual implementation of the syntax in the Nqthm system. In our implementation the user types ``displayed token trees.'' These character strings are read by the Common Lisp read routine. The read routine causes an error if the token tree presented is not ``readable'' (e.g., uses a comma outside a backquote). Otherwise, the read routine ``expands'' the ``read macros'' (single quote, backquote, and #) and returns the s-expression as a Lisp object. It is only then that our theorem prover gets to inspect the object to determine if it is ``well-formed'' and, if so, what term it abbreviates. In Appendix I we not only formalize the concepts defined below but we provide a recursive descent parser that recognizes when a string of ASCII character codes is the display of a token tree. 8.1. Token Trees and Their Display Note. Our token trees are essentially the parse trees of Common Lisp s-expressions, except for the treatment of read macro characters (such as # and ') and certain atoms. For example, #B010, +2. and 2 are three distinct token trees. We define ``readmacro expansion'' so that these three trees expand into the same ``s-expression.'' We start the development with the definition of the # convention for writing down integers in various bases. Then we introduce the tokens involved in the single quote and backquote conventions. Finally, we define token trees and how to display them. Terminology. A character c is a base n digit character if and only if n < = 16 and c is among the first n characters in the sequence 0123456789ABCDEF. The position of c (using zero-based indexing) in the sequence is called its digit value. Note. When we define how we display ``token trees'' and the digit characters in them we will make it clear that case is irrelevant. Thus, while this definition makes it appear that only the upper case characters A-F are digit characters, we will effectively treat a-f as digit characters also. Example. The base 2 digits are 0 and 1. Their digit values are 0 and 1, respectively. Among the base 16 digits are A and F. The digit value of A is 10 and the digit value of F is 15. Terminology. A sequence of characters, s, is a base n digit sequence if and only if s is nonempty and every element of s is a base n digit character. The k base n value of a base n digit sequence c ...c c is the integer c n + ... + k 1 0 k 1 0 c n + c n , where c is the value of the digit c . 1 0 i i Example. 1011 is a base 2 digit sequence. Its base 2 value is the integer eleven. 1011 is also a base 8 digit sequence. Its base 8 value is the integer five hundred and twenty one. Terminology. A sequence of characters, s, is an optionally signed base n digit sequence if and only if s is either a base n digit sequence or s is nonempty, the first character of s is either a + or -, and the remaining characters constitute a base n digit sequence. If the first character of s is -, the base n signed value of s is the negative of the base n value of the constituent base n digit sequence. Otherwise, the base n signed value of s is the base n value of the constitutent base n digit sequence. Example. A2 and +A2 are both optionally signed base 16 digit sequences whose signed values (in decimal notation) are both 162. -A2 is also such a sequence; its signed value is -162. Terminology. A sequence of characters, s, is a #-sequence if and only if the length of s is at least three, the first character in s is #, the second character in s is in the set {B O X}, and the remaining characters in s constitute an optionally signed base n digit sequence, where n is 2, 8, or 16 according to whether the second character of s is B, O, or X, respectively. Note. Our convention of disregarding case will allow b, o, and x in the second character position of #-sequences. Terminology. Finally, a sequence of characters, s, is a numeric sequence if and only if one of the following is true: - s is an optionally signed base 10 digit sequence (in which case its numeric value is the base 10 signed value of s); - s is an optionally signed base 10 digit sequence with a dot character appended on the right (in which case its numeric value is the base 10 signed value of s with the dot removed); - s is a #-sequence (in which case its numeric value is the base n signed value of the sequence obtained from s by deleting the first two characters, where n is 2, 8, or 16 according to whether the second character of s is B, O, or X). Example. Table @ref(Number-table) shows some numeric sequences and their numeric values written in decimal notation. Table 8-1: @tag(number-table) sequence value ------------------------------------------------------------------------------ 123 123 -5. -5 #B1011 11 #O-123 -83 #Xfab 4011 ------------------------------------------------------------------------------ Terminology. The character sequence containing just the single quote (sometimes called ``single gritch'') character (') is called the single quote token. The character sequence containing just the backquote character (`) is called the backquote token. The character sequence containing just the dot character (.) is called the dot token. The character sequence containing just the comma character (,) is called the comma token. The character sequence containing just the comma character followed by the at-sign character (,@) is called the comma at-sign token. The character sequence containing just the comma character followed by the dot character (,.) is called the comma dot token. @label(word) Terminology. A sequence of characters, s, is a word if and only if s is a numeric sequence or s is nonempty and each character in s is a member of the set {A B C D E F G H I J K L M N O P Q R S T U V W X Y Z 0 1 2 3 4 5 6 7 8 9 $ ^ & * _ - + = ~ { } ? < >}. Note. All of our symbols are words, but the set of words is larger because it includes such non-symbols as *1*TRUE, 123, 1AF, and #B1011 that begin with non-alphabetic characters. Terminology. A token tree is one of the following: - an integer; - a word; - a nonempty sequence of token trees (a token tree of this kind is said to be an undotted token tree); - a sequence of length at least three whose second-to-last element is the dot token and all of whose other elements are token trees (a token tree of this kind is said to be a dotted token tree); or - a sequence of length two whose first element is one of the tokens specified below and whose second element is a token tree (called the constitutent token tree): * the single quote token (such a token tree is said to be a single quote token tree), * the backquote token (a backquote token tree), * the comma token (a comma escape token tree), or * the comma at-sign or comma dot tokens (such token trees are said to be splice escape token trees). Note. In order to explain how token trees are displayed we must first introduce the notion of ``comments.'' Following Common Lisp, we permit both ``semicolon comments'' and ``number sign comments.'' The latter are, roughly speaking, text delimited by balanced occurrences of #| and |#. To define this notion precisely, we must introduce the terminology to let us talk about #| and |# clearly. Terminology. The integer i is a #|-occurrence in the character string s of th length n iff 0 < = i < = n-2, the i (0-based) character of s is the number st sign character (#) and the i+1 character of s is the vertical bar character, |. We define what it is for i to be a |#-occurrence in strict analogy. A |#-occurrence, j, is strictly to the right of a #|-occurrence, i, iff j>i+1. Finally, if i is a #|-occurrence in s and j is a |#-occurrence in s that is strictly to the right, then the substring of s delimited by i and j is the nd st substring of s that begins with the i+2 character and ends with the j-1 character. Examples. Consider the string #|Comment|#. The string has eleven characters in it. The only #|-occurrence is 0. The only |#-occurrence is 9. The substring delimited by these occurrences is Comment. In the string #||# the only #|-occurrence is 0 and the only |#-occurrence is 2, which is strictly to the right of the former. The substring delimited by these two occurrences is the empty string. Terminology. A string of characters, s, has balanced number signs iff all the #|- and |#-occurrences can be paired (i.e., put into 1:1 correspondence) so that every #| has its corresponding |# strictly to its right and the text delimited by the paired occurrences has balanced number signs. Examples. The string Comment has balanced number signs because there are no #|- or |#-occurrences. The string code #|Comment|# and code also has balanced number signs. The following string does not have balanced number signs: #|code #|Comment|# and code. Terminology. A string of characters, s, is a #-comment iff s is obtained from a string, s', that has balanced number signs, by adding a number sign character immediately followed by a vertical bar (#|) to the left-hand end and a vertical bar immediately followed by a number sign (|#) to the right-hand end. Notes. Generally speaking, any string of characters not including #| or |# can be made into a #-comment by surrounding the string with #| and |#. Such comments will be allowed in certain positions in the display of terms. Roughly speaking, the recognition that a string is a comment is license to ignore the string; that is the whole point of comments. Comments can be added to the display of a term without changing the term displayed. We are more specific in a moment. The display of such a commented term can itself be turned into a #-comment by again surrounding it with #| and |#. If we did not insist on ``balancing number signs'' the attempt to ``comment out'' a term could produce ill-formed results because the ``opening'' #| would be ``closed'' by the first |# encountered in the term's comments and the rest of the term would not be part of the comment. The question of where #-comments are allowed is difficult to answer, but it is answered below. The problem is that in Common Lisp (whose read routine we actually use to parse terms) the number sign character does not automatically terminate the parsing of a lexeme. Thus, (H #|text|# X) reads as a list containing the lexeme H followed by the lexeme X, but (H#|text|# X) reads as the list containing the lexeme H#text# followed by the lexeme X. So some ``white space'' must appear after H and before the number sign in order for the number sign to be read as the beginning of a comment. As for the end of the comment, the |# closes the comment no matter what follows. Thus, (H #|text|#X) is also read as H followed by X, even though there is no space after the second number sign. The naive reader might conclude that #| must always be preceded by white space and |# may optionally be followed by white space. Unfortunately, the rule is a little more complicated. The display (FN (H X)#|text|# X) is read as (FN (H X) X). The reason is that the close parenthesis in (H X) is a ``lexeme terminating character'' that terminates the lexeme before it, i.e., X, and constitutes a lexeme in itself. Thus, the #| is recognized as beginning a comment. We now explain this precisely. Terminology. The white space characters are defined to be space, tab, and newline (i.e., carriage return). The lexeme terminating characters are defined to be semicolon, open parenthesis, close parenthesis, single quote mark, backquote mark, and comma. (Note that # is not a lexeme terminator!) The union of the white space characters and the lexeme terminating characters is called the break characters. Terminology. A comment is any of the following: - a (possibly empty) sequence of white space characters, - a #-comment, - a sequence of characters that starts with a semicolon, ends with a newline, and contains no other newlines, or - the concatenation of two comments. A comment is said to be a separating comment if it is nonempty and its first character is either a white space character or a semicolon. Example. Thus, ;This is a comment. is a separating comment. The string #|And this is a comment.|# is a comment but not a separating comment. It can be made into a separating comment by adding a space before the first #. The following is a display of a separating comment (since it starts with a semicolon) that illustrates that comments may be strung together: ; This is a long comment. ; It spans several lines and #|Contains both semicolon and number sign comments. In addition, immediately after the following number sign is a white space comment.|# ; And here's another ;semicolon comment. Terminology. Suppose s and s are non-empty character strings. Then 1 2 suitable separation between s and s is any comment with the following 1 2 properties. Let c be the last character in s , and let c be the first 1 1 2 character in s . 2 - If c is a break character, suitable separation is any comment. 1 - If c is not a break character but c is a break character, suitable 1 2 separation is either the empty comment or any separating comment. - If neither c nor c is a break character, suitable separation is 1 2 any separating comment. When we use the phrase ``suitable separation'' it is always in a context in which s and s are implicit. 1 2 Terminology. A suitable trailer after a string s is any suitable separation between s and a string beginning with a break character. That is, a suitable trailer may be any comment if the last character of s is a break character and otherwise may be either an empty comment or a separating comment. Examples. We use suitable separations and trailers to separate the lexemes in our displays of terms in the extended syntax. For example, in (FN X) the lexeme FN is separated from the lexeme X by the separating comment consisting of a single space. Any separating comment is allowed in the extended syntax. Thus, (FN;Comment X) is an acceptable display. The empty string is not a separating comment. Thus, (FNX) is an unacceptable display. Similarly, because #|Comment|# is not a separating comment, (FN#|Comment|#X) is unacceptable. On the other hand, by adding a space to the front of the #-comment above we obtain a separating comment and thus (FN #|Comment|#X) is an acceptable display. Now consider (FN (H X) Y). Because the last character of FN is not a break character but open parenthesis is a break character, suitable separation between displays of FN and (H X) is either the empty string or a separating comment. Thus, the first four of the following five displays will be acceptable. The last will not, because the comment used is not a separating comment or the empty comment. (FN(H X) Y) ; the empty comment (FN (H X) Y) ; a white space comment (FN;text ; a semicolon comment (H X) Y) (FN #|text|# (H X) Y) ; a separating #-comment (FN#|text|# (H X) Y) ; unacceptable! Any comment may be used to separate (H X) and Y, because the close parenthesis character is a break character. Thus, (FN(H X)Y) will be an allowed display, as will (FN(H X)#|text|#Y). Terminology. To display a token tree that is an integer or word, we write down a comment, a decimal representation of the integer or the characters in the word, followed by a suitable trailer. Upper case characters in a word may be displayed in lower case. To display a dotted or undotted token tree consisting of the elements t , ..., t , where t may or may not be the dot 1 n n-1 token, we write down a comment, an open parenthesis, suitable separation, a display of t , suitable separation, a display of t , suitable separation, ..., 1 2 a display of t , suitable separation, a close parenthesis, and a comment, n where we display the dot token as though it were a word. All other token trees consist of a token and a constituent token tree. To display them we write down a comment, the characters in the token, a comment, a display of the constituent token tree, and a suitable trailer. Note. What token tree displays as 123? Unfortunately, there are two: the tree consisting of the integer 123 and the tree consisting of the numeric sequence 123. These two trees readmacro expand to the same tree and since readmacro expansion is involved in our abbreviation convention, it is irrelevant which of the two trees was actually displayed. Example. Below we show some (displays of) token trees: (EQUAL X ;Comments may (QUOTE (A B . C))) ;be included (EQUAL X (QUOTE (A B . C))) (equal x (quote (a b . c))) (QUOTE (A . B)) '(A . B) `(A ,X ,@(STRIP-CARS Y) B) ((1AB B**3 C) 12R45 (ADD1)) The first, second and third are different displays of the same token tree-the only difference between them is the comments used and the case of the characters. The fourth and fifth are displays of two different token trees, both of length two with the same second element, (A . B), but one having the word QUOTE as its first element and the other having the single quote token as its first element. Note the difference in the way they are displayed. It will turn out that these two different token trees readmacro expand to the same s-expression. The sixth display shows how a backquote token tree containing two escapes may be displayed. Once we have defined readmacro expansion and translation it will be clear that all of the token trees except the last abbreviate terms. Notes. Because of our convention in this book of using lower case typewriter font words as metavariables, we will refrain from using lower case when displaying token trees. Thus, if fn is understood to be any function symbol of two arguments, then (PLUS X Y) is to be understood to be ``of the form'' of the token tree we display as (fn X Y) while it is not ``of the form'' of the tree we display as (FN X Y). The reader may wonder why we permit token trees to be displayed in lower case if we never so display them. The point is that we never so display them in this book. But in other papers in which formulas are displayed, users frequently find lowercase characters more attractive. Furthermore, our implementation of Nqthm inherits from the host Lisp system the default action of raising lower case characters to upper case characters when reading from the user's terminal or files. (Special action has to be taken to prevent this.) Thus, many users type formulas in lower case. Since metavariables are not part of the system, this presents no ambiguity. In Appendix I we define the inverse of the display process: a parser that determines whether a list of ASCII character codes is a display of a token tree and, if so, what token tree was displayed (up to the integer/numeric sequence ambiguity which is resolved by always adopting the numeric sequence interpretation). The parser is defined in two passes, one that breaks the list of character codes into lexemes and a second which attempts to construct a token tree from the lexemes. 8.2. Readable Token Trees, S-Expressions and Readmacro Expansion Note. The token tree displayed as `(,,X) is problematic because it contains a doubly-nested backquote escape in a singly nested backquote tree. The token trees displayed as `,@X and `(1 . ,@X) are problematic because they use the ,@ notation in ``non-element positions.'' We make precise these requirements by defining the notion of ``readable'' token trees for depth n and then restricting our attention later to the readable token trees for depth 0. Terminology. A token tree s is readable from depth n iff one of the following holds: - s is an integer or word; - s is an undotted token tree and each element of s is readable from n; - s is a dotted token tree and each element of s (other than the dot token) is readable from n and the last element of s is not a splice escape tree; - s is a single quote token tree and the constituent token tree is readable from n; - s is a backquote token tree and the constituent token tree is readable from n+1 and is not a splice escape tree; or - s is a comma escape or splice escape token tree, n>0, and the constituent token tree is readable from n-1. Example. The token tree (A ,X B) is not readable from depth 0 but is readable from depth 1. Thus, `(A ,X B) is readable from depth 0. The expressions `,@X and (A . ,@X) are not readable from any depth. Terminology. An s-expression is a token tree containing no numeric sequences or tokens other than the dot token. Terminology. If s is a token tree readable from depth 0, then its readmacro expansion is the s-expression obtained by the following four successive transformations. - Replace every numeric sequence by its numeric value. - Replace every single quote token by the word QUOTE. - Replace every backquote token tree, `x, by the ``backquote expansion'' of x (see below), replacing innermost trees first. - At this point the transformed tree contains no tokens other than, possibly, the dot token. Replace every subtree of s of the form, (x x ... x . (y ... y )), by (x x ... x y ... y ) and every 1 2 k 1 n 1 2 k 1 n subtree of the form (x x ... x . NIL) by (x x ... x ). That 1 2 k 1 2 k is, a subtree should be replaced if it is a dotted token tree and its last element is either a dotted or undotted token tree or the word NIL. Let x be such a tree and let y be its last element. If y is a dotted or undotted token tree, then x is replaced by the concatenation of y onto the right-hand end of the sequence obtained from x by deleting the dot and the last element. If y is the word NIL then x is replaced by the sequence obtained from x by deleting the dot and the last element. Examples. The readmacro expansion of (A B . '(#B100 . C)) proceeds in the following steps. First, the numeric sequence is replaced by its integer value, producing (A B . '(4 . C)). Second, the single quote token tree is replaced by a QUOTE tree, (A B . (QUOTE (4 . C))). Since there are no backquote tokens in the tree, that step of readmacro expansion is irrelevant here. Finally we consider the dotted token trees. The innermost one is not of the form that is replaced. The outermost one is replaceable. The result is (A B QUOTE (4 . C)). The readmacro expansion of (PLUS #B100 (SUM '(1 2 3))) is (PLUS 4 (SUM (QUOTE (1 2 3)))). Note that the ambiguity concerning the display of integers and numeric sequences makes it impossible to uniquely determine the token tree initially displayed. For example, we do not know if it contained the integer two or the numeric sequence 2. However, the second tree displayed is the readmacro expansion of the first. As such, it is an s-expression and contains no numeric sequences. Thus, the second token tree is uniquely determined by the display and the fact that it is known to be an s-expression. @label(backquote-expansion) Note. We now define ``backquote expansion.'' It is via this process that `(,X ,Y . ,Z) is readmacro expanded into (CONS X (CONS Y Z)), for example. Our interpretation of backquote is consistent with the Common Lisp interpretation [8, 9]. However, Common Lisp does not specify what s-expression is built by backquote; instead it specifies what the value of the s-expression must be. Different implementations of Common Lisp actually produce different readmacro expansions. For example, in one Common Lisp, `(,X) might be (CONS X NIL) and in another it might be (LIST X). The values of these expressions are the same. But consider what happens when a backquoted form is quoted, e.g., '`(,X). In one of the two hypothetical Lisps mentioned above, this string reads as the constant '(CONS X NIL), while in the other it reads as '(LIST X). This is intolerable in our setting since it would mean that the token tree (EQUAL (CAR '`(,X)) 'CONS) might read as a theorem in one Common Lisp and read as a non-theorem in another. We therefore have to choose a particular readmacro expansion of backquote (consistent with Common Lisp). We document it here. It is implemented by suitable changes to the Lisp readtable in Nqthm.< Actually, we do not force our implementation of backquote onto the Nqthm user typing Lisp at the top-level. See BACKQUOTE-SETTING in the Reference Guide, page @pageref(backquote-setting).> Terminology. If s is a token tree readable from some depth n and s contains no numeric sequences, single quote tokens or backquote tokens, then its backquote expansion is the token tree defined as follows. - If s is an integer or a word, then (QUOTE s) is its backquote expansion. - If s is a comma escape token tree, ,x, or a splice escape token tree, ,@x or ,.x, then x is its backquote expansion. - If s is an undotted token tree or a dotted token tree, then its backquote expansion is the ``backquote-list expansion'' of s (see below). Terminology. We now define the backquote-list expansion for a dotted or undotted token tree, s, that is readable from some depth n and contains no numeric sequences, single quote tokens, or backquote tokens. Let x be the backquote expansion of the first element of s. Let y be as defined by cases below. Then the backquote-list expansion of s is either (APPEND x y) or (CONS x y), according to whether the first element of s is a splice escape token tree or not. The definition of y is by cases: - If s is a token tree of length 1, then y is (QUOTE NIL). - If s is a dotted token tree of length 3, then y is the backquote expansion of the last element of s. - If s is any other dotted or undotted token tree, then y is the backquote-list expansion of the token tree obtained by removing the first element from s. Examples. To illustrate the first case above, where s is an undotted token tree of length 1, consider the backquote-list expansion of (A). The result is (CONS (QUOTE A) (QUOTE NIL)) because the backquote expansion of A is (QUOTE A). The second case is illustrated by (B . ,Z). Its backquote-list expansion is (CONS (QUOTE B) Z). We combine these to illustrate the third case. The backquote-list expansion of ((A) B . ,Z) is (CONS (CONS (QUOTE A) (QUOTE NIL)) (CONS (QUOTE B) Z)). The backquote-list expansion of (A ,@Z B) is (CONS (QUOTE A) (APPEND Z (CONS (QUOTE B) (QUOTE NIL)))). Since the readmacro expansion of `(A) is just the backquote expansion of (A), which, in turn, is the backquote-list expansion of (A), we see that the readmacro expansion of `(A) is (CONS (QUOTE A) (QUOTE NIL)). In Table @ref(backquote-table) we show some other examples of the readmacro expansion of backquote trees. Table 8-2: @tag(backquote-table) token tree readmacro expansion ------------------------------------------------------------------------------ `(X ,X ,@X) (CONS (QUOTE X) (CONS X (APPEND X (QUOTE NIL)))) `((A . ,X) (CONS (CONS (QUOTE A) X) (B . ,Y) (CONS (CONS (QUOTE B) Y) . ,REST) REST)) ``(,,X) (CONS (QUOTE CONS) (CONS X (CONS (CONS (QUOTE QUOTE) (CONS (QUOTE NIL) (QUOTE NIL))) (QUOTE NIL)))) ------------------------------------------------------------------------------ We can explain the last example of Table @ref(backquote-table). The readmacro expansion of ``(,,X) proceeds by first replacing the innermost backquote tree by its backquote expansion. So let us consider the backquote expansion of `(,,X). We might first observe that while this tree is not readable from depth 0, its backquote expansion is nevertheless well defined. Indeed, its backquote expansion is the token tree (CONS ,X (QUOTE NIL)) because the backquote expansion of ,,X is ,X. So replacing the constituent token tree, `(,,X), of ``(,,X) by its backquote expansion produces `(CONS ,X (QUOTE NIL)). It is easy to check that the readmacro expansion of this tree is as shown in the table. Observe that backquote expansion does not always yield an s-expression: the backquote expansion of ,,X is ,X. However, the backquote expansion of a token tree readable from depth 0 produces an s-expression because each escape token tree is embedded in enough backquotes to ensure that all the escape and backquote tokens are eliminated. 8.3. Some Preliminary Terminology @label[prelim-term Note. We have described how readmacro expansion transforms readable token trees into s-expressions. We now turn to the identification of a subset of the s-expressions, called ``well-formed'' s-expressions and the formal terms they abbreviate. We need a few preliminary concepts first. Terminology. The NUMBERP corresponding to a nonnegative integer n is the term (ZERO) if n is 0, and otherwise is the term (ADD1 t), where t is the NUMBERP corresponding to n-1. The NEGATIVEP corresponding to a negative integer n is the term (MINUS t), where t is the NUMBERP corresponding to -n. Examples. The NUMBERP corresponding to 2 is (ADD1 (ADD1 (ZERO))). The NEGATIVEP corresponding to -1 is (MINUS (ADD1 (ZERO))). Terminology. If fn is a CAR/CDR symbol, we call the sequence of characters in fn starting with the second and concluding with the next to last the A/D sequence of fn. Terminology. If s is a character sequence of A's and D's, the CAR/CDR nest for s around a term b is the term t defined as follows. If s is empty, t is b. Otherwise, s consists of either an A or D followed by a sequence s'. Let t' be the CAR/CDR nest for s' around b. Then t is (CAR t') or (CDR t'), according to whether the first character of s is A or D. Example. The symbol CADDAAR is a CAR/CDR symbol. Its A/D sequence is the sequence ADDAA. The CAR/CDR nest for ADDAA around L is (CAR (CDR (CDR (CAR (CAR L))))). Terminology. We say a term e is the explosion of a sequence of ASCII characters, s, iff either (a) s is empty and e is (ZERO) or (b) s is a character c followed by some sequence s' and e is (CONS i e') where i is the NUMBERP corresponding to the ASCII code for c and e' is the explosion of s'. Note. See the definition of ASCII-TABLE in Appendix I for the codes of the printing ASCII characters. Example. The ASCII codes for the characters A, B, and C are 65, 66, and 67 respectively. Let t , t , and t denote, respectively, the NUMBERPs 65 66 67 corresponding to 65, 66, and 67. For example, t here denotes a nest of 65 ADD1s 65 deep with a (ZERO) at the bottom. Then the explosion of ABC is the formal term (CONS t (CONS t (CONS t (ZERO)))). 65 66 67 Terminology. We say the term e is the LITATOM corresponding to a symbol s iff e is the term (PACK e') where e' is the explosion of s. Example. The LITATOM corresponding to the symbol ABC is (PACK (CONS t (CONS t (CONS t (ZERO))))), 65 66 67 where t , t , and t are as in the last example. 65 66 67 8.4. Well-Formed S-Expressions and Their Translations Notes. The terminology we have developed is sufficient for defining what it means for an s-expression to be ``well-formed'' and what its ``translation'' is, for all s-expressions except those employing QUOTE or abbreviated FORs. Rather than define the concepts necessary to pin down these conventions, we now jump ahead in our development of the syntax and define ``well-formed'' and ``translation.'' Such a presentation here necessarily involves undefined concepts-the notions of well-formedness and translation of both QUOTE and FOR expressions. However, by providing the definition at this point in the development we can use some s-expressions to illustrate and motivate the discussion of the more elaborate notations. Terminology. Below we define two concepts: what it means for an s-expression x to be a well-formed term in the extended syntax and, for well-formed s-expressions, what is the translation into a term in the formal syntax. These definitions are made implicitly with respect to a history because QUOTE notation permits the abbreviation of explicit values, a concept which, recall, is sensitive to the history. Our style of definition is to consider any s-expression x and announce whether it is well-formed or not and if so, what its translation is. @label(well-formed) - If x is an integer, it is well-formed and its translation is the explicit value term denoted by x (see page @pageref(quote- notation)). - If x is a symbol then * If x is T, it is well-formed and its translation is the formal term (TRUE). * If x is F, it is well-formed and its translation is the formal term (FALSE). * If x is NIL, it is well-formed and its translation is the explicit value term denoted by NIL (see page @pageref(quote- notation)). * If x is any other symbol, it is well-formed and its translation is the formal term x. - If x is a dotted s-expression, it is not well-formed. - If the first element of x is the symbol QUOTE, then x is well-formed iff it is of the form (QUOTE e) where e is an explicit value descriptor (see page @pageref(quote-notation)). If well-formed, the translation of x is the explicit value term denoted by e (see page @pageref(quote-notation)). - If the first element of x is the symbol COND, then the well-formedness of x and its translation are defined by cases as follows. * If x is of the form (COND (T v)), then it is well-formed iff v is well-formed. If x is well-formed, the translation of x is the translation of v. * If x is of the form (COND (w v) x ... x ), where n>0, then x 1 n is well-formed iff w is not T and w, v and (COND x ... x ) are 1 n well-formed. If x is well-formed, let test, val, and rest be, respectively, the translations of w, v, and (COND x ... x ). 1 n Then the translation of x is (IF test val rest). * Otherwise, x is not well-formed. - If the first element of x is the symbol CASE, then the well-formedness of x and its translation are defined by cases as follows. * If x is of the form (CASE w (OTHERWISE v)), then x is well-formed iff w and v are well-formed. If x is well-formed, the translation of x is the translation of v. * If x is of the form (CASE w (e v) x ... x ), where n>0, then 1 n x is well-formed iff no x is of the form (e x' ) and in i i addition w, (QUOTE e), v, and (CASE w x ... x ) are 1 n well-formed. If x is well-formed, then let key, obj, val, and rest be, respectively, the translations of w, (QUOTE e), v, and (CASE w x ... x ). Then the translation of x is (IF (EQUAL 1 n key obj) val rest). * Otherwise, x is not well-formed. - If the first element of x is the symbol LET, then x is well-formed iff x is of the form (LET ((w v ) ... (w v )) y), the w , v and 1 1 n n i i y are well-formed, the translation of each w is a symbol and the i translation of w is different from that of w when i is different i j from j. If x is well-formed, let var be the translation of w , let i i t be the translation of v and let body be the translation of y. i i Let s be the substitution that replaces var by t , i.e., {< var , i i 1 t > ... < var , t >}. Then the translation of x is body/s. 1 n n - Otherwise, x is of the form (fn x ... x ), where fn is a symbol 1 n other than QUOTE, COND, CASE, or LET, and each x is an i s-expression. If some x is not well-formed, then x is not i well-formed. Otherwise, let t be the translation of x below: i i * If fn is in the set {NIL T F}, x is not well-formed. * If fn is the symbol LIST then x is well-formed and its translation is the CONS nest around the translation of NIL for t , ..., t . 1 n * If fn is the symbol LIST* then x is well-formed iff n >= 1. If x is well-formed, its translation is the CONS nest around t n for t , ..., t . 1 n-1 * If fn is a CAR/CDR symbol, then x is well-formed iff n is 1 and, if well-formed, its translation is the CAR/CDR nest around t for the A/D sequence of fn. 1 * If fn is a function symbol of arity n, then x is well-formed and its translation is the formal term (fn t ... t ). 1 n * If fn is the symbol FOR and n is 5 or 7, then x is well-formed iff x is an abbreviated FOR (see page @pageref[FOR-syntax]). If well-formed, the translation of x is the FOR expression denoted by x (see page @pageref[FOR-syntax]). * If fn is in the set {AND OR PLUS TIMES} and n>2, then x is well-formed and its translation is the fn nest around t for n t , ..., t . 1 n-1 * Otherwise, x is not well-formed. Examples. Table @ref(trans-table) shows well-formed s-expressions on the left and their translations to formal terms on the right. Table 8-3: @tag(trans-table) s-expression translation ------------------------------------------------------------------------------ T (TRUE) 2 (ADD1 (ADD1 (ZERO))) (COND (P X) (IF P X (IF Q Y Z)) (Q Y) (T Z)) (LIST* A B C) (CONS A (CONS B C)) (CADR X) (CAR (CDR X)) (PLUS I J K) (PLUS I (PLUS J K)) ------------------------------------------------------------------------------ Certain formal terms, such as the translation of NIL, are exceedingly painful to write down because they contain deep nests of ADD1s. Table @ref(trans2-table) also contains translations, except this time the right-hand column is, technically, not a formal term but rather another well-formed s-expression with the same translation. In particular, in Table @ref(trans2-table) we use decimal notation in the right-hand column, but otherwise confine ourselves to formal syntax. Table 8-4: @tag(trans2-table) s-expression with s-expression same translation ------------------------------------------------------------------------------ NIL (PACK (CONS 78 (CONS 73 (CONS 76 0)))) (LIST 1 2 3) (CONS 1 ;first element (CONS 2 ;second element (CONS 3 ;third element (PACK ;NIL (CONS 78 (CONS 73 (CONS 76 0))))))) ------------------------------------------------------------------------------ 8.5. QUOTE Notation @label(quote-notation) Notes and Example. In this subsection we define what we mean by an ``explicit value descriptor'' and the ``explicit value denoted'' by such a descriptor. These are the concepts used to define the well-formedness and meaning of s-expressions of the form (QUOTE e). Each explicit value term can be written in QUOTE notation. That is, for each explicit value term t there is exactly one s-expression e such that the s-expression (QUOTE e) is well-formed and translates to t. We call e the ``explicit value descriptor'' of t. For example, consider the s-expression (CONS 1 (CONS (PACK (CONS 65 (CONS 66 (CONS 67 0)))) (CONS 2 3))). This s-expression is well-formed and translates to an explicit value- indeed, except for the use of decimal notation, this s-expression is an explicit value. Call that explicit value term t. The explicit value descriptor for t is the s-expression (1 ABC 2 . 3). Thus, the translation of (QUOTE (1 ABC 2 . 3)) is t. Our QUOTE notation is derived from the Lisp notation for data structures composed of numbers, symbols, and ordered pairs, but is complicated by the need to denote structures containing user-defined shell constants. That is, after the theory has been extended by the addition of a new shell, it is possible to build constants containing both primitive shells and user-defined ones, e.g., lists of stacks. Unlike Lisp's QUOTE notation, the notation described here permits such constants to be written down, via an ``escape'' mechanism. Following the precedent set for well-formedness and translation, we proceed in a top-down fashion to define what we mean by an ``explicit value descriptor'' and its ``denoted explicit value'' without first defining the terminology to discuss the ``escape'' mechanism. Immediately following the definition below we illustrate the use of QUOTE notation on primitive shell constants, e.g., lists, numbers, and literal atoms. We define the escape mechanism for user-declared shells in the next subsection. Terminology. Below we define two concepts: what it is for an s-expression e to be an explicit value descriptor and, for explicit value descriptors, what is the denoted explicit value term. These definitions are made with respect to a history which is used implicitly below. Our style of definition is to consider any s-expression e and announce whether it is an explicit value descriptor or not and if so, what its denoted explicit value term is. - If e is an integer, it is an explicit value descriptor and the explicit value term it denotes is the NEGATIVEP or NUMBERP corresponding to e, according to whether e is negative or not. - If e is a word, then * If e is the word *1*TRUE, e is an explicit value descriptor and denotes the explicit value (TRUE). * If e is the word *1*FALSE, e is an explicit value descriptor and denotes the explicit value (FALSE). * If e is a symbol, e is an explicit value descriptor and denotes the LITATOM corresponding to e. * Otherwise, e is not an explicit value descriptor. - If the first element of e is the word *1*QUOTE, e is an explicit value descriptor iff it is an explicit value escape descriptor (see the next subsection). If so, it has the form (*1*QUOTE fn e ... 1 e ), where fn is a constructor or base function symbol of arity n n and each e is an explicit value descriptor denoting an explicit i value t . The explicit value denoted by e is then (fn t ... t ). i 1 n (That this is, indeed, an explicit value is assured by the definition of ``explicit value escape descriptor.'') - If e is a dotted s-expression of length 3, i.e., (e . e ), then e 1 2 is an explicit value descriptor iff each e is an explicit value i descriptor. If so, let t be the explicit value denoted by e . i i Then the explicit value denoted by e is (CONS t t ). 1 2 - If e is an s-expression of length 1, i.e., (e ), e is an explicit 1 value descriptor iff e is an explicit value descriptor. If so, let 1 t be the explicit value denoted by e and let nil be the explicit 1 1 value denoted by NIL. Then the explicit value denoted by e is (CONS t nil). 1 - Otherwise, either e is a dotted s-expression of length greater than 3 or e is a non-dotted s-expression of length greater than 1. Let e be the first element of e and let e be the sequence consisting 1 2 of the remaining elements of e. Observe that e and e are both 1 2 s-expressions. e is an explicit value descriptor iff each e is an i explicit value descriptor. If so, let t be the explicit value i denoted by e . Then the explicit value denoted by e is (CONS t i 1 t ). 2 Examples. Table @ref(quote-table) illustrates the QUOTE notation. The two columns contain token trees rather than s-expressions simply to save space-we write 'x in place of the s-expression (QUOTE x). Each token tree is readable and readmacro expands to a well-formed s-expression. The s-expressions of the left-hand column are all examples of QUOTE forms. The s-expressions of the right-hand column use QUOTE only to represent literal atoms. Corresponding s-expressions in the two columns have identical translations. Table 8-5: @tag(quote-table) token tree for token tree for s-expression in s-expression with QUOTE notation same translation ------------------------------------------------------------------------------ '123 123 'ABC (PACK '(65 66 67 . 0)) '(65 66 67 . 0) (CONS 65 (CONS 66 (CONS 67 0))) '(PLUS I J) (CONS 'PLUS (CONS 'I (CONS 'J 'NIL))) '((I . 2) (J . 3)) (LIST (CONS 'I 2) (CONS 'J 3)) '((A . *1*TRUE) (LIST (CONS 'A (TRUE)) (B . T)) (CONS 'B (PACK (CONS 84 0)))) ------------------------------------------------------------------------------ Note. Of particular note is the possible confusion of the meaning of the symbol T (and, symmetrically, of F) in s-expressions. If T is used ``outside a QUOTE'' it denotes (TRUE). If T is used ``inside a QUOTE'' it denotes the literal atom whose ``print name'' is the single character T. To include (TRUE) among the elements of a QUOTEd list, the non-symbol *1*TRUE should be written. If the s-expression (QUOTE ABC) is used as a term it denotes the term also denoted by (PACK (QUOTE (65 66 67 . 0))). However, if the s-expression (QUOTE ABC) is used ``inside a QUOTE,'' i.e., as an explicit value descriptor as in the term (QUOTE (QUOTE ABC)), it denotes the term also denoted by (LIST (QUOTE QUOTE) (QUOTE ABC)). The translation of (QUOTE ABC) is a LITATOM constant; the translation of (QUOTE (QUOTE ABC)) is a LISTP constant. Here is another example illustrating the subtlety of the situation. The innocent reader may have, by now, adopted the convention that whenever (CADR X) is seen, (CAR (CDR X)) is used in its place. This is incorrect. When (CADR X) is used as a term, i.e., when we are interested in its translation into a formal term, it denotes (CAR (CDR X)). But if (CADR X) is ``inside a QUOTE'' it is not being used as a term but rather as an explicit value descriptor. In particular, the translation of (QUOTE (CADR X)) is a list whose first element is the LITATOM denoted by the term (QUOTE CADR), not a list whose first element is the LITATOM denoted by (QUOTE CAR). While the translations of (CADR X) and (CAR (CDR X)) are the same, the translations of (QUOTE (CADR X)) and (QUOTE (CAR (CDR X))) are different. Similarly the translation of (QUOTE 1) is not the same as that of (QUOTE (ADD1 (ZERO))); the first is a NUMBERP, the second is a LISTP. 8.6. *1*QUOTE Escape Mechanism for User Shells Notes and Example. In this section we describe how to use the *1*QUOTE convention to write down user-declared shell constants. In particular, we define the notion of the ``explicit value escape descriptor'' used above. Roughly speaking, an explicit value escape descriptor is an s-expression of the form (*1*QUOTE fn e ... e ) where fn is a shell constructor or base 1 n function and the e are explicit value descriptors denoting its arguments. i Thus, if PUSH is a shell constructor of two arguments and EMPTY is the corresponding base function then (*1*QUOTE PUSH 3 (*1*QUOTE EMPTY)) is an explicit value escape descriptor, and hence an explicit value descriptor, that denotes the constant term also denoted by (PUSH 3 (EMPTY)). We restrict the legal escape descriptors so that the mechanism cannot be used to write down alternative representations of constants that can be written in the conventional QUOTE notation. For example, (*1*QUOTE CONS 1 2) is not an explicit value escape descriptor because if it were it would be an alternative representation of (CONS 1 2). Furthermore, we must restrict the escape descriptors so that they indeed denote explicit values. Is (PUSH 3 (EMPTY)) an explicit value? The answer depends upon the type restrictions for the PUSH shell. To answer this question it is necessary to know the current history. Terminology. The s-expression e is an explicit value escape descriptor with respect to a history h iff e has the form (*1*QUOTE fn e ... e ) and each of 1 n the following is true: - fn is a constructor or base function symbol of arity n in history h; - fn is not ADD1, ZERO, or CONS; - each e is an explicit value descriptor with corresponding denoted i term t in h; i - if fn is a constructor, the top function symbol of each t satisfies i the corresponding type restriction for fn; - if fn is PACK, t is not the explosion of any symbol; and 1 - if fn is MINUS, t is (ZERO). 1 Notes and Examples. We now illustrate the use of the *1*QUOTE escape mechanism. Suppose we are in a history obtained by extending the current one with the following: Shell Definition. Add the shell PUSH of 2 arguments with base function EMPTY, recognizer function STACKP, accessor functions TOP and POP type restrictions (ONE-OF NUMBERP) and (ONE-OF STACKP), and default functions ZERO and EMPTY. Table @ref(*1*quote-table) contains some example s-expressions employing the *1*QUOTE mechanism. To save space we again exhibit token trees whose readmacro expansions are the s-expressions in question. Table 8-6: @tag(*1*quote-table) token tree for token tree for s-expression with s-expression same translation ------------------------------------------------------------------------------ '(A (*1*QUOTE MINUS 0)) (LIST 'A (MINUS 0)) '((*1*QUOTE PUSH 2 (CONS (*1*QUOTE PUSH 3 (PUSH 2 (*1*QUOTE EMPTY))) (PUSH 3 (EMPTY))) FOO . 45) (CONS 'FOO 45)) '(*1*QUOTE PACK (PACK (97 98 99 . 0)) '(97 98 99 . 0)) ------------------------------------------------------------------------------ *1*QUOTE can be used not only to denote constants of ``new'' types but also to write down ``unusual'' constants of the primitive types, namely (MINUS 0) and ``LITATOMs corresponding to non-symbols.'' *1*QUOTE notation is actually a direct reflection of the internal representation of shell constants in the Nqthm system. If STACKP constants, say, are allowed as terms, then it is desirable to have a unique representation of them that can be used in the representation of other constants as well. The representation we developed is the one suggested by *1*QUOTE notation. We did not have to make this implementation decision be visible to the user of the logic. We could have arranged for only the primitive data types to be abbreviated by QUOTE notation and all other constants built by the application of constructor and base functions. Making the convention visible is actually an expression of our opinion that the syntax should not hide too much from the user. For example, the user writing and verifying metafunctions will appreciate knowing the internal forms. Finally, it should be noted that backquote notation can often be used where *1*QUOTE is otherwise needed. For example, (QUOTE (A (*1*QUOTE EMPTY) B)) can also be written as `(A ,(EMPTY) B). The translation of the former is the same as the translation of the readmacro expansion of the latter. 8.7. The Definition of the Extended Syntax Abbreviation. When a token tree that is readable from depth 0 and that is not an s-expression is used as an s-expression, we mean the s-expression obtained by readmacro expanding the token tree. Thus, henceforth, when we say something like ``consider the s-expression 'ABC'' we mean ``consider the s-expression (QUOTE ABC).'' Terminology. The extended syntax consists of the token trees readable from depth 0 whose readmacro expansions are well-formed. Abbreviation. When an expression in the extended syntax is used as a term, it is an abbreviation for the translation of its readmacro expansion. When an expression in the extended syntax is used as a formula, it is an abbreviation for t /= (FALSE), where t is the translation of the readmacro expansion of the expression. Note. In Appendix I we exhibit a parser for the extended syntax as a function defined within the logic. ] 9. Ordinals @label(Ordinal) Defining Axiom 22. (LESSP X Y) = (IF (ZEROP Y) F (IF (ZEROP X) T (LESSP (SUB1 X) (SUB1 Y)))) Axiom 23. (IMPLIES (NOT (ZEROP I)) (LESSP (SUB1 I) I)) Note. Axiom 23 permits us to apply the induction principle to prove the fundamental properties of LESSP, PLUS, and COUNT, which in turn permit us to induct in more sophisticated ways. Defining Axiom 24. (ORD-LESSP X Y) = (IF (NOT (LISTP X)) (IF (NOT (LISTP Y)) (LESSP X Y) T) (IF (NOT (LISTP Y)) F (IF (ORD-LESSP (CAR X) (CAR Y)) T (AND (EQUAL (CAR X) (CAR Y)) (ORD-LESSP (CDR X) (CDR Y)))))) Defining Axiom 25. (ORDINALP X) = (IF (LISTP X) (AND (ORDINALP (CAR X)) (NOT (EQUAL (CAR X) 0)) (ORDINALP (CDR X)) (OR (NOT (LISTP (CDR X))) (NOT (ORD-LESSP (CAR X) (CADR X))))) (NUMBERP X)) Examples. See the primer for a table of example ordinals. 10. Useful Function Definitions @label(Useful) 10.1. Boolean Equivalence Defining Axiom 26. (IFF P Q) = (IF P (IF Q T F) (IF Q F T)) 10.2. Natural Number Arithmetic Defining Axiom 27. (GREATERP I J) = (LESSP J I) Defining Axiom 28. (LEQ I J) = (NOT (LESSP J I)) Defining Axiom 29. (GEQ I J) = (NOT (LESSP I J)) Defining Axiom 30. (MAX I J) = (IF (LESSP I J) J (FIX I)) Defining Axiom 31. (DIFFERENCE I J) = (IF (ZEROP I) 0 (IF (ZEROP J) I (DIFFERENCE (SUB1 I) (SUB1 J)))) Defining Axiom 32. (TIMES I J) = (IF (ZEROP I) 0 (PLUS J (TIMES (SUB1 I) J))) Defining Axiom 33. (QUOTIENT I J) = (IF (ZEROP J) 0 (IF (LESSP I J) 0 (ADD1 (QUOTIENT (DIFFERENCE I J) J)))) Defining Axiom 34. (REMAINDER I J) = (IF (ZEROP J) (FIX I) (IF (LESSP I J) (FIX I) (REMAINDER (DIFFERENCE I J) J))) 10.3. List Processing Defining Axiom 35. (NLISTP X) = (NOT (LISTP X)) Defining Axiom 35a. (IDENTITY X) = X Defining Axiom 36. (APPEND L1 L2) = (IF (LISTP L1) (CONS (CAR L1) (APPEND (CDR L1) L2)) L2) Defining Axiom 37. (MEMBER X L) = (IF (NLISTP L) F (IF (EQUAL X (CAR L)) T (MEMBER X (CDR L)))) Defining Axiom 38. (UNION L1 L2) = (IF (LISTP L1) (IF (MEMBER (CAR L1) L2) (UNION (CDR L1) L2) (CONS (CAR L1) (UNION (CDR L1) L2))) L2) Defining Axiom 39. (ADD-TO-SET X L) = (IF (MEMBER X L) L (CONS X L)) Defining Axiom 40. (ASSOC X ALIST) = (IF (NLISTP ALIST) F (IF (EQUAL X (CAAR ALIST)) (CAR ALIST) (ASSOC X (CDR ALIST)))) Defining Axiom 41. (PAIRLIST L1 L2) = (IF (LISTP L1) (CONS (CONS (CAR L1) (CAR L2)) (PAIRLIST (CDR L1) (CDR L2))) NIL) 11. The Formal Metatheory @label(Meta) Note. In this section we describe the interpreter for the logic. We start by presenting the notion of the ``quotation'' of terms. Roughly speaking, the quotation of a term is an explicit value that has a structure isomorphic to that of the term; for example, the quotation of (PLUS X Y) is the explicit value '(PLUS X Y). An important property of quotations is that, for most terms, the interpreted value of the quotation under a certain standard assignment is equal to the term. For example, the value of '(PLUS X Y) as determined by our interpreter, when 'X has the value X and 'Y has the value Y, is (PLUS X Y). After defining quotations we define the interpreter. Finally, we describe the SUBRP and non-SUBRP axioms that tie QUOTEd symbols to the interpreter. 11.1. The Quotation of Terms Note. The ``quotation'' of an explicit value term may be rendered either by nests of constructor function applications or by embedding the term in a QUOTE form. This makes the notion of ``quotation'' depend upon the notion of ``explicit value,'' which, recall, involves a particular history h from which the constructor and base functions are drawn. This is the only sense in which the notion of ``quotation'' depends upon a history. Terminology. We say e is a quotation of t (in some history h which is implicit throughout this definition) iff e and t are terms and either (a) t is a variable symbol and e is the LITATOM corresponding to t, (b) t is an explicit value term and e is (LIST 'QUOTE t), or (c) t has the form (fn a ... 1 a ) and e is (CONS efn elst) where efn is the LITATOM corresponding to fn and n elst is a ``quotation list'' (see below) of a ... a . Note that clauses (b) 1 n and (c) are not mutually exclusive. Terminology. We say elst is a quotation list of tlst (in some history h which is implicit throughout this definition) iff elst is a term and tlst is a sequence of terms, and either (a) tlst is empty and elst is NIL or (b) tlst consists of a term t followed by a sequence tlst' and elst is (CONS e elst') where e is a quotation of t and elst' is a quotation list of tlst'. Examples. In Table @ref(extended-syntax-table) we give some terms and examples of their quotations. Table 11-1: @tag(extended-syntax-table) quotation displayed in term the extended syntax ------------------------------------------------------------------------------ ABC 'ABC (ZERO) '(ZERO) (ZERO) '(QUOTE 0) (PLUS 3 (TIMES X Y)) '(PLUS (QUOTE 3) (TIMES X Y)) ------------------------------------------------------------------------------ Note. To describe the axioms for the BODY function, we wish to say something like ``for each defined function symbol, fn, (BODY 'fn) is the quotation of the body of the definition of fn.'' But note that explicit values, e.g., (ZERO) above, have multiple quotations. (Indeed, all terms containing explicit values have multiple quotations.) Consequently, we cannot speak of ``the'' quotation of a term. To get around this we define the notion of the ``preferred quotation.'' The preferred quotation of (ZERO) is '(QUOTE 0). In general, the definitions of ``preferred quotation'' and ``preferred quotation list,'' below, are strictly analogous to the definitions of ``quotation'' and ``quotation list,'' above, except that explicit values must be encoded in 'QUOTE form. This is done by making clauses (b) and (c) of the definition of ``quotation'' be mutually exclusive with clause (b) the superior one. @label(preferred-quotation) Terminology. We say e is the preferred quotation of t (in some history h which is implicit throughout this definition) iff e and t are terms and either (a) t is a variable symbol and e is the LITATOM corresponding to t, (b) t is an explicit value term and e is (LIST 'QUOTE t), or (c) t has the form (fn a 1 ... a ), t is not an explicit value, and e is (CONS efn elst) where efn is the n LITATOM corresponding to fn and elst is the ``preferred quotation list'' (see below) of a ... a . 1 n Terminology. We say elst is the preferred quotation list of tlst (in some history h which is implicit throughout this definition) iff elst is a term and tlst is a sequence of terms, and either (a) tlst is empty and elst is NIL or (b) tlst consists of a term t followed by a sequence tlst' and elst is (CONS e elst') where e is the preferred quotation of t and elst' is the preferred quotation list of tlst'. 11.2. V&C$ and EVAL$ Note. The axiomatization of V&C$ and EVAL$ are rather subtle. In the primer, we explain many of the constraints and ``design decisions.'' In addition, the interested reader is urged to see [5]. Defining Axiom 42. (FIX-COST VC N) = (IF VC (CONS (CAR VC) (PLUS N (CDR VC))) F) Defining Axiom 43. (STRIP-CARS L) = (IF (NLISTP L) NIL (CONS (CAAR L) (STRIP-CARS (CDR L)))) Defining Axiom 44. (SUM-CDRS L) = (IF (NLISTP L) 0 (PLUS (CDAR L) (SUM-CDRS (CDR L)))) Note. We now ``define'' V&C$. This axiom defines a partial function and would not be admissible under the definitional principle. Because of its complexity we include comments in the axiom. Defining Axiom 45. (V&C$ FLG X VA) = (IF (EQUAL FLG 'LIST) ;X is a list of terms. Return a list of value-cost ;``pairs''-some ``pairs'' may be F. (IF (NLISTP X) NIL (CONS (V&C$ T (CAR X) VA) (V&C$ 'LIST (CDR X) VA))) ;Otherwise, consider the cases on the X. (IF (LITATOM X) ;Variable (CONS (CDR (ASSOC X VA)) 0) (IF (NLISTP X) ;Constant (CONS X 0) (IF (EQUAL (CAR X) 'QUOTE) ;QUOTEd (CONS (CADR X) 0) (IF (EQUAL (CAR X) 'IF) ;IF-expr ;If the test of the IF is defined, test the value and ;interpret the appropriate branch. Then, if the branch ;is defined, increment its cost by that of the test plus ;one. If the test is undefined, X is undefined. (IF (V&C$ T (CADR X) VA) (FIX-COST (IF (CAR (V&C$ T (CADR X) VA)) (V&C$ T (CADDR X) VA) (V&C$ T (CADDDR X) VA)) (ADD1 (CDR (V&C$ T (CADR X) VA)))) F) ;Otherwise, X is the application of a SUBRP or ;defined function. If some argument is undefined, so is X. (IF (MEMBER F (V&C$ 'LIST (CDR X) VA)) F (IF (SUBRP (CAR X)) ;SUBRP ;Apply the primitive to the values of the arguments and ;let the cost be one plus the sum of the argument costs. (CONS (APPLY-SUBR (CAR X) (STRIP-CARS (V&C$ 'LIST (CDR X) VA))) (ADD1 (SUM-CDRS (V&C$ 'LIST (CDR X) VA)))) ;Defined fn ;Interpret the BODY on the values of the arguments ;and if that is defined increment the cost by one plus ;the sum of the argument costs. (FIX-COST (V&C$ T (BODY (CAR X)) (PAIRLIST (FORMALS (CAR X)) (STRIP-CARS (V&C$ 'LIST (CDR X) VA)))) (ADD1 (SUM-CDRS (V&C$ 'LIST (CDR X) VA))))))))))) Note. Having defined V&C$ we can now define the general purpose ``apply'' function in terms of it: Defining Axiom 46. (V&C-APPLY$ FN ARGS) = (IF (EQUAL FN 'IF) (IF (CAR ARGS) (FIX-COST (IF (CAAR ARGS) (CADR ARGS) (CADDR ARGS)) (ADD1 (CDAR ARGS))) F) (IF (MEMBER F ARGS) F (IF (SUBRP FN) (CONS (APPLY-SUBR FN (STRIP-CARS ARGS)) (ADD1 (SUM-CDRS ARGS))) (FIX-COST (V&C$ T (BODY FN) (PAIRLIST (FORMALS FN) (STRIP-CARS ARGS))) (ADD1 (SUM-CDRS ARGS)))))) Note. A trivial consequence of the definitions of V&C$ and V&C-APPLY$ is that the following is a theorem: Theorem. (V&C$ FLG X VA) = (IF (EQUAL FLG 'LIST) (IF (NLISTP X) NIL (CONS (V&C$ T (CAR X) VA) (V&C$ 'LIST (CDR X) VA))) (IF (LITATOM X) (CONS (CDR (ASSOC X VA)) 0) (IF (NLISTP X) (CONS X 0) (IF (EQUAL (CAR X) 'QUOTE) (CONS (CADR X) 0) (V&C-APPLY$ (CAR X) (V&C$ 'LIST (CDR X) VA)))))) Note. We finally define the functions APPLY$ and EVAL$: Defining Axiom 47. (APPLY$ FN ARGS) = (CAR (V&C-APPLY$ FN (PAIRLIST ARGS 0))) Defining Axiom 48. (EVAL$ FLG X A) = (IF (EQUAL FLG 'LIST) (IF (NLISTP X) NIL (CONS (EVAL$ T (CAR X) A) (EVAL$ 'LIST (CDR X) A))) (IF (LITATOM X) (CDR (ASSOC X A)) (IF (NLISTP X) X (IF (EQUAL (CAR X) 'QUOTE) (CADR X) (APPLY$ (CAR X) (EVAL$ 'LIST (CDR X) A)))))) 11.3. The SUBRP and non-SUBRP Axioms @label(subrp-axiom) Notes. We now axiomatize the functions SUBRP, APPLY-SUBR, FORMALS, and BODY and define what we mean by the ``SUBRP'' and ``non-SUBRP axioms.'' The function SUBRP is Boolean: Axiom 49. (OR (EQUAL (SUBRP FN) T) (EQUAL (SUBRP FN) F)) The three functions SUBRP, FORMALS, and BODY ``expect'' LITATOMs as arguments, i.e., the quotations of function symbols. We tie down the three functions outside their ``expected'' domain with the following three axioms: Axiom 50. (IMPLIES (NOT (LITATOM FN)) (EQUAL (SUBRP FN) F)) Axiom 51. (IMPLIES (NOT (LITATOM FN)) (EQUAL (FORMALS FN) F)) Axiom 52. (IMPLIES (NOT (LITATOM FN)) (EQUAL (BODY FN) F)) Note. In a similar spirit, we define the FORMALS and BODY of SUBRPs to be F, and we define the result of applying a non-SUBRP with APPLY-SUBR to be F: Axiom 53. (IMPLIES (SUBRP FN) (EQUAL (FORMALS FN) F)) Axiom 54. (IMPLIES (SUBRP FN) (EQUAL (BODY FN) F)) Axiom 55. (IMPLIES (NOT (SUBRP FN)) (EQUAL (APPLY-SUBR FN X) F)) Note. In section @ref(subrps-and-non-subrps) we enumerate the primitive SUBRPs and non-SUBRPs. For each we will add either the ``SUBRP axiom'' or the ``non-SUBRP axiom,'' which we now proceed to define. Terminology. We say term t is the nth CDR nest around the term x iff n is a natural number and either (a) n is 0 and t is x or (b) n>0 and t is (CDR t') n where t' is the n-1st CDR nest around x. When we write (CDR x) where a term is expected it is an abbreviation for the nth CDR nest around x. 2 Example. (CDR A) is (CDR (CDR A)). Terminology. The SUBRP axiom for fn, where fn is a function symbol of arity n, is (AND (EQUAL (SUBRP 'fn) T) (EQUAL (APPLY-SUBR 'fn L) 0 (fn (CAR (CDR L)) ... n-1 (CAR (CDR L))))) where 'fn is the LITATOM corresponding to fn. Example. The SUBRP axiom for PLUS is (AND (EQUAL (SUBRP 'PLUS) T) (EQUAL (APPLY-SUBR 'PLUS L) (PLUS (CAR L) (CAR (CDR L))))) @label(standard-alist) Terminology. The standard alist for a sequence of variable symbols args is NIL if args is empty and otherwise is (CONS (CONS 'v v) alist) where v is the first symbol in args, 'v is the LITATOM corresponding to v, and alist is the standard alist for the sequence of symbols obtained by deleting v from args. Example. The standard alist for X, ANS, and L is (LIST (CONS 'X X) (CONS 'ANS ANS) (CONS 'L L)) @LABEL(NON-SUBRP-AXIOM) Terminology. The non-SUBRP axiom for fn, args, and body, where fn is a function symbol, args is a sequence of variable symbols, and body is a term, is (AND (EQUAL (SUBRP 'fn) F) (EQUAL (FORMALS 'fn) eargs) (EQUAL (BODY 'fn) ebody)) where 'fn is the LITATOM corresponding to fn, eargs is the quotation list for args, and ebody is the preferred quotation of body unless body has the form (EVAL$ flg ebody1 alist) where 1. flg is an explicit value other than 'LIST; 2. ebody1 is an explicit value that is a quotation of some term body1; 3. alist is the standard alist for args; and 4. the set of variables in body1 is a subset of those in args, in which case ebody is the preferred quotation of body1. Examples. The non-SUBRP axiom for ADD2, (X Y), and (PLUS 2 X Y) is (AND (EQUAL (SUBRP 'ADD2) F) (EQUAL (FORMALS 'ADD2) '(X Y)) (EQUAL (BODY 'ADD2) '(PLUS (QUOTE 2) (PLUS X Y)))). The non-SUBRP axiom for RUS, (), and (EVAL$ T '(ADD1 (RUS)) NIL) is (AND (EQUAL (SUBRP 'RUS) F) (EQUAL (FORMALS 'RUS) NIL) (EQUAL (BODY 'RUS) '(ADD1 (RUS)))). 12. Quantification @LABEL(QUANT) Note. The reader is urged to see [5] for a motivated development of our axiomatization of FOR. 12.1. The Definition of FOR and its Subfunctions Defining Axiom 56. (QUANTIFIER-INITIAL-VALUE OP) = (CDR (ASSOC OP '((ADD-TO-SET . NIL) (ALWAYS . *1*TRUE) (APPEND . NIL) (COLLECT . NIL) (COUNT . 0) (DO-RETURN . NIL) (EXISTS . *1*FALSE) (MAX . 0) (SUM . 0) (MULTIPLY . 1) (UNION . NIL)))) Defining Axiom 57. (QUANTIFIER-OPERATION OP VAL REST) = (IF (EQUAL OP 'ADD-TO-SET) (ADD-TO-SET VAL REST) (IF (EQUAL OP 'ALWAYS) (AND VAL REST) (IF (EQUAL OP 'APPEND) (APPEND VAL REST) (IF (EQUAL OP 'COLLECT) (CONS VAL REST) (IF (EQUAL OP 'COUNT) (IF VAL (ADD1 REST) REST) (IF (EQUAL OP 'DO-RETURN) VAL (IF (EQUAL OP 'EXISTS) (OR VAL REST) (IF (EQUAL OP 'MAX) (MAX VAL REST) (IF (EQUAL OP 'SUM) (PLUS VAL REST) (IF (EQUAL OP 'MULTIPLY) (TIMES VAL REST) (IF (EQUAL OP 'UNION) (UNION VAL REST) 0))))))))))) Defining Axiom 58. (FOR V L COND OP BODY A) = (IF (NLISTP L) (QUANTIFIER-INITIAL-VALUE OP) (IF (EVAL$ T COND (CONS (CONS V (CAR L)) A)) (QUANTIFIER-OPERATION OP (EVAL$ T BODY (CONS (CONS V (CAR L)) A)) (FOR V (CDR L) COND OP BODY A)) (FOR V (CDR L) COND OP BODY A))) 12.2. The Extended Syntax for FOR-Abbreviations II @label(FOR-syntax) Note. This section completes the precise specification of the extended syntax by defining when an s-expression is an ``abbreviated FOR'' and the ``FOR expression denoted'' by such an s-expression. Terminology. An s-expression x of the form (FOR v IN lst WHEN cond op body)-i.e., x is an s-expression of length eight whose first element is the word FOR, third element is the word IN, and fifth element is the word WHEN-is an abbreviated FOR iff each of the following is true: - v is a variable symbol, - lst, cond, and body are well-formed s-expressions whose translations are the terms t-lst, t-cond, and t-body, and - op is an element of the set {ADD-TO-SET ALWAYS APPEND COLLECT COUNT DO-RETURN EXISTS MAX SUM MULTIPLY UNION}. The FOR expression denoted by such an x is (FOR 'v t-lst 't-cond 'op 't-body alist) where 'v, 't-cond, 'op, and 't-body are the preferred quotations (see page @pageref(preferred-quotation)) of v, t-cond, op, and t-body respectively, and alist is the standard alist (see page @pageref(standard-alist)) on the sequence of variable symbols obtained by deleting v from the union of the variable symbols of t-cond with those of t-body and then sorting the resulting set alphabetically. An s-expression of the form (FOR x IN lst op body) is an abbreviated FOR iff (FOR x IN lst WHEN T op body) is an abbreviated FOR and, if so, denotes the same FOR expression as that denoted by (FOR x IN lst WHEN T op body). No other form of s-expression is an abbreviated FOR. 13. SUBRPs and non-SUBRPs @label(subrps-and-non-subrps) Note. The symbol QUOTE, which is treated specially by V&C$ and cannot be defined by the user, is not a SUBRP. Axiom 59. (NOT (SUBRP 'QUOTE)). Axioms 60-64. We now add the non-SUBRP axiom for each of the following five function symbols: APPLY$, EVAL$, V&C$, V&C-APPLY$, and FOR. Each of these symbols was introduced with a defining axiom of the form (fn x ... x ) = 1 n body. For each of the five function symbols we add the non-SUBRP axiom for fn, (x ... x ), and body. 1 n Axioms 65-121. We add the SUBRP axiom for every other function symbol that is mentioned in an axiom of the current theory. The complete list of SUBRPs is: ADD1, ADD-TO-SET, AND, APPEND, APPLY-SUBR, ASSOC, BODY, CAR, CDR, CONS, COUNT, DIFFERENCE, EQUAL, FALSE, FALSEP, FIX, FIX-COST, FORMALS, GEQ, GREATERP, IDENTITY, IF, IFF, IMPLIES, LEQ, LESSP, LISTP, LITATOM, MAX, MEMBER, MINUS, NEGATIVEP, NEGATIVE-GUTS, NLISTP, NOT, NUMBERP, OR, ORDINALP, ORD-LESSP, PACK, PAIRLIST, PLUS, QUANTIFIER-INITIAL-VALUE, QUANTIFIER-OPERATION, QUOTIENT, REMAINDER, STRIP-CARS, SUB1, SUBRP, SUM-CDRS, TIMES, TRUE, TRUEP, UNION, UNPACK, ZERO, and ZEROP. 14. Induction and Recursion 14.1. Induction @label(INDUCTION) Rule of Inference. Induction Suppose (a) p is a term; (b) m is a term; (c) q , ..., q are terms; 1 k (d) h , ..., h are positive integers; 1 k (e) it is a theorem that (ORDINALP m); and (f) for 1 < = i < = k and 1 < = j < = h , s i i,j is a substitution and it is a theorem that (IMPLIES q (ORD-LESSP m/s m)). i i,j Then p is a theorem if (1) (IMPLIES (AND (NOT q ) ... (NOT q )) o* T 1 k p) is a theorem and for each 1 < = i < = k, (2) (IMPLIES (AND q p/s ... p/s ) o* T i i,1 i,h i p) is a theorem. Notes. In informally describing an application of the induction principle to some conjecture p we generally say the induction is on the variables occurring in the term m, which is called the measure. An inductive proof splits the problem into k+1 cases, a base case, given by formula (1) above, and k induction steps, given by the k formulas of form (2) above. The cases are th given by the q . The i induction step requires proving p under case q . i i The base case requires proving p under the conjunction of the negations of the th q . In the i induction step one may assume an arbitrary number (namely h ) i i th of instances, p/s , of the conjecture being proved. The j instance for i,j th the i case is given by substitution s . Each instance is called an i,j induction hypothesis. To justify an induction one must show in the theorems of supposition (f) that some ordinal measure m of the induction variables decreases under each substitution in each respective case. 14.2. The Principle of Definition @label(DEFNS) Terminology. We say that a term t governs an occurrence of a term s in a term b iff (a) either b contains a subterm of the form (IF t p q) and the occurrence of s is in p or (b) if b contains a subterm of the form (IF t' p q), where t is (NOT t') and the occurrence of s is in q. Examples. The terms P and (NOT Q) govern the first occurrence of S in (IF P (IF (IF Q A S) S B) C) The terms P and (IF Q A S) govern the second occurrence of S. Note. The mechanization of the logic is slightly more restrictive because it only inspects the ``top-level'' IFs in b. Thus, the mechanization recognizes that P governs S in (IF P (FN (IF Q S A)) B) but it does not recognize that Q governs S also. Extension Principle. Definition The axiomatic act Definition. (f x ... x ) = body 1 n is admissible under the history h provided (a) f is a function symbol of n arguments and is new in h; (b) x , ..., x are distinct variables; 1 n (c) body is a term and mentions no symbol as a variable other than x , ..., x ; 1 n (d) there is a term m such that (a) (ORDINALP m) can be proved directly in h, and (b) for each occurrence of a subterm of the form (f y ... y ) 1 n in body and the terms t , ..., t governing it, 1 k the following formula can be proved directly in h: (IMPLIES (AND t ... t ) o* T 1 k (ORD-LESSP m/s m)), where s is the substitution {< x , y > ... < x , y >}. 1 1 n n If admissible, we add the Defining Axiom. (f x ... x ) = body. 1 n In addition, we add Axiom. the non-SUBRP axiom for f, (x , ..., x ), and body. 1 n 15. Contraints and Functional Instantiation Notes. In this section we describe another extension principle and a new rule of inference: the introduction of function symbols by ``constraint'' and derivation by ``functional instantiation.'' The validity of these principles can be derived from the foregoing material, but because they change the ``flavor'' of the logic by permitting certain apparently higher-order acts we prefer to include their description here. Functional instantiation permits one to infer new theorems from old ones by instantiating function symbols instead of variables. To be sure that such an instantiation actually produces a theorem, we first check that the formulas that result from similarly instantiating certain of the axioms about the function symbols being replaced are also theorems. Intuitively speaking, the correctness of this derived rule of inference consists of little more than the trivial observation that one may systematically change the name of a function symbol to a new name in a first-order theory without losing any theorems, modulo the renaming. However, we have found that this trivial observation has important potential practical ramifications in reducing mechanical proof efforts. We also find that this observation leads to superficially shocking results, such as the proof of the associativity of APPEND by instantiation rather than induction. And finally, we are intrigued by the extent to which such techniques permit one to capture the power of higher-order logic within first-order logic. In order to make effective use of functional instantiation, we have found it necessary to augment the logic with an extension principle that permits the introduction of new function symbols without completely characterizing them. This facility permits one to add axioms about a set of new function symbols, provided one can exhibit ``witnessing'' functions that have the alleged properties. The provision for witnesses ensures that the new axioms do not render the logic inconsistent. An example of the use of such constraints is to introduce a two-place function symbol, FN, constrained to be commutative. Any commutative function, e.g., a constant function of two arguments, suffices to witness the new axiom about FN. One can then prove theorems about FN. These theorems necessarily depend upon only one fact about FN, the fact that it is commutative. Thus, no matter how complicated these theorems are to prove, the analogous theorems about some other function symbol can be inferred via functional instantiation at the mere cost of confirming that the new symbol is commutative. In the paper [3] (and in its more detailed counterpart [2]) we derive introduction by constraint and functional instantiation and we show many examples of their use, including formal studies of ``mapping functions'' such as FOLDR and FOLDL, alternatives to quantifiers, and properties of generic language interpreters. These examples are also included among the example files of Nqthm-1992. See example file examples/basic/fs-examples.events. Terminology. A LAMBDA expression is an s-expression of the form (LAMBDA (a 1 ... a ) body), where the a are distinct variable symbols and body is a term. n i The arity of such a LAMBDA expression is n, its argument list is the sequence a , ..., a , and its body is body. 1 n @label(formal-functional-substitution) Terminology. A functional substitution is a function on a finite set of function symbols such that for each pair < f, g> in the substitution, g is either a function symbol or LAMBDA expression and the arity of f is the arity of g. Terminology. We recursively define the functional instantiation of a term t under a functional substitution fs. If t is a variable, the result is t. If t is the term (f t ... t ), let t ' be the functional instantiation of t , 1 n i i for i from 1 to n inclusive, under fs. If, for some function symbol f', the pair < f, f'> is in fs, the result is (f' t ' ... t '). If a pair < f, (LAMBDA 1 n (a ... a ) term)> is in fs, the result is term/{... < a , t '> ...}. 1 n i i Otherwise, the result is (f t ' ... t '). 1 n Note. Recall that ``term/sigma'' denotes the result of applying the ordinary (variable) substitution sigma to term. If sigma is the variable substitution {< X, (FN A)> < Y, B>}, then (PLUS X Y)/sigma is (PLUS (FN A) B). Example. The functional instantiation of the term (PLUS (FN X) (TIMES Y Z)) under the functional substitution {< PLUS, DIFFERENCE> < FN, (LAMBDA (V) (QUOTIENT V A))>} is the term (DIFFERENCE (QUOTIENT X A) (TIMES Y Z)). Terminology. We recursively define the functional instantiation of a formula phi under a functional substitution fs. If phi is phi \/ phi , then the 1 2 result is phi ' \/ phi ', where phi ' and phi ' are the functional 1 2 1 2 instantiations of phi and phi under fs. If phi is ~ phi , then the result 1 2 1 is ~ phi ', where phi ' is the functional instantiation of phi under fs. If 1 1 1 phi is (x = y), then the result is (x' = y'), where x' and y' are the functional instantiations of x and y under fs. Terminology. A variable v is said to be free in (LAMBDA (a ... a ) term) if 1 n and only if v is a variable of term and v is not among the a . A variable v i is said to be free in a functional substitution if and only if it is free in a LAMBDA expression in the range of the substitution. A variable v is said to be bound in (LAMBDA (a ... a ) term) if and only if v is among the a . 1 n i Terminology. We denote functional instantiation with \ to distinguish it from ordinary (variable) substitution, which is denoted with /. Example. If rho is the functional substitution {< PLUS, (LAMBDA (U V) (ADD1 U))>} then (PLUS X Y)\rho is (ADD1 X). Extension Principle. Conservatively constraining new function symbols. The axiomatic act Constraint. Constrain f , ..., and f to have property ax, 1 n is admissible under the history h provided there exists a functional substitution fs with domain {f ... f } such that 1 n 1. the f are distinct new function symbols, i 2. each member of the range of fs is either an old function symbol or is a LAMBDA expression whose body is formed of variables and old function symbols, 3. no variable is free in fs, and 4. ax\fs is a theorem of h. If admissible, the act adds the axiom ax to the history h. The image of f i under fs is called the witness for f . i Note. Unlike the shell and definitional events, the constraint event does not add any SUBRP or non-SUBRP axioms about the new function symbols. Terminology. A functional substitution fs is tolerable with respect to a history h provided that the domain of fs contains only function symbols introduced into h by the user via extension principles other than the shell mechanism. Notes. We do not want to consider functionally substituting for built-in function symbols or shell function symbols because the axioms about them are so diffuse in the implementation. We especially do not want to consider substituting for such function symbols as ORD-LESSP, because they are used in the principle of induction. The rule of functional instantiation requires that we prove appropriate functional instances of certain axioms. Roughly speaking, we have to prove that the ``new'' functions satisfy all the axioms about the ``old'' ones. However we must be careful to avoid ``capture''-like problems. For example, if the axiom constraining an old function symbol happens to involve a variable that is free in the functional substitution, then the functional instantiation of that axiom may be a weaker formula than the soundness argument in [3] requires. We illustrate this problem in the example below. Example. Imagine that ID1 is a function of two arguments that always returns its first argument. Let the defining axiom for ID1 be the term (EQUAL (ID1 X Y) X). Call this term t. Let fs be the functional substitution {< ID1, (LAMBDA (A B) X)>}. This substitution replaces ID1 by the constant function that returns X. Observe that the fs instance of the defining axiom for ID1 is a theorem, i.e., t\fs is (EQUAL X X). A careless definition of the rule of functional instantiation would therefore permit the conclusion that any fact about ID1 holds for the constant function that returns X. But this conclusion is specious: (EQUAL (ID1 (ADD1 X) Y) (ADD1 X)) is a fact about ID1 but its functional instance under fs, (EQUAL X (ADD1 X)), is not. What is wrong? A variable in the defining axiom, t, occurs freely in fs. We were just ``lucky'' that the fs instance of the defining axiom, t, was a theorem. Had ID1 been defined with the equivalent axiom (EQUAL (ID1 U V) U), which we will call t', we would have been required to prove t'\fs which is (EQUAL X U) and is unprovable. The point is that when we attempt to prove the functional instances of the axioms, we must first rename the variables in the axioms so as to avoid the free variables in the functional substitution. Terminology. Term t is a variant of term t if t is an instance of t and 1 2 1 2 t is an instance of t . 2 1 Example. (EQUAL (ID1 U V) U) is a variant of (EQUAL (ID1 X Y) X). Terminology. If fs is a functional substitution and t is a term, then an fs renaming of t is any variant of t containing no variable free in fs. Derived Rule Of Inference. Functional Instantiation. If h is a history, fs is a tolerable functional substitution, thm is a theorem of h, and the fs instance of an fs renaming of every axiom of h can be proved in h, then thm\fs is a theorem of a definitional/constrain extension of h. Note. In [3] we show that the introduction of constrained function symbols preserves the consistency of the logic and we derive the rule of functional instantiation. In fact, we prove a more general version of it that permits us to ignore the ``irrelevant'' axioms and definitions in h. 16. Reference Guide @label(Reference-guide) We now present an alphabetical listing of the commands to the theorem prover along with the definitions of concepts used in the command descriptions. 17. Aborting or Interrupting Commands @label(abort) Means for aborting a computation or interrupting and resuming a computation are not specified in Common Lisp The Language, but there always seems to be an implementation dependent means for doing these things. Of course, even if it is possible to abort or interrupt a process, the exact point in the computation where the effect will occur is bound to be very time dependent, i.e., it's a random thing to do, in the vernacular. In general, aborting a computation means that control is taken away from the ongoing computation and is given to the top-level read-eval-print loop of Common Lisp. To abort a computation: - On a Symbolics, simultaneously press the CONTROL, META, and ABORT keys. - In Lucid on a Sun, simultaneously press the CONTROL and c keys and then type :A to the resulting break prompt. - In KCL or CMU Common Lisp on a Sun, simultaneously press the CONTROL and c keys and then type :Q to the resulting break prompt. - In Allegro on a Sun, simultaneously press the CONTROL and c keys and then type :RES to the resulting break prompt. It is sometimes necessary to try several times to abort because certain Lisp programs (e.g., the garbage collector) may cause keystrokes to be ignored. In addition, if the theorem prover is printing to the terminal when you try to abort, you may get several pages of output before the requested action seems to occur. This is because terminal output lags behind the actual computation (e.g., because of buffering). @label(interrupt) By ``interrupting'' a computation we mean that control is temporarily taken away from the ongoing computation and given to an inferior read-eval-print loop. From within this loop you can evaluate Lisp expressions, e.g., to inspect the state. See BREAK-REWRITE for example. When you are ready for the interrupted computation to resume, you communicate this to the inferior read-eval-print loop, which then terminates and returns control to the interrupted computation. To interrupt a computation - On a Symbolics, simultaneously press the CONTROL, META, and SUSPEND keys. To resume, press the RESUME key. - In Lucid on a Sun, simultaneously press the CONTROL and c keys. To resume, type :C to the break prompt. - In KCL on a Sun, simultaneously press the CONTROL and c keys. To resume, type :R to the break prompt. - In Allegro on a Sun, simultaneously press the CONTROL and c keys. To resume, type :CONT to the break prompt. - In CMU Common Lisp on a Sun, simultaneously press the CONTROL and c keys. To resume, type :GO to the break prompt. @label(db-integrity) Warning: It is technically dangerous to abort any command that changes the data base, including the event commands such as ADD-SHELL, DEFN, and PROVE-LEMMA. Such aborts may leave the data base in an inconsistent state. The only proofs we endorse are those constructed by an uninterrupted sequence of event commands. Having thus officially disavowed the practice, let us now make a few practical remarks about the effects of aborting event commands. All commands that change the data base adhere to the policy of first storing ``undo'' information and then making the change. The undo information allows us later to remove an event from the data base. Thus, if you do abort an event command that might have made changes to the data base, use UNDO-NAME to remove the aborted event. What do we mean by ``that might have made changes to the data base?'' How can you tell? The answer is, technically, see if the new name has an EVENT-FORM in the data base (see DATA-BASE). However, it doesn't hurt anything to do an UNDO-NAME; the worst that will happen is that an error is reported because the ``event'' to be undone does not exist. However, we personally behave in a somewhat less rigid way. Whenever we abort a DEFN or ADD-SHELL we do an UNDO-NAME. We don't bother to do an UNDO-NAME when we abort a PROVE-LEMMA because PROVE-LEMMA doesn't change the data base until after the proof has successfully completed. Because the theorem prover's output lags behind its actual computation, it is possible that we will someday abort a proof-thinking that it is doomed to fail-after it has in fact succeeded. But it has not happened yet. If it happens, the inconsistency will show up if the same event name is submitted later. In any case, we never feel like we have completed a proof project until an uninterrupted run of the events is performed by PROVE-FILE (see page @pageref(prove-file)). 18. ACCUMULATED-PERSISTENCE General and Example Form: (ACCUMULATED-PERSISTENCE) This routine prints a summary of the persistence totals accumulated against function and rule names for the most recently started proof attempt during which the rewrite path was maintained. See BREAK-LEMMA and MAINTAIN-REWRITE-PATH for an explanation of related features. The rewrite path is a stack of ``frames'' maintained by the rewriter and encodes a complete description of the currently active calls to the rewrite routine. Most frames record a call of the rewriter; each such frame is associated with a non-variable term (the term being rewritten) or a rule (the rule being applied). When the rewriter has completed the processing of the term or rule, the frame is popped off the rewrite path. The number of frames built while a given frame is on the path is called the persistence of the frame and is an indication of the amount of work attributable to the term or rule associated with the frame. When we pop a frame, we compute its persistence and add it into an accumulating persistence table under the topmost function symbol of the term or the name of the rule. Thus, if a proof (successful or otherwise) has been run while the rewrite path was being maintained, the accumulated persistence table will indicate the ``expense'' of dealing with all of the function names and rules involved in the proof. ACCUMULATED-PERSISTENCE prints to *STANDARD-OUTPUT* a summary of the accumulated persistence table. In particular, it says how many names have been seen by the rewriter and it lists the persistence totals of the 20 most persistent user-introduced names and the 5 most persistent primitive names.(The numbers 20 and 5 are not fixed. ACCUMULATED-PERSISTENCE actually takes two optional arguments, the first of which defaults to 20 and the second of which defaults to 5.) If names that are irrelevant to your proof appear in this listing, you could DISABLE them to speed up the proof. 19. ADD-AXIOM General Form: (ADD-AXIOM name rule-classes term) Example Form: (ADD-AXIOM NUMBERP-LOC (REWRITE) (NUMBERP (LOC X M))) ADD-AXIOM is an event command for adding a new axiom to the logic and storing it and possibly some generated rules in the data base. It does not evaluate its arguments. name must be a new name and will be made the name of the event in the data base, rule-classes must be a (possibly empty) list of rule classes and term must be a well-formed term (see TRANSLATE). ADD-AXIOM stores term in the data base as an axiom; in addition, rules of the classes specified by rule-classes are generated from term and stored. Each rule has the name name and is initially ENABLED. An error is caused if term is unsuitable for some class in rule-classes and no change is made in the data base. If successful, ADD-AXIOM prints a time triple for the event and returns the name of the new event, name. When formulating input for ADD-AXIOM you must be cognizant of the rule interpretation of term in addition to its mathematical content. See Chapter 11 for a detailed explanation of the effect of each type of rule and how rules are generated from formulas and rule classes. Note that if rule-classes is NIL then the term is stored as an axiom and will be available for USE hints but will generate no rules. We strongly advise against the use of ADD-AXIOM. Moderate use of the theorem prover usually provides convincing evidence for the proposition that users frequently believe formulas to be valid when they are not. Conferring upon an unproved formula the stamp Axiom in no way lessens the danger that it is inconsistent with the other axioms. If a concept or relation can be defined within the logic, we urge you to so define it. If a formula is in principle provable, we urge you to prove it. If your intention is to constrain some new function symbols to have certain properties, we urge you to use CONSTRAIN. 20. ADD-SHELL General Form: (ADD-SHELL const base r ac-descriptors) Example Form: (ADD-SHELL PUSH EMPTY-STACK STACKP ((TOP (ONE-OF NUMBERP LITATOM) ZERO) (POP (ONE-OF STACKP) EMPTY-STACK))) ADD-SHELL is an event command for adding a new shell to the logic. It does not evaluate its arguments. ac-descriptors must be a list of n elements. Each element must be a triple of the form (ac tr dv ). If base is non-NIL, i i i the command has the theoretical effect of the axiomatic act Shell Definition Add the shell const of n arguments with base function symbol base, recognizer symbol r, accessors ac , ..., ac , 1 n type restrictions tr , ..., tr , and 1 n default functions dv , ..., dv . 1 n If base is NIL no base function symbol is supplied. Note that the ADD-SHELL command causes an error if the corresponding invocation of the shell principle is inadmissible in the current history. If admissible, the command adds a new event in the data base whose name is const. In addition, the command adds a large number of rules to the data base. The names of the rules are generated from the user-supplied names above. We do not describe the rules generated or their precise names here. The command prints a time triple and returns const. It is with ADD-SHELL that BOOT-STRAP builds in the rules for the natural numbers, lists, and the other primitive shells. The only ways in which those primitive shells are ``more built-in'' than user declared shells are (a) because they are satellites of GROUND-ZERO they cannot be undone individually and we do not keep track of references to them, (b) the QUOTE notation provides succinct abbreviations for them, and (c) the linear arithmetic procedure is built specifically for the NUMBERPs. Note. The time ADD-SHELL takes to operate depends on the number of accessors, n, and the number of recognizers, k, listed in the ONE-OF and NONE-OF clauses of the type restrictions. Roughly speaking, the size of the normal form of one of the rewrite rules added by ADD-SHELL grows exponentially with n and quadratically with k. The rewrite rule in question, called const-EQUAL, is essentially a conjunction of n terms, each of which is a disjunction of k terms. Computing the normal form of const-EQUAL can take a while, for large n and k. In the pre-1992 releases of Nqthm this problem was exacerbated by the coding of the routine for storing rewrite rules. That routine processed each rule in a way that was quadratic in the size of the (normalized) rule. As a result, multi-accessor shell declarations with non-trivial type restrictions on each component could cause ADD-SHELL to take hours of cpu time. Nqthm-1992 contains a short cut, inspired by a suggestion of Matt Kaufmann's, that makes the storage processing linear for const-EQUAL. Nevertheless, the exponential growth is still inherent in the shell axioms. If you have an n-ary shell declaration that is taking a very long time, you might consider trivializing all of the type restrictions, by using (NONE-OF) for each accessor position. That will introduce a class of n-tuples with no restrictions on the components. You may then define a predicate that recognizes when such an n-tuple has the desired types of components. The IF-normal form of that predicate will suggest to you the size of the problem. If you use that predicate in your theorems, it may possibly cause combinatoric explosions. However, you can deal with them through conventional means: decompose your predicate into a nest of nonrecursively defined functions and disable those functions. 21. AXIOM General Forms: (AXIOM name rule-classes term) and (AXIOM name rule-classes term hints) Example Form: (AXIOM NUMBERP-LOC (REWRITE) (NUMBERP (LOC X M))) The form (AXIOM name rule-classes term) is just an abbreviation for (ADD-AXIOM name rule-classes term). The hints argument, if supplied, is ignored. This odd functionality is provided so that during proof development AXIOM commands can be used in place of selected PROVE-LEMMA commands- as one might want to do if an event list must be ``replayed'' to reproduce some data base state (e.g., to demonstrate a bug or rewrite-rule loop) but some PROVE-LEMMA commands in it take ``too long.'' See also SKIM-FILE. 22. BACKQUOTE-SETTING @label(backquote-setting) General and Example Forms: (BACKQUOTE-SETTING 'ORIG) and (BACKQUOTE-SETTING 'NQTHM) If you do not use backquote, or at least, do not use backquote in the formulas you submit to Nqthm, then BACKQUOTE-SETTING is unimportant to you. If you do use backquote in your theorems, and especially if you use it both in Nqthm formulas and in special-purpose Lisp utilities you use in connection with Nqthm, then BACKQUOTE-SETTING is very important. The Nqthm user interface is just the read-eval-print loop of the host Common Lisp. Commands are read with the standard Lisp reader. This raises a problem, illustrated below, because the backquote notation has different interpretations in different Common Lisps. Depending on which Common Lisp is used, an utterance involving backquote might read as a theorem, a non-theorem, or an ill-formed formula. To avoid this dependency on the host's interpretation of backquote, Nqthm supplies an interpretation that is consistent with the Common Lisp standard [8, 9]. If you use backquote in Nqthm terms, then you should be sure the terms are read under Nqthm's interpretation of backquote. However, the s-expressions produced by Nqthm's backquote, while consistent with the standard, are generally not as efficient, when treated as Lisp code, as those produced by most Common Lisps. Thus, if you use backquote in Lisp utility functions, you might wish to use the host interpretation when those utilities are loaded. Common Lisp's ``current readtable'' (*READTABLE*) determines how the Common Lisp reader interprets backquote. The function BACKQUOTE-SETTING modifies the readtable so as to provide either of the two interpretations backquote. (BACKQUOTE-SETTING 'ORIG) modifies the current Common Lisp readtable so that backquote is given the interpretation initially present in the host Common Lisp. That is, after invoking (BACKQUOTE-SETTING 'ORIG), type-in is read according to the host's interpretation of backquote. (BACKQUOTE-SETTING 'NQTHM) modifies the current Common Lisp readtable so that backquote is given the interpretation defined in Section @ref(extended-syntax). Warning. The initial interpretation of backquote in Nqthm is that of the host Common Lisp. If you want our formal interpretation in a session, you must invoke (BACKQUOTE-SETTING 'NQTHM). @label(backquote-problem) We now illustrate the problem caused by backquote. The Common Lisp standard [8, 9] does not specify the s-expression read in response to a backquote expression. Instead, it specifies what the value of that s-expression must be. Different implementations of Common Lisp produce different s-expressions for the same backquote expression. For example, the Nqthm interpretation of `(,X) is (CONS X 'NIL); the AKCL (Austin-Kyoto Common Lisp) interpretation of the same backquote expression is (LIST X); the Lucid interpretation is (LUCID-RUNTIME-SUPPORT:BQ-LIST X). Thus, (EQUAL (CAR '`(,X)) 'CONS) reads as a theorem under Nqthm's interpretation of backquote, reads as a falsehood under AKCL's, and reads as an ill-formed formula under Lucid's because it involves the character sequence LUCID-RUNTIME-SUPPORT:BQ-LIST which is not a legal word (see page @pageref(word)) because it contains a colon. Many experienced Nqthm users have special-purpose Lisp programs and macros they use in connection with Nqthm. Such users must be especially careful about which interpretation is given backquote. When their Lisp utilities are read and compiled, the ORIG backquote setting should be in use, for efficiency. When Nqthm formulas are read, the NQTHM setting should be in use. The Nqthm utility PROVE-FILE, which reads Nqthm events from a file and executes them, always uses the Nqthm interpretation of backquote, regardless of what setting is in force in Common Lisp's read-eval-print loop. This is part of PROVE-FILE's assurance that the file contains nothing but well-formed events. PROVE-FILE restores the previous interpretation upon termination. Our decision to make the host's backquote setting be the default setting stems from the fact that few Nqthm users are tempted to use backquote in Nqthm terms. But this decision admits the following unhappy scenario: The user fires up a Lisp and begins to develop a sequence of events leading to some interesting result, submitting each event to the read-eval-print loop as development proceeds. At some point, backquote is used in an event. The user, however, has forgotten the backquote problem and is accidentally still using the host's interpretation. It happens that the host in question expands backquoted forms into legal Nqthm terms but different ones than Nqthm's interpretation would produce. Thus, without knowing it, the user develops a data base of rules around this spurious interpretation of type-in. When the final event list is submitted to PROVE-FILE, which uses the correct Nqthm interpretation of backquote, it fails to replay. The moral is that if you use backquote in terms, use BACKQUOTE-SETTING to ensure you get the correct treatment of your type-in. Unfortunately, it is sometimes difficult, in the heat of the chase, to note that you've begun to use backquote. 23. BOOT-STRAP General Form: (BOOT-STRAP flg) Example Form: (BOOT-STRAP NQTHM) BOOT-STRAP is an event command. It erases the current data base and initializes it to the Ground Zero logic. This command creates a very large number of rules corresponding to the primitive shells and the definitions of the functions in the Ground Zero logic. It prints a time triple and returns the event name GROUND-ZERO.(A quick and dirty sketch of the theory created by BOOT-STRAP is available by printing the value of the Lisp variable BOOT-STRAP-INSTRS.) @label(thm-mode) The flg argument lets the user select which of two sets of Ground Zero axioms should be used. The argument is not evaluated by Lisp. If flg is NQTHM the theory used is that documented in this handbook. If no flg argument is supplied or if NIL is supplied or if flg is THM, the system is booted into a constructive logic very similar to the one we used before adopting the current one. We call the first logic ``NQTHM logic'' (for ``New Quantified THM'') and say the theorem prover is running in ``NQTHM mode'' when that logic is being used. We call the second logic ``THM logic'' and the associated mode ``THM mode.'' THM logic differs from NQTHM logic in the following respects: - THM does not support the ordinals. ORD-LESSP and ORDINALP are not defined in THM. Two simple lexicographic relations, LEX2 and LEX3, are defined. (LEX2 (LIST i j ) (LIST i j )) is T precisely if 1 1 2 2 either (LESSP i i ) or (EQUAL i i ) and (LESSP j j ). LEX3 is 1 2 1 2 1 2 defined similarly. LESSP, LEX2, and LEX3 are the only accepted well-founded relations in THM. - THM does not support V&C$ but does provide a more restricted sense of EVAL$. In particular, ASSOC, PAIRLIST, FIX-COST, STRIP-CARS, SUM-CDRS, SUBRP, APPLY-SUBR, FORMALS, BODY, V&C$, and V&C-APPLY$ are defined in NQTHM but are not defined in THM. EVAL$ and APPLY$ are axiomatized in THM but they are not equivalent to their counterparts in NQTHM. (EVAL$ T X A) in THM is equivalent to (MEANING X A), as it is defined in [4]. (EVAL$ 'LIST X A) is equivalent to (MEANING-LST X A) of [4]. APPLY$ in THM is axiomatized as is APPLY in [4]. Roughly speaking this means that EVAL$ ``does not know its own name.'' Additional restrictions are enforced in THM: no definition body may use EVAL$ or APPLY$. The consequence of these restrictions is that mapping functions like FOR cannot be defined, but EVAL$ of 'term is always equal to term under the standard alist, provided term does not mention EVAL$ or APPLY$. The only intended use for EVAL$ in THM is in the statement of correctness for metafunctions. - THM does not support FOR. Hence, the functions included in the NQTHM Ground Zero theory exclusively for the definition of FOR are not defined in THM: ADD-TO-SET, APPEND, MAX, UNION, QUANTIFIER-INITIAL-VALUE, QUANTIFIER-OPERATION, and FOR. - THM contains definitions for the functions LENGTH, SUBSETP, and LAST, which are not defined in the Ground Zero logic of NQTHM. THM logic differs somewhat from the logic supported by the previous release of our theorem prover. Let us call the previous version of the logic the ``old'' logic. The differences between THM logic and the old logic are as follows: - IFF is included in THM but not in the old logic. This permits the implementation, in THM mode, of ``propositional replacement'' rules. If you have an old-style event list including a definition of IFF, you should delete it (if it is defined as is our IFF) or rename it and all its uses otherwise. - EVAL$ and APPLY$ are included in THM but not in the old logic. In fact, they ``replace'' the functions MEANING, MEANING-LST, and APPLY of the old logic. The implementation of metalemmas in THM and NQTHM was simplified by changing the names of MEANING and APPLY to EVAL$ and APPLY$. See the next note. If you have an old-style event list involving theorems about MEANING and APPLY, use EVAL$ and APPLY$ instead. - The form of metalemmas in THM is as described here, not as described in [4]. The old style of metalemmas required proving that the metafunction returns a ``FORMP''. The new style does not. If you have an old-style event list containing a metalemma, reformulate it as described here. The new theorem will be simpler. - In addition to MEANING, MEANING-LST, and APPLY, the following functions were defined in the old logic but are not defined in THM: FORMP, FORM-LSTP, ARITY, SYMBOLP, LEGAL-CHAR-CODE-SEQ, ILLEGAL-FIRST-CHAR-CODES, and LEGAL-CHAR-CODES. These functions all participated in the definition of FORMP and hence were necessary for the old-style form of metalemma. Because they are no longer necessary for metalemmas, and because we imagine that no user relied upon them except for metalemmas, we simply omitted putting them into the THM logic. 24. BREAK-LEMMA General Form: (BREAK-LEMMA name) Example Form: (BREAK-LEMMA 'REVERSE-REVERSE) The argument, name, is evaluated and should be the name of a replacement rule or linear arithmetic rule. BREAK-LEMMA alerts the rewriter to look out for all attempted applications of the named rule. Whenever the rule is tried, an interactive break occurs. To remove name from the list of monitored rules, use UNBREAK-LEMMA. Note that BREAK-LEMMA cannot be used to break on function definitions or on type-prescription, compound recognizer, meta, elimination, or generalization rules. If name is not the name of an ADD-AXIOM, CONSTRAIN, FUNCTIONALLY-INSTANTIATE or PROVE-LEMMA event with lemma type REWRITE, BREAK-LEMMA prints a warning message but alerts the rewriter anyway. It is most often the case that this warning message means you misspelled the name of the rule to be monitored, but it is sometimes useful to break on names that are satellites of other events (e.g., a rewrite rule introduced by an ADD-SHELL) so the simple test that name names an event is insufficient. Warning. Because it is possible to execute an arbitrary Common Lisp form while in the interactive break under the theorem prover, it is possible to do arbitrary damage. For example, executing (THROW 'PROVE T) will immediately terminate the proof attempt successfully! We do not endorse proofs in which interactive breaks occur. We provide BREAK-LEMMA and BREAK-REWRITE simply as a means to help you diagnose what is going wrong with your rewrite rules. Recall that to apply a replacement or linear arithmetic rule the first step is to find a substitution under which the left-hand side of the replacement rule or the key term of the linear arithmetic rule matches some target term being simplified. The substitution is computed by a simple pattern matcher that is complete: if a substitution exists to make the rule syntactically identical to the target, we find it (quickly). Subsequent steps in the application of a rule include relieving the hypotheses and rewriting the right-hand side of the conclusion. When a matched rule's name appears on the list of monitored rules, an interactive break occurs immediately after the pattern matcher has succeeded. When the pattern matcher fails, no substitution exists and no break occurs even though the rule was actually considered briefly. Thus, if a rule is being monitored and no break for it occurs during a proof attempt, then either the rule is disabled or no instance of its left-hand side (or key term, as the case may be) was ever encountered by the rewriter. In this case it is probable that your expected target term got mangled somehow by other rules. We offer no mechanical help for tracking down the rules or identifying the mangled target. Our best advice is to think hard about what rules might have applied to your target. Some users would here use Pc-Nqthm [6] to carry out the rewrites which supposedly produce the target term, to verify that the term is as expected; Pc-Nqthm can also be used to determine all the rules applicable to a given term, which might suggest how the intended term got mangled. If a substitution is found, then an interactive break occurs. By typing various commands you can inspect the state of the rewriter and step through the process of attempting to apply the rule. For replacement rules the steps are first relieve the hypotheses and then rewrite the right-hand side of the conclusion. For linear arithmetic rules there are more steps: relieve the hypotheses, rewrite the conclusion, convert the rewritten conclusion into polynomial form, and make heuristic checks on the resulting polynomials. Keep in mind that additional breaks may occur during the recursive processing done to relieve hypotheses and rewrite conclusions. If at any step it is determined that the rule cannot be applied, the interactive break provides commands for displaying an explanation. However, the interactive break is not intended as a proof-checker: no facilities are provided for directing the theorem prover's strategy or affecting in any way the outcome of the attempt to apply the rule. The interactive break is a Lisp read-eval-print loop where certain atoms are treated specially. The name of the Lisp function that implements the command interpreter is BREAK-REWRITE which, under certain conditions, can be invoked directly by the user during Lisp breaks to inspect the state of the rewriter (see page @pageref(break-rewrite)). The prompt character for the break is a colon. Your commands are read by the Lisp reader. The command ? (i.e., the Lisp symbol obtained by reading a question mark followed by a carriage return) will cause a brief summary of the commands to be printed. The available commands are divided into two categories: those that are specific to this particular step in the attempt to apply the rule and general commands for inspecting the state of the rewriter. The general commands are available all the time. The context-specific or ``special'' commands change with each step. For example, on entry to the break, the command OK means ``try to relieve the hypotheses and break again when the attempt has finished.'' But immediately after the hypotheses have been relieved, OK means ``proceed to rewrite the conclusion and break again when that has finished.'' In addition, the special commands at any particular time may include some that make sense only at that time. For example, one can ask to the see the TARGET term anytime, but one can ask for the FAILED-HYP only after a failed attempt to relieve the hypotheses. Roughly speaking, the special command OK always means ``go ahead with the next step and break when it is done'' while the special command GO always means ``go ahead with the next step and all subsequent steps of this application.'' GO is useful when you wish to shortcut the interactive processing of a rule because you have determined (say from the TARGET term) that the application at hand is not interesting. Until you are familiar with the special commands you should type ``?'' often to see what your options are. The general commands for inspecting the state of the rewriter are not summarized by the ``?'' command, since ``?'' is typed fairly often. A summary of the general commands may be obtained by typing ``??''. Using the general commands you can inspect the ``rewrite path'' from the @label(rewrite-path) current target term up to the top-level goal of the simplifier. The rewrite path is a stack of frames. Roughly speaking, each frame (except the first) represents a call of the theorem prover's rewrite routine. Commands permit you to see the entire list of frames sketchily or to focus attention on a particular frame and get more information. The frame on which attention is focused is called the ``current frame'' and is initially the frame in which the target term is being rewritten. You may use general purpose commands to move the current frame up or down the stack. Other commands display detailed information about the current frame. However, the position of the current frame in no way affects the simplifier or rewriter! That is, if you move the current frame up to a point where some other target is being rewritten, the theorem prover's attention does not shift to that target! The notion of the ``current frame'' is merely a convenient way to let you inspect the stack. We now present an example of the use of general commands. Suppose we have the rules generated from the following two events: (PROVE-LEMMA REVERSE-REVERSE (REWRITE) (IMPLIES (PROPERP X) (EQUAL (REVERSE (REVERSE X)) X))) (PROVE-LEMMA PROPERP-APPEND (REWRITE) (IMPLIES (PROPERP B) (PROPERP (APPEND A B)))) Suppose also we have installed a break on PROPERP-APPEND: (BREAK-LEMMA 'PROPERP-APPEND) Finally, suppose we then execute the event (PROVE-LEMMA LEMMA NIL (IMPLIES (AND (PROPERP B) (PROPERP A)) (EQUAL (REVERSE (REVERSE (APPEND A B))) (APPEND A B)))) We show the resulting output below in typewriter font. (Entering break on replacement rule PROPERP-APPEND : ? You are in the BREAK-REWRITE command interpreter. The commands specific to this break are: cmd effect OK Attempt to relieve the hypotheses and then break. GO Proceed without further interaction. NAME Print name of the broken rule. HYPS List the hypotheses of the broken rule. CONCL Print the conclusion of the broken rule. SUBST Print the substitution being applied to the broken rule. TARGET Print the term to which the rule is being applied. ?? General purpose commands. : TARGET (PROPERP (APPEND A B)) Note that we are trying to use PROPERP-APPEND to prove that (APPEND A B) is PROPERP. We might wish to know how this subgoal has arisen. To find out, we use the general purpose commands. First we use ?? to get a summary of them. : ?? You are in the BREAK-REWRITE command interpreter. The general purpose commands are: cmd effect PATH Highlight the REWRITE path. FRAME Print the current frame, pruning deep terms. PATH! Print every frame in the path, pruning deep terms. FRAME! Print the current frame, with no pruning. PATH!! Print the path, with no pruning. ASSUMPTIONS Print the governing assumptions. ANCESTORS Print the negations of backchaining hypotheses. ACCUMULATED-PERSISTENCE Print the accumulated persistence totals. BK Move one frame towards the top-level SIMPLIFY. NX Move one frame away from the top-level SIMPLIFY. TOP Go to the top-level SIMPLIFY frame. BTM Go to the frame farthest from the top-level SIMPLIFY. n (a natural number) Go to frame number n. s-expr (a list expression) Evaluate Common Lisp s-expr ? Special purpose commands. The rewrite path will tell us how we got to the current target from the top-level goal of the simplifier. The sketchiest display of the rewrite path is given by the PATH command: : PATH ( 90) 0. (top) ( 62) 1. Rewriting (EQUAL ...) *( 61) 2. Rewriting (REVERSE ...) ( 3) 3. Applying REVERSE-REVERSE *( 2) 4. Rewriting (PROPERP ...) ( 0) 5. Applying PROPERP-APPEND There are six frames on the stack, numbered 0 through 5. The topmost one, 0, is the initial call of the simplifier. The bottommost one, 5, is the frame in which we are working on the target term. From the above display we can see that we got to the target from the top by (a) rewriting an EQUAL expression in the topmost goal, (b) rewriting a REVERSE expression below that, (c) attempting to apply the rule REVERSE-REVERSE to that, (d) rewriting a PROPERP expression as part of the attempt, and (e) attempting to apply PROPERP-APPEND to that. However, in this sketch of the path we are not told the relation of one frame to the next. Note also the parenthesized numbers on the left-hand edge of the display. Each number is the ``persistence'' of the corresponding frame. The persistence of a frame is the number of frames built since the given frame was built. The persistence of a frame is an indication of the amount of work expended so far on behalf of that frame. A frame is marked with a ``*'' if the persistence of the frame is at least twice the persistence of the frame immediately below it. In some sense, the frames marked with *'s contain terms or rewrite rules that have caused the rewriter a lot of work relative to the total amount of work so far. From the fact that the persistence of frame 1 is 62 we know that 62 frames have been built since we began rewriting the EQUAL expression in frame 1. Since only four of them are now active (frames 2-5), we know the others have since been discarded. At first sight then, the EQUAL expression in frame 1 is relatively expensive to rewrite. But the persistence of frame 2 is 61. Thus, except for the construction of frame 2 itself, all the work involved in frame 1 has been done under frame 2. Now note the persistence of frame 3. It is only 3. Thus, 58 frames (61 minus 3) were built under frame 2 before we got around to trying REVERSE-REVERSE in frame 3. We conclude that the REVERSE expression in frame 2 was relatively expensive to rewrite and frame 2 is marked with a *. What work was done? After the frame was built we rewrote the arguments to the REVERSE expression before looking for rules that match the target. Thus, the 58 frames in question were used for the arguments and for any REVERSE rules tried before REVERSE-REVERSE. See also ACCUMULATED-PERSISTENCE. The entire rewrite path is displayed in more detail by the following command: : PATH! ---- Frame 0 ----- (persistence 90) Goal: (IMPLIES (AND (PROPERP B) (PROPERP A)) (EQUAL (REVERSE #) (APPEND A B))) ---- Frame 1 ----- (persistence 62) Rewriting the conclusion of the top-level goal: (EQUAL (REVERSE (REVERSE #)) (APPEND A B)) under the substitution: NIL ---- Frame 2 ----- (persistence 61) < -*** Rewriting the first argument of the term in frame 1: (REVERSE (REVERSE (APPEND A B))) under the substitution: NIL ---- Frame 3 ----- (persistence 3) Attempting to apply the replacement rule REVERSE-REVERSE using the substitution: X < - (APPEND A B) ---- Frame 4 ----- (persistence 2) < -*** Rewriting the first hypothesis of REVERSE-REVERSE: (PROPERP X) under the substitution: X < - (APPEND A B) ---- Frame 5 ----- (persistence 0) Attempting to apply the replacement rule PROPERP-APPEND using the substitution: B < - B A < - A Observe that now we see more of each term being rewritten. However, we do not see each term in its entirety-note frame 1. The symbol # is printed in place of deep subterms. This is what is meant by ``pruning'' in the ?? command summary. PATH! also gives an explanation relating the activity in each frame to the activity in the frame above. In particular, we see that the REVERSE expression being rewritten in frame 2 is in fact (REVERSE (REVERSE (APPEND A B))) and is the first argument of the EQUAL expression being worked on in frame 1. When the stack contains hundreds of frames, PATH! often provides too much information. That is why the notion of current frame exists. The commands FRAME and FRAME! print out the current frame. The command n, where n is a natural number, means ``select frame n as the current frame.'' The commands BK (for ``back'') and NX (for ``next'') let you move the current frame back and forth and are useful for exploring an area of the path. 25. BREAK-REWRITE @label(BREAK-REWRITE) General Form: (BREAK-REWRITE) This Lisp routine permits the user to inspect the rewrite path (see page @pageref(rewrite-path)) as though a BREAK-LEMMA rule monitor had caused an interactive break. BREAK-REWRITE is a user-level entry into the command interpreter and can be invoked directly by the user after forcing a Lisp break while the rewriter is operating. The method used to force a Lisp break while a computation is in progress is implementation dependent. For example, in KCL the ``control-C'' key is pressed while on the Symbolics Lisp Machine the ``Suspend'' key is pressed. See page @pageref(interrupt). Once a break has been caused, executing (BREAK-REWRITE) will enable you to inspect the rewrite path with the general purpose commands described in BREAK-LEMMA above. (The special purpose commands (e.g., TARGET or CONCL) do not make sense since there is in fact no rule associated with the break.) The command OK exits BREAK-REWRITE and returns to the Lisp break from which it was invoked. For efficiency, the theorem prover does not maintain the rewrite path all the time. If BREAK-REWRITE is called when the path is not being maintained, or when the rewrite path is empty (so that there is no topmost frame), it prints a message and returns immediately. See MAINTAIN-REWRITE-PATH. BREAK-REWRITE is useful when you are trying to find out why the theorem prover is spending an unusually long time silently simplifying a particular formula. (Of course, what is unusual depends on what is usual for you. There are successful proofs in which the system is silent for many minutes.) If you have previously enabled the maintenance of the rewrite path you might force a Lisp break. If you have not previously enabled the maintenance of the rewrite path you should abort the now silent proof attempt, use (MAINTAIN-REWRITE-PATH T) to turn on maintenance, restart the proof attempt and force a break as before when the silent simplification is in progress. Once you have forced a break while the simplifier is running, call BREAK-REWRITE and use the path and frame commands to see what is going on. Most likely you will be surprised at the depth of the path and perhaps at the names of some of the rules or functions on it. Typically in these situations the simplifier is backchaining through rules you have long since forgotten and has set itself subgoals that have little to do with the problem at hand; another common problem is that nonrecursive functions have been expanded and have introduced many cases or concepts needlessly. In any case, it is frequently the case that by inspecting the path you will find the names of rules and functions that can be DISABLEd to make the proof go faster. @label(stack-overflow) In addition, BREAK-REWRITE is often useful in tracking down circularities in your rewrite rules. Circularities in the rewrite rules lead to stack overflows in the rewriter. Often when stack overflow occurs, there is no way to investigate it, because the Lisp stack is already as big as permitted. However, the rewrite path maintained by the rewriter is not part of the stack but is a separate data structure that persists even after an aborted computation. If the rewrite path was being maintained during a proof attempt that caused a stack overflow, you may abort out of the stack overflow error-thereby gaining all that stack space. Then, from the top-level Lisp read-eval-print loop invoke (BREAK-REWRITE). If it reports that the theorem prover is not in the simplifier, it means ``the theorem prover was not in the simplifier when the stack overflow occurred.''(Some replacement rules are considered so simple that they are used as ``abbreviations'' and applied exhaustively before we begin normal simplification. These rules may contain loops, and at present we offer no aids in tracking down such loops.) Otherwise, you will be able to use the BREAK-REWRITE commands to investigate the rewrite path as it stood at the time of the stack overflow. This will often make the loop manifest. This conjecture can be simplified, using the abbreviations ADDRP and IMPLIES, to: Error: Bind stack overflow. Error signalled by PROVE-LEMMA-FN. Broken at PROVE-LEMMA-FN. Type :H for Help. >>:Q Top level. >(BREAK-REWRITE) : PATH (3404) 0. (top) (3394) 1. Rewriting (GET ...) (3392) 2. Applying GET-NORMALIZER (3382) 3. Rewriting (GET ...) (3359) 4. Applying GET-NORMALIZER ... ... ( 92) 202. Applying GET-NORMALIZER ( 82) 203. Rewriting (GET ...) ( 59) 204. Applying GET-NORMALIZER ( 49) 205. Rewriting (GET ...) ( 26) 206. Applying GET-NORMALIZER ( 16) 207. Rewriting (GET ...) ( 15) 208. Rewriting (ADD-ADDR ...) ( 13) 209. Rewriting (CONS ...) *( 8) 210. Rewriting (PLUS ...) *( 2) 211. Rewriting (IF ...) ( 0) 212. Rewriting (IF ...) In using BREAK-REWRITE to look for circularities you must keep in mind that the path does not show everything that has been used to derive the current term, but what is being used right now. It might be that, in some sense, the ``cause'' of the loop is a rule not shown on the current path but which fires and completes, introducing a term which will permit it to fire again later during the rewriting. 26. CH General Forms: (CH) and (CH n) and (CH m n) Example Forms: (CH 10) (CH 'PROPERP-REVERSE) (CH 12 20) CH prints out the names of the events that have been created so far. CH takes zero, one or two arguments which are used to specify an interval in the chronological sequence of events. The arguments are both evaluated and should be either event names or event numbers, where 0 is the most recent event, 1 the next most recent, etc. Events are printed in reverse chronological order, i.e., the youngest (most recently created) event is displayed first. If no arguments are supplied, the entire chronology is printed. If only one argument is supplied, it is taken as the rightmost end point, and 0 (the most recently created event) is used as the leftmost. Here is an example. Suppose that we have just completed the proof described in Chapter 8. In particular, starting from BOOT-STRAP we defined REVERSE and PROPERP and then worked our way through the proofs of several lemmas about PROPERP, APPEND, and REVERSE, concluding with REVERSE-REVERSE. Then the following use of CH prints out a sketch of the entire session in reverse chronological order: (CH 'GROUND-ZERO) 0 (PROVE-LEMMA REVERSE-REVERSE ...) 1 (PROVE-LEMMA REVERSE-APPEND ...) 2 (PROVE-LEMMA APPEND-IS-ASSOCIATIVE ...) 3 (PROVE-LEMMA PROPERP-REVERSE ...) 4 (PROVE-LEMMA PROPERP-APPEND ...) 5 (PROVE-LEMMA APPEND-RIGHT-ID ...) 6 (DEFN PROPERP ...) 7 (DEFN REVERSE ...) 8 (BOOT-STRAP NQTHM ...) Equivalent CH commands are (CH 8), (CH 0 8), and (CH 'REVERSE-REVERSE 'GROUND-ZERO). CH prints a D after the number if the event is currently disabled. Thus, suppose we execute (DISABLE PROPERP-REVERSE) and (DISABLE PROPERP-APPEND). If we print the events between REVERSE-REVERSE and APPEND-RIGHT-ID we get 2 (PROVE-LEMMA REVERSE-REVERSE ...) 3 (PROVE-LEMMA REVERSE-APPEND ...) 4 (PROVE-LEMMA APPEND-IS-ASSOCIATIVE ...) 5 D (PROVE-LEMMA PROPERP-REVERSE ...) 6 D (PROVE-LEMMA PROPERP-APPEND ...) 7 (PROVE-LEMMA APPEND-RIGHT-ID ...) Observe in the example above that the event numbers of the events shown have been increased by 2 because the two DISABLEs (actually TOGGLE events) have become events 0 and 1. In general, event numbers are so volatile that they are useful only in successive calls of CH as one scans through the chronology looking for a given interval. The only other command in our system that uses event numbers is UBT. When the theorem prover is being used with a fast terminal and text editor it is often practical to print the entire chronology, as with (CH) and then scan it at leisure with the editor. But with slow terminals or systems that discard text that has been scrolled off the top, the primitive interval handling of CH is useful. 27. CHRONOLOGY General Form: CHRONOLOGY The Lisp variable CHRONOLOGY is set to the list of all event names in reverse chronological order. Thus, the first element of CHRONOLOGY is the name of the most recently processed event. The last element is always GROUND-ZERO, the name of the oldest event. Users typically print the value of CHRONOLOGY to refresh their memory of ``where they are'' or what names they have used. Printing CHRONOLOGY is a good way to see what is in a data base that has just been loaded. However, the value of CHRONOLOGY is often very long and the command CH is often more convenient. Users should not bind or set CHRONOLOGY. 28. COMMENT General Form: (COMMENT x ... x ) 1 k Example Form: (COMMENT THE NEXT EVENT IS THE CRUCIAL LEMMA) COMMENT is defined as a Lisp macro that takes an arbitrary number of arguments and returns T. COMMENT ignores its arguments. COMMENT is provided for historical reasons: an early version of Nqthm was written in Interlisp [10] and the COMMENT macro was the Interlisp primitive supporting the insertion of comments into code. The arguments to COMMENT were generally symbols or strings expressing some comment in \"natural language\" (e.g., English, German, etc). Because of this Interlisp ancestory, users grew accustomed to inserting such comments in event lists, where the COMMENT form appeared as though it were an event command. COMMENT is not an event; it does not change CHRONOLOGY or add any names or rules. But we permit COMMENT forms in places where events forms are expected, e.g., PROVE-FILE. Because Nqthm is now written in Common Lisp, we generally use the Common Lisp semicolon and number sign comments. Such comments have the advantage that they can be written virtually anywhere a \"white space\" can be written, e.g., before or after an event, or \"inside\" an event or formula, and they do not have to follow any syntactic rules except those regarding their delimiters. 29. COMPILE-UNCOMPILED-DEFNS General Form: (COMPILE-UNCOMPILED-DEFNS filename) Example Form: (COMPILE-UNCOMPILED-DEFNS "/temp/foo") The argument, filename, is evaluated and should be a file name. This routine creates a file of the specified name, containing the Common Lisp definitions of the currently uncompiled executable counterparts (see page @pageref[exec- counter]) of all functions in the current data base; it then compiles that file, and loads it. Thus, after calling this routine all executable counterparts are defined with compiled code. This will significantly increase the speed with which R-LOOP computes the values of submitted expressions and may increase the speed of the theorem prover if your proofs involve computation with explicit values. The name of the file created has as its extension the value of the variable FILE-EXTENSION-LISP. The directory on which the file resides is affected by the value of the variable *DEFAULT-NQTHM-PATH*. The extension of the file loaded after the compilation is specified by the variable FILE-EXTENSION-BIN (see page @pageref(file-names)). We do not always automatically compile each executable counterpart as it is created because in some circumstances (e.g., when using Kyoto Common Lisp) invoking the function COMPILE involves significant overhead and the creation of weirdly named temporary files. In addition, because files are created there is the possibilities of protection violations and resource allocation errors, problems that the theorem prover is not able to gracefully report much less recover from. However, if you wish to have each executable counterpart COMPILEd as it is defined, you may set the flag *COMPILE-FUNCTIONS-FLG* to T. We advise against doing this except on Lisp machines. 30. CONSTRAIN @label(CONSTRAIN) General Forms: (CONSTRAIN name rule-classes term fs) and (CONSTRAIN name rule-classes term fs hints) Example Form: (CONSTRAIN H-COMMUTATIVITY2 (REWRITE) (EQUAL (H X (H Y Z)) (H Y (H X Z))) ((H PLUS)) ;Hints ((USE (PLUS-COMMUTATIVITY2)))) CONSTRAIN is an event command that introduces new function symbols that are constrained to satisfy a given axiom. It does not evaluate its arguments. name must be a new name and will be made the name of the event in the data base and rule-casses must be a (possibly empty) list of rule classes. fs must be a functional substitution; the domain of fs, {f ... f }, must consist 1 n entirely of new names and may not include name, and no LAMBDA expression in the range of fs may contain free variables. The s-expression term must be a term, provided that the symbols in the domain of fs are considered function symbols with the arities of their images under fs. Finally, hints, if provided, must be as required by the PROVE-LEMMA event (see page @pageref(hint-specs)). The CONSTRAIN command has the same theoretical effect as the axiomatic act Constraint. Constrain f , ..., and f to have property term, 1 n with the additional restrictions that fs is a functional substitution satisfying the requirements of the axiomatic act and that term\fs is not just provable in the logic but provable by the implemented theorem prover. Operationally, CONSTRAIN invokes the theorem prover on the functional instantiation of term under fs, i.e., on term\fs, supplying the prover with any hints provided. Note that term\fs is a term and if it is a theorem then there exist definitions of the functions in the domain of fs such that term is a theorem. Thus, if the proof succeeds, CONSTRAIN declares each of the symbols in the domain of fs to be a function symbol of the appropriate arity, adds term as an axiom, and in addition, generates from term the rules specified by rule-classes and stores each of them in the data base. The name of each rule is name. An error is caused and there is no change in the data base if term\fs cannot be proved or if term is of a form inappropriate for some class in rule-classes. Because the only axiom added by CONSTRAIN is term, the values of the functions BODY, FORMALS, SUBRP, and APPLY-SUBR on the new function symbols are undefined. When formulating input for CONSTRAIN you must be cognizant of the rule interpretation of term in addition to its mathematical content. See Chapter 11 for a detailed explanation of the effect of each type of rule and how rules are generated from formulas and rule classes. Note that if rule-classes is NIL then the term is stored as a theorem and will be available for USE hints (see PROVE-LEMMA) but will generate no rules. 31. DATA-BASE @label(DATA-BASE) General Form: (DATA-BASE query name) Example Forms: (DATA-BASE 'IMMEDIATE-DEPENDENTS 'REVERSE) and (DATA-BASE 'IMMEDIATE-SUPPORTERS 'REVERSE) and (DATA-BASE 'EVENT-FORM 'REVERSE) This is a low-level function for getting information about the data base. Before discussing the function we describe the data base in detail. The data base is an acyclic directed graph. At each node is the following information: - the name of the node, - the event command which created the node, - a number indicating the time at which the node was created (used to order event lists chronologically), and - a list of satellites-the names of auxiliary axioms, functions, and executable counterparts introduced by the event command that created the node (see the discussion below). A node has satellites if the creating event introduces a function symbol or introduces more than one axiom. For example, the GROUND-ZERO node has as its satellites the list of every primitive function symbol, every executable counterpart, and every rule added by BOOT-STRAP. DCL nodes have a single satellite that is the executable counterpart of the symbol introduced. ADD-SHELL nodes have many satellites: the base object, the recognizer, the accessors, the executable counterparts of all the new symbols, and all the rules generated by the shell axioms. No name is a satellite of more than one node. We say a Lisp symbol is a citizen of the data base if it is either the name of a node or is a satellite of a node. The name of each axiom, theorem, function, and executable counterpart is a citizen. The only other citizens are the names of events such as TOGGLEs. Henceforth, whenever we refer to a citizen x as a node we mean either the node with name x, if such a node exists, or the node of which x is a satellite. Every citizen has a status, ENABLED or DISABLED, that is used as the status of the associated rule(s). The primary of a citizen, fn, is defined as follows. If fn is a satellite of p, then p is the primary of fn. Otherwise, fn is a node and is its own primary. The arcs in the data base graph represent ``immediate dependency.'' The relation is defined below. It is not the obvious ``logical dependency'' relation. We define immediate dependency as follows. Every node in the data base is immediately dependent on GROUND-ZERO. An ADD-SHELL event is immediately dependent upon the primary of every other shell function involved in its definition, i.e., the older recognizers in the type restrictions and the older base objects in the default values. Every node whose event contains a term (including the terms used in hints) is immediately dependent upon the primary of every function symbol in every such term. Every node whose admissibility requires theorem proving (e.g., DEFN and PROVE-LEMMA nodes) is immediately dependent upon the primary of every citizen reported used in the proofs. Furthermore, every such node is immediately dependent upon the primary of every prior event that generated a type prescription rule about any function used in the proofs.[The rewriter does not keep track of the use of type prescription rules because the type set mechanism is so heavily used. This clause in the definition of dependency is an attempt to compensate for this inadequacy by sweeping into the dependency relation some of the events that might have been used. Even this does not guarantee to get all of the rules used. See the warning below.] TOGGLE events (including DISABLEs and ENABLEs) are dependent upon the primary of the event enabled or disabled. TOGGLE-DEFINED-FUNCTIONS events are dependent only upon GROUND-ZERO. The above definition establishes the meaning of the ``immediate dependents'' of every node. Note that the immediate dependents of a node include the reported uses of all of its satellites. We make the convention that the ``immediate dependents'' of a satellite are just those of its primary. For example, suppose PUSH is declared as a constructor with accessors TOP and POP. Then PUSH is the name of a node and TOP and POP are among its satellites. If TOP is used in some subsequent event, the event is recorded among the dependents of TOP's primary, namely PUSH. Uses of POP and the other functions introduced in the shell declaration are similarly recorded against PUSH. We freely mix such dependencies because we do not provide a way to remove one accessor, say, from the data base without removing the entire shell declaration. @label(undo-caveat) Warning: This notion of ``immediate dependency'' is flawed. Not every logical dependent is among the ``immediate dependents.'' The problem is that not all facts used by the theorem prover are reported used. In particular, type prescription lemmas are not tracked and the executable counterparts for the metafunctions SUBRP, APPLY-SUBRP, FORMALS, BODY, V&C$, V&C-APPLY$, EVAL$, APPLY$, and FOR do not leave tracks when they operate on quoted constants, even though the values of those metafunctions depend not just on the constants but how certain functions are defined. For example, suppose FN is a user-defined function. Then (SUBRP 'FN) reduces to F. Furthermore, no record is left that the computation depends on FN; indeed, in a way, it doesn't depend on the function FN, it depends on the atom (PACK '(70 78 . 0)). Thus, by using UNDO-NAME to remove an event and its dependents it is possible to get the data base into an inconsistent state: define FN, prove 'FN is not a SUBRP, undo FN, add a shell with FN as the constructor, prove 'FN is a SUBRP. Because we do not track the dependency of (SUBRP 'FN) on FN, undoing FN fails to undo the lemma that 'FN is a non-SUBRP. Moral: Do not rely upon the validity of any formula proved in a session in which UNDO-NAME was used. Think of UNDO-NAME as a quick and dirty way to approximate the logical theory obtained by removing the given event. When an interactive session has successfully led to the proof of the main theorem, replay the entire sequence of events from GROUND-ZERO or some trusted library without any undoing. See also the discussion of UNDO-BACK-THROUGH, a trusted way to remove events from the data base. We now discuss the DATA-BASE procedure. General Form: (DATA-BASE query name) The first argument is a Lisp symbol corresponding to one of the queries listed below. If the second argument, name, is not a citizen, the result is NIL. Otherwise, the result depends upon the query as described below. query result PRIMARY If name is the name of a node, DATA-BASE returns name. Otherwise, name is the name of a satellite and DATA-BASE returns the name of the node to which name is attached. Since NIL is not an event name, (DATA-BASE 'PRIMARY x) is non-NIL iff x is a citizen. If the result is different than x, x is a satellite of the result. EVENT-FORM Returns an event command equivalent to the one the user submitted to create name. name may be a satellite of the event returned. The command returned will be a list whose first element is the name of an event command, e.g., PROVE-LEMMA, ADD-SHELL, TOGGLE, etc. All list structures used as terms within the command are the result of translating (with TRANSLATE ) the user type-in. The EVENT-FORM returned may differ in other respects from the one typed by the user. For example, the user may type a DISABLE command and the EVENT-FORM may be an equivalent TOGGLE, or the user may have omitted the hints argument to a PROVE-LEMMA command and the EVENT-FORM may supply the hints NIL. STATUS Returns the Lisp symbol DISABLED if name is currently disabled; otherwise returns the symbol ENABLED. Recall that if the name of a rule is DISABLED the rule is never applied. SATELLITES Returns a list of all the satellites of the primary of name. FORMULA Roughly speaking, DATA-BASE returns the formula named by name. However, this is not a well-defined concept since some names (e.g., the name of a TOGGLE event) do not have any associated formula, and other names (e.g., the name of a shell constructor) have many associated formulas. The precise specification is as follows: If name is the name of an ADD- AXIOM, CONSTRAIN, FUNCTIONALLY- INSTANTIATE or PROVE-LEMMA event (including those generated by AXIOM and LEMMA commands), the translation of the third argument of that event command is returned (i.e., the axiom added or theorem proved). If name is the name of a defined function-even a satellite-the defining equation is returned as a formula of the form (EQUAL (name x ... x ) body). If name is anything else, NIL is 1 n returned. IMMEDIATE-DEPENDENTS Returns a list containing the names of the immediate dependents of name, ordered chronologically. ALL-DEPENDENTS Returns the transitive closure of the immediate dependents relation starting at name, ordered chronologically. This is the list of all events that somehow depend upon name-in so far as we are able to determine given the incomplete usage reports. It is this list of events, plus name itself, that will be removed from the data base if name is removed. IMMEDIATE-SUPPORTERS Returns the list of all events claiming name among their immediate dependents, ordered chronologically. ALL-SUPPORTERS Returns the transitive closure of the immediate supporters relation starting at name, ordered chronologically. This is the list of all events upon which name somehow depends-in so far as we are able to determine given the incomplete usage reports. ANCESTORS If name is not a function symbol, NIL is returned. Otherwise, returns a list of the names of all the DEFN, CONSTRAIN, ADD-SHELL and DCL events which introduced the function symbols that are ancestors of name. See page @pageref(ancestor) for the definition of ``ancestor.''< The Lisp program ANCESTORS takes a list of function symbols and returns the union of the ancestral event names of each of them. (DATA-BASE 'ANCESTORS name) is just (ANCESTORS (LIST name)). When the ancestors of a clique of function symbols is needed, the routine ANCESTORS is much more efficient than multiple calls of DATA-BASE.> 32. DCL General Form: (DCL fn args) Example Form: (DCL LOC (VAR MEM)) DCL is an event command for introducing an undefined function symbol into the logic. It does not evaluate its arguments. fn must be a new function symbol and args must be a list of n distinct variable symbols. DCL declares fn to be a function symbol of arity n. fn is henceforth considered ``old.'' DCL adds no axioms to the theory. Unless an error is caused because of improper arguments, DCL adds a new event to the data base, prints a time triple, and returns the new event name, fn. If a function symbol has been introduced with DCL we say it is an undefined function symbol. The example declaration above declares LOC to be a function of arity 2, provided the name LOC has not been previously introduced as an event or function name. After the declaration, it is permitted to use such expressions as (LOC V M) and (LOC (CAAR X) (MEM ST)) as terms. Undefined function symbols can be used in formulas, e.g., axioms, definitions, and theorems. However, they cannot subsequently be defined. Undefined functions are not explicit value preserving: calls of undefined functions on explicit values cannot be reduced to explicit values by the primitive axioms and definitions. Calls of functions defined in terms of undefined functions are usually not explicit value preserving-not if the undefined functions are necessarily involved in the computation. Since DCL adds no axioms, the primitive metafunctions SUBRP, APPLY-SUBR, etc., are undefined on 'fn if they were undefined on 'fn before the DCL. The user may add axioms to characterize fn. However, in that case we recommend that you use CONSTRAIN, rather than DCL, to introduce fn and thus avoid the use of ADD-AXIOM. It may be instructive to note that (DCL fn args) could be implemented as (CONSTRAIN fn-INTRO NIL T ((fn (LAMBDA args T)))), except that the latter creates the event name fn-INTRO whereas the former uses fn as both the event name and the name of the introduced function. 33. DEFN General Forms: (DEFN fn args body) and (DEFN fn args body hints) Example Forms: (DEFN LEN (X) (IF (NLISTP X) 0 (ADD1 (LEN (CDR X))))) and (DEFN UP (I J) (IF (LESSP I J) (UP (ADD1 I) J) T) ((LESSP (DIFFERENCE J I)))) DEFN is an event command for defining a function symbol. It does not evaluate its arguments. args must be a list of n variable names v , ..., v . The 1 n command has the same theoretical effect as the axiomatic act: Definition. (fn v ... v ) = body 1 n with the following exception. Admissibility restriction (d) of the principle of definition is that ``there is a term m ...'' such that certain derived formulas are theorems. The implemented principle of definition further requires that the theorems be provable by the theorem prover's simplification process! If admissible, the theory is augmented by the axioms introduced by the above axiomatic act. In addition, the rules corresponding to those axioms are added to the data base. DEFN then computes the induction schemes suggested by the various measured subsets. It also computes a type prescription rule for the function and preprocesses the body of the function to create a definitional replacement rule (named fn) for expanding calls of the function. To preprocess the body, DEFN expands the calls of all nonrecursive primitive functions in the body (e.g., AND, FIX) and then normalizes the resulting IF-expression so that no IF contains an IF in its test. This may exponentially increase the size of the body. Finally, DEFN creates a new event named fn and links it into the data base. Then DEFN prints a narrative describing the justification(s) of the definition and the type prescription computed, a time triple is printed, and fn is returned. If the axiomatic act above is inadmissible (or the simplifier cannot prove the required formulas), an appropriate message is printed, an error is caused, and the data base is left as it was before the DEFN command was executed. We have not yet discussed how the appropriate measure term is selected by DEFN. The answer is simple: unless otherwise instructed by the hints argument, DEFN tries COUNT on each argument changed in recursion. The optional hints argument permits the user-specification of a measure term to be used. @label(defn-hints) If non-NIL, hints must be a list of doublets as described below. Each doublet specifies a well-founded relation and a measure term. For each doublet, DEFN generates formulas which, if theorems, are sufficient to establish the theorems described in requirement (d). DEFN tries to prove each of the formulas for each doublet. If it is successful for any doublet, the definition is admissible. If it is unsuccessful on each, an error is caused. The hints argument allows multiple ``justifications'' of a definition; for example the first doublet might claim that the COUNT of the first argument gets smaller, while the second doublet claims that the second argument gets closer to 100. Having alternative justifications makes the theorem prover more powerful when it is considering what induction should be used on a given conjecture. Each doublet must be of the form (wfn m-term), where wfn is a ``known well-founded relation'' and m-term is a term all of whose variables are among those in args, namely x , ..., x . The known well-founded relations depend 1 n upon how BOOT-STRAP was called. If booted in NQTHM mode, the known well-founded relations are ORD-LESSP and LESSP.(Technically, the logic requires use of ORD-LESSP to justify a definition or an induction. But it is easy to see, from the definition of ORD-LESSP, that if the analogous measure theorems are proved about LESSP then the required theorems could be proved for ORD-LESSP. When LESSP is used as the relation it is unnecessary to prove that the measure term satisfies ORDINALP: since LESSP coerces non-NUMBERPs to 0, the measure term used in the required ORD-LESSP justification is just the FIX of the measure term used in the LESSP justification.) In THM mode, the known well-founded relations are LESSP, LEX2, and LEX3. When the system fails to prove the formulas justifying a submitted definition, it prints out an explanatory message that lists the measures tried and the simplified (but unproven) goals generated. If the measure you believe is the correct one was not tried, use the hints argument to specify the correct measure. If the measure you believe is the correct one was tried but could not be shown to decrease, prove REWRITE rules suitable to establish the printed goals and resubmit the definition. 34. DEFTHEORY General Form: (DEFTHEORY name theory) Example Form: (DEFTHEORY LIST-THEORY (APPEND *1*APPEND REVERSE *1*REVERSE ASSOC-OF-APPEND APPEND-RIGHT-ID REVERSE-REVERSE)) DEFTHEORY is an event command. It does not evaluate its arguments. The first argument, name, must be a new name. The second argument, theory, must be a non-empty list of citizens. DEFTHEORY creates a new event, name, that associates theory with name. Henceforth name may be used as a theory name and its ``value'' is theory. In addition to the theory names defined via DEFTHEORY there are two built-in theory names: - GROUND-ZERO: a theory name whose value is the list of citizens introduced by BOOT-STRAP, i.e., the satellites of the GROUND-ZERO event in the current data base; and - T: a theory name whose value is the list of all citizens in the current data base. Theory names make it convenient to enable or disable all the names associated with the theory. For example, the event (DISABLE-THEORY name) will globally disable all of the citizens in the value of the theory named name. There is an analogous hint to PROVE-LEMMA, also called DISABLE-THEORY, that permits the ``local disabling'' of all the names in a theory during a proof. The analogous enabling command and hint is called ENABLE-THEORY. See DISABLE-THEORY, ENABLE-THEORY, and the hints of PROVE-LEMMA for details. It is also possible to map over all the names in the value of a theory and set the enabled/disabled status of each according to the type of event that introduced the name, e.g., one can enable all the definitions and shell axioms and disable all the proved lemmas in a theory. See SET-STATUS. Using the built-in theory T and SET-STATUS it is possible to ``erect barricades'' in your data base marking the end of one phase of a project and the beginning of another. For example, by disabling all rules except definitions one ``wipes the slate clean'' and is able to begin developing a new set of rules about selected definitions just as though the definitions had just been introduced-with the added advantage that when old rules are recognized as useful they can be enabled. See SET-STATUS. Theories are very useful in connection with projects involving several layers. Imagine a project in which there are just two layers, which we shall call the ``low'' level and the ``high'' level. The low layer is defined in terms of Nqthm primitives and the high level is defined primarily in terms of the low level functions. Let LOW-DEFNS be a theory that contains the low level function names and let HIGH-DEFNS be the analogous theory for the high level functions. Suppose a large collection of rules has been developed for each layer. Collect the rule names into two theories, LOW-RULES and HIGH-RULES. The intention is that the rules for a given layer be sufficient for reasoning about the functions at that layer. Thus, to prove a high level theorem, one should have HIGH-DEFNS disabled and HIGH-RULES enabled, so the high level functions are not expanded into their low level equivalents and the high level rules are employed to manipulate them. Now suppose a useful new high level rule is discovered and that it is not derivable from the current high level rules. To prove such a rule it is necessary to ``drop down a level'' and expose the definitions of the high level concepts. Thus, HIGH-DEFNS should be enabled, HIGH-RULES should be disabled and LOW-RULES should be enabled. The proof of the new high level rule is constructed from the rules of the lower level. Theories make it convenient to move between such layers or to ensure that the theorem prover stays at a given layer. This is particularly important when, as always seems to happen, the various layers share certain function symbols and contain different sets of rules for them according to the paradigms of use in a given layer. In these cases it is often the intended use rather than the statement of a theorem that indicates what layer is involved. 35. DISABLE General Form: (DISABLE name) Example Forms: (DISABLE TIMES-2-REWRITE) and (DISABLE REVERSE) and (DISABLE *1*REMAINDER) DISABLE is an event command that sets the status of a citizen to DISABLED. The command does not evaluate its argument. The argument, name, must be a citizen. The command creates a new event name, new-name, adds a new event to the data base with new-name as its name, and sets the status of name in the data base to DISABLED. Then DISABLE prints a time triple and returns new-name. (DISABLE name) is just an abbreviation for (TOGGLE new-name name T). Indeed, even though we speak of ``DISABLE events'' the data base actually records all DISABLE, ENABLE, and TOGGLE commands as TOGGLE events. @label(disable-discussion) Roughly speaking, the effect of (DISABLE name) is to prohibit the use of name in all subsequent proof attempts until the DISABLE is overridden with an ENABLE command or temporarily overridden with an ENABLE hint in PROVE-LEMMA or new-name is undone. More precisely, suppose the status of name is DISABLED in the data base. Then if name is the name of a rule, the rule is never applied. If name is the name of a defined function, calls of the function are not expanded.< However, if all the arguments of a function call are explicit values, the executable counterpart of the function may be executed. Thus, (REVERSE '(1 2 3)) will be replaced by '(3 2 1) even if REVERSE is disabled. To prevent this, disable the executable counterpart, *1*REVERSE, of the function as well.> If name is the name of the executable counterpart of a function, applications of the function to explicit values in formulas being proved are not reduced to explicit values.< Applications of a DISABLED executable counterpart are reduced when they arise in the execution of some other executable counterpart. For example, suppose REVERSE is defined in terms of APPEND and the executable counterpart of APPEND is DISABLED as by (DISABLE *1*APPEND). Then (APPEND '(3 2) '(1)) will not be reduced to an explicit value when it appears in formulas being proved. But (REVERSE '(1 2 3)) does reduce to '(3 2 1), even though it requires the reduction of APPEND calls.> Note that, while legal, there is no sense in disabling any name other than the name of a rule, a function, or an executable counterpart. For example, disabling the name of a DISABLE event has no effect. The status of a name in the data base is either ENABLED or DISABLED according to the most recently executed ENABLE or DISABLE (or equivalent TOGGLE) event for that name still in the data base. If no such event is in the data base, the status is ENABLED. A citizen can also be disabled ``locally'' (without affecting its status in the data base) via the DISABLE and DISABLE-THEORY hints to PROVE-LEMMA, CONSTRAIN, and FUNCTIONALLY-INSTANTIATE. Disabling is often important in trying to construct large proofs. Some users prefer to operate in the mode in which all names are disabled globally and a name must be explicitly enabled locally to be used in a proof. In this mode the theorem prover usually responds quickly because its options are so limited. The command LEMMA is a variant of PROVE-LEMMA that makes it easy to operate in this mode when desired. Three situations requiring disabling arise so often we will discuss them explicitly here. 35.1. A Bolt from the Blue Scenario: A proof that was supposed to work failed. Upon analysis of the output you see that a key REWRITE rule was not applied. Upon further analysis you see that it is because the target term to which it was supposed to apply was deformed by the prior application of another rule. The most common solution to this is to disable the unwanted rule, either ``globally'' with the DISABLE command or ``locally'' with the DISABLE hint to PROVE-LEMMA. Depending on the nature of the unwanted rule it is sometimes more reasonable to re-express the desired rule so that its left-hand side anticipates the action of the other rule. This is particularly true if the ``unwanted'' rule is one of the fundamental rules of your evolving theory and having it disabled is disastrous. It should be noted that the ``unwanted'' rule might be a definition which is unexpectedly expanding. 35.2. Nonrecursive Definitions Scenario: A complicated nonrecursive function has been defined, and you have just finished proving a set of beautiful REWRITE rules that hide its complexity and let you manipulate calls of the function smoothly. However, none of your rules are ever applied! The problem here is that nonrecursive functions are (almost) always expanded immediately. Thus, no rule about such a function will ever find a match in a simplified conjecture. The solution, generally, is to disable the nonrecursive function as soon as you have characterized it with REWRITE rules. If you use nonrecursive functions extensively and do not want all proofs about them to proceed by simply expanding them into their cases, we advise the following approach: define the function, prove the fundamental properties as rewrite rules, disable the function, and base all subsequent proofs on the fundamental properties. You will frequently discover that you omitted a ``fundamental property.'' ENABLE will be useful then. 35.3. Hierarchical Rule Development Scenario: You have just finished proving a fundamental result in your evolving theory. You expect the result to be used widely in subsequent proofs. However, you find that it is not. The problem here, often, is that the lemmas proved in order to derive the fundamental result are ``getting in the way.'' Frequently, the proof of a major theorem requires the proofs of many minor ones that handle special cases. These ``lemmas'' are often formulated haphazardly simply to permit the derivation of the proof of the main theorem. However, because the lemmas necessarily deal with the same clique of function names as the main theorem, they will often find unanticipated applications outside the proof of the main theorem. In particular, they may well deform the very targets for which the main theorem was intended. The standard solution is to disable these intermediate or inconsequential lemmas once the main theorem has been proved. 36. DISABLE-THEORY General Form: (DISABLE-THEORY theory-name) Example Forms: (DISABLE-THEORY LIST-THEORY) DISABLE-THEORY is an event command. It does not evaluate its argument. The argument, theory-name, should be the name of a theory. See DEFTHEORY. DISABLE-THEORY creates a new event name, name, adds a new event to the data base with name as its name, and sets the status of every name in the list of citizens denoted by theory-name to DISABLED unless the name's status already is DISABLED. Then DISABLE-THEORY prints a time triple and returns name. The DISABLE-THEORY hint to PROVE-LEMMA permits one to disable a theory ``locally.'' (DISABLE-THEORY theory-name) is just an abbreviation for (SET-STATUS name theory-name ((OTHERWISE DISABLE))), which is defined on page @pageref(set- status). The careful reader will note that theory-name is therefore also permitted to be an explicit list of citizen names or a dotted-pair naming the endpoints of an interval of citizen names. However, to highlight the symmetry between the global disabling effect of this event and the local disabling effect of the DISABLE-THEORY hint to PROVE-LEMMA, where the ``arguments'' must be theory names, we prefer to encourage the view that DISABLE-THEORY operates on a named theory. The experienced user may wish to use the more general forms of DISABLE-THEORY. See page @pageref(disable-discussion) for a discussion of the effect of enabling or disabling a name and why it is done. See DEFTHEORY for a general discussion of why theories are useful. See the documentation of SET-STATUS for a warning about the peculiar interaction between SET-STATUS and undoing. 37. DO-EVENTS General Form: (DO-EVENTS events) Example Forms: (DO-EVENTS '((DEFN LEN (X) (IF (NLISTP X) 0 (ADD1 (LEN (CDR X))))) (PROVE-LEMMA LEN-APPEND (REWRITE) (EQUAL (LEN (APPEND A B)) (PLUS (LEN A) (LEN B)))))) (DO-EVENTS XXX) DO-EVENTS executes each event form in a list of such forms and is the most common way to replay an edited sequence of undone events or process an unproblematic sequence of newly created commands. The argument, events, is evaluated and should be a list of event forms. DO-EVENTS iterates down events, considering each event form in turn. For each form it prettyprints the form, then evaluates the form (which causes additional printing, e.g., of proofs and time triples), prints the value of the form, and then prints a form feed.(Actually, DO-EVENTS prints the value of the global Lisp variable EVENT-SEPARATOR-STRING to separate one event and its output from the next. The initial value of that variable is #\Page.) DO-EVENTS terminates either when all events have been processed or some event either causes an ERROR or FATAL ERROR or some PROVE-LEMMA fails. DO-EVENTS returns T if all events were successfully processed and NIL otherwise. Normally, the output of DO-EVENTS, and of the event commands it executes, is printed to the terminal. However, when used by PROVEALL, all output, including error messages, goes to the proofs and err extensions as noted on page @pageref(proveall). In this case, DO-EVENTS indicates its progress through events by printing out the name of each event form just before the form is executed. It prints out a comma upon completion of the execution of each form. 38. DO-FILE General Form: (DO-FILE file) Example Form: (DO-FILE "region.events") DO-FILE executes the forms in a file, treating them as though they were Nqthm event forms. The argument is evaluated and should the name of a file containing Nqthm events. The forms in the file are iteratively read, printed to the terminal, and evaluated. If any form causes an error or returns nil then it is considered to have failed and DO-FILE terminates and returns NIL. DO-FILE terminates and returns T when it has processed all of forms in the file. DO-FILE is similar in spirit to PROVE-FILE in that it processes a file presumed to contain events. Unlike PROVE-FILE it does not check that the file actually contains events and will execute any lisp form. In that sense, DO-FILE is similar to the Common Lisp function LOAD, except that DO-FILE prints the forms before execution and aborts if any form fails. Because of its cavalier attitude toward the forms in the file, DO-FILE should not be used for the final ``endorsing'' replay of a script file. But it is very handy in daily work where, for example, it is not uncommon to replay a segment of a larger event file by writing it to a temporary file and calling DO-FILE. 39. ELIM ELIM is one of the rule class tokens that may be given to ADD-AXIOM, CONSTRAIN, FUNCTIONALLY-INSTANTIATE or PROVE-LEMMA to indicate what kinds of rules should be generated from a formula. ELIM rules are used in the destructor elimination process, which is the second process tried (simplification being the first). 40. ENABLE General Form: (ENABLE name) Example Forms: (ENABLE TIMES-2-REWRITE) and (ENABLE REVERSE) and (ENABLE *1*REMAINDER) ENABLE is an event command that sets the status of a citizen to ENABLED. The command does not evaluate its argument. The argument, name, must be a citizen. The command creates a new event name, new-name, adds a new event to the data base with new-name as its name, and sets the status of name in the data base to ENABLED. Then ENABLE prints a time triple and returns new-name. (ENABLE name) is just an abbreviation for (TOGGLE new-name name NIL). See the discussion of DISABLE for details. A citizen can also be enabled ``locally'' (without affecting its status in the data base) via the ENABLE and ENABLE-THEORY hints in PROVE-LEMMA CONSTRAIN, and FUNCTIONALLY-INSTANTIATE. 41. ENABLE-THEORY General Form: (ENABLE-THEORY theory-name) Example Forms: (ENABLE-THEORY LIST-THEORY) ENABLE-THEORY is an event command. It does not evaluate its argument. The argument, theory-name, should be the name of a theory. See DEFTHEORY. ENABLE-THEORY creates a new event name, name, adds a new event to the data base with name as its name, and sets the status of every name in the list of citizens denoted by theory-name to ENABLED unless the name's status already is ENABLED. Then ENABLE-THEORY prints a time triple and returns name. The ENABLE-THEORY hint to PROVE-LEMMA permits one to enable a theory ``locally.'' (ENABLE-THEORY theory-name) is just an abbreviation for (SET-STATUS name theory-name ((OTHERWISE ENABLE))), which is defined on page @pageref(set- status). The careful reader will note that theory-name is therefore also permitted to be an explicit list of citizen names or a dotted-pair naming the endpoints of an interval of citizen names. However, to highlight the symmetry between the global enabling effect of this event and the local enabling effect of the ENABLE-THEORY hint to PROVE-LEMMA, where the ``arguments'' must be theory names, we prefer to encourage the view that ENABLE-THEORY operates on a named theory. The experienced user may wish to use the more general forms of ENABLE-THEORY. See page @pageref(disable-discussion) for a discussion of the effect of enabling or disabling a name and why it is done. See DEFTHEORY for a general discussion of why theories are useful. See the documentation of SET-STATUS for a warning about the peculiar interaction between ENABLE-STATUS and undoing. 42. Errors @label(errors) Each error condition checked and reported by the system is classified into one of three classes: - WARNING: a cautionary message concerning a legal but perhaps unintended aspect of a command, e.g., that the body of a function definition makes no reference to one of the formal parameters. - ERROR: a violation of the preconditions on a command, such as the submission of an ill-formed term, the submission of an inadmissible function definition, the attempted introduction of an event name already in the data base, etc. Generally ERRORs can be fixed by editing your type-in, though they sometimes indicate a deeper problem than mere syntax. - FATAL ERROR: a violation of the internal invariants assumed by our code or the exhaustion of some resource (e.g., the variable symbols that may be introduced by destructor elimination). It is generally not possible to fix such an error. Except for resource errors or situations in which the user has entered our code via some route other than the documented commands, FATAL ERRORs should not arise. The system may cause Lisp resource errors, such as stack overflow due to excessively deep function calling (usually an indication of circularities in the rewrite rules you have added) or the exhaustion of dynamic storage space (usually caused by circular rewriting that enlarges the term, excessive case splitting, or combinatoric explosion in the normalization of propositional expressions). The system should not cause any other kind of error, e.g., ``Trap: Argument given to CAR was not a list, locative, or NIL,'' while it is being used entirely in accordance with this handbook. If such errors occur, please notify us. All three types of errors print supposedly self-explanatory messages on the terminal. After WARNINGs the computation proceeds as though nothing had happened. The other two kinds of errors cause interactive Lisp breaks. It is not possible to fix an error from within the Lisp break and proceed. Proceeding from the break automatically aborts the computation that led to the error. The only reason we enter a break at all is to give you the opportunity to inspect the state of the computation before it is lost by the abort. Getting out of the break is a system-dependent operation. - On a Symbolics Lisp Machine, press the ABORT key. - In Lucid on a Sun, type :A to the break prompt. - In KCL or CMU Common Lisp on a Sun, type :Q to the break prompt. - In Allegro on a Sun, type :RES to the break prompt. These actions should return you to the top level of the Lisp system. The data base is not disturbed by any command that halts with an ERROR. The same cannot be said if a FATAL ERROR occurs. See however the discussion of the data base integrity on page @pageref(db-integrity). To fix an error you must edit (or retype) the command that caused it. Most Lisp systems support this, and since our code runs in many different implementations of Common Lisp and under many different kinds of host operating systems, we have not tried to implement a uniform error recovery mechanism. 43. Event Commands The event commands are those that create nodes in the data base. The event commands are - ADD-AXIOM (with its variant AXIOM) - ADD-SHELL - BOOT-STRAP - CONSTRAIN - DCL - DEFN - DEFTHEORY - FUNCTIONALLY-INSTANTIATE - PROVE-LEMMA (with its variant LEMMA) - SET-STATUS (with its variants DISABLE-THEORY and ENABLE-THEORY) - TOGGLE (with its variants DISABLE and ENABLE) - TOGGLE-DEFINED-FUNCTIONS The ``variants'' of the event commands are defined in terms of the basic commands but provide convenient commonly used forms. Thus, for example, a DISABLE command actually executes a certain call of TOGGLE. It is the TOGGLE command that is stored in the data base. 44. EVENTS-SINCE General Form: (EVENTS-SINCE name) Example Form: (EVENTS-SINCE 'REVERSE) The argument, name, is evaluated and must be the name of an event. EVENTS-SINCE returns the list of event forms for all events created since name. The list includes the event form for name itself and is ordered chronologically, starting with the event form for name. 45. Executable Counterparts @label[exec-counter] Corresponding to every function symbol in the logic is a Lisp procedure called the executable counterpart of the function. The name of the executable counterpart is obtained by concatenating the string, ``*1*'' onto the front of the function symbol. Thus, *1*APPEND is the executable counterpart of APPEND. Executable counterparts are used to compute the value of functions on constants. Such computations are the essence of the execution facility provided by R-LOOP but also arise in the theorem prover proper. Whenever a term of the form (fn 't ... 't ), e.g., the application of a function to 1 n explicit values, is produced, we use the executable counterpart of fn to compute the equivalent explicit value, if any.< More precisely, the executable counterpart of fn is so used, provided either fn is a shell constructor or base function symbol or it is enabled. Executable counterparts can be disabled individually with DISABLE or TOGGLE, as in (DISABLE *1*APPEND), in theories with DISABLE-THEORY, or in regions of the CHRONOLOGY with SET-STATUS. All executable counterparts can be disabled with TOGGLE-DEFINED-FUNCTIONS. Note that shell constructors and base function cannot be effectively disabled; they are used whether disabled or not. The theorem prover's internal form requires that explicit values be kept in a certain normal form.> To explain further we must first discuss the notion of explicit value. Recall that an explicit value is a variable-free term involving only shell constructors and base objects with the property that each argument of each constructor satisfies the type restriction of the corresponding argument position. For example, (CONS (ADD1 (ZERO)) (ZERO)) is an explicit value term. Internally, each explicit value term, t, is represented by a Lisp data structure of the form (QUOTE evg), where evg is called the explicit value guts of t. The explicit value guts is just the Lisp object corresponding to what we called the ``explicit value descriptor'' in section @ref[quote-notation], page @pageref[quote-notation].(This is not quite true. A ``dotted s-expression'' in our formal presentation is a sequence whose next-to-last element is the dot character. In Lisp, the explicit value guts corresponding to a ``dotted s-expression'' is in fact a binary tree of Lisp list cells whose right-most cell contains an atom other than NIL. Such trees are printed by Lisp with a dot. Our dotted s-expressions are read by Lisp and converted into such trees.) The explicit value above is represented by (QUOTE (1 . 0)). The Lisp object (1 . 0) is the explicit value guts of (CONS (ADD1 (ZERO)) (ZERO)). Suppose that 'e , ..., 'e are n explicit value terms and that their 1 n respective explicit value guts are e , ..., e . Suppose fn is an n-ary 1 n function. Then (fn 'e ... 'e ) is a term which is likely to be equal to some 1 n explicit value. The executable counterpart of fn, *1*fn, can sometimes be used to compute the explicit value equivalent to (fn 'e ... 'e ) as follows: 1 n Apply the Lisp procedure *1*fn to the n Lisp objects e , ..., e . If a 1 n result, e, is returned then 'e is the internal representation of an explicit value term equivalent to (fn 'e ... 'e ). Otherwise, the execution of *1*fn 1 n will signal failure (by executing a Lisp THROW). Failure is signaled either because an undefined function is encountered on the execution path or, for functions involving V&C$, certain resource limits are exhausted. See REDUCE-TERM-CLOCK. Note that we have not said that *1*fn computes an equivalent explicit if there is one, merely that if *1*fn computes a value it represents an equivalent explicit value. However, for a very large class of functions the equivalent explicit value always exists and the executable counterparts compute them. We say a function fn is explicit value preserving if either (a) it is one of the primitive functions other than the metafunctions SUBRP, APPLY-SUBR, FORMALS, BODY, V&C$, V&C-APPLY$, EVAL$, APPLY$, and FOR or (b) it is a defined function with the property that every function symbol used in the body, other than fn itself, is explicit value preserving. Explicit value preserving functions have the property that for every application to explicit values there exists an equivalent explicit value. Except for those functions which use the metafunctions excluded above and those which use functions introduced with DCL or CONSTRAIN, every function in our system is explicit value preserving. It is in this sense we used the word ``likely'' above. For all explicit value preserving functions, the executable counterparts always compute the corresponding explicit values. However, in addition to the syntactically defined class of explicit value preserving functions, there are defined functions which in fact reduce, or often reduce, to explicit values on explicit values even though metafunctions or undefined functions are used on some branches through their definitions. V&C$ itself is a good example: on many applications to explicit values, e.g., on applications to the quotations of terms composed of explicit value preserving functions, V&C$ can be reduced computationally to an explicit value. Every function symbol in the logic has an executable counterpart whether the function is explicit value preserving or not. The ADD-SHELL command and the DEFN command create the executable counterparts for the symbols they introduce. The DCL and CONSTRAIN commands create the trivial executable counterpart (``signal failure'') for their function symbols. The command TOGGLE-DEFINED-FUNCTIONS can be used to disable all executable counterparts other than shell constructors and base objects. If *1*fn is disabled then (fn 'e ... 'e ) is not reduced to an explicit value by execution of *1*fn. 1 n It is possible to compile executable counterparts. This generally makes R-LOOP evaluate your input much faster, and it will speed up your proofs if they involve explicit values. See COMPILE-UNCOMPILED-DEFNS. 46. Explicit Values Explicit values are the canonical constants in the logic: terms composed entirely of shell constructors and bottom objects with the additional property that every subterm satisfies the type restriction for the constructor argument position occupied. See page @pageref[explicit-values], in Chapter @ref[logic] for a formal definition of explicit values. See page @pageref[quote-notation] for a formal description of the notation in which they are written. See the discussion of ``executable counterparts,'' page @pageref[exec-counter], for a discussion of how we compute on explicit values. 47. Extensions See the discussion of File Names on page @pageref[file-names]. 48. FAILED-EVENTS General Form: FAILED-EVENTS FAILED-EVENTS is a Lisp variable that contains all of the event commands submitted in the current session that did not terminate successfully. 49. File Names @label(file-names) Generally speaking it is not necessary to know anything about file names the first few times you use the theorem prover: commands are typed to Lisp at the terminal and their output is printed at the terminal. The first use of file names usually occurs when you want to save the current data base to a file, with MAKE-LIB, and subsequently restore the data base, with NOTE-LIB. The other common use of file names is at the successful conclusion of a major phase of a project when you will probably want to create an ``endorsed data base'' (see page @pageref[endorsed]) and a coherent record of the event commands that construct it and the proofs concerned. This is done by calling the function PROVE-FILE or the function PROVEALL. To use these more sophisticated commands it is necessary to understand file name formats and our file name conventions. The file name format used by the theorem prover is that defined by the host operating system. We assume you are familiar with the file name formats on your machine. We make two assumptions about file name formats and then proceed to define our file name conventions. Our assumptions are - File names are written as Lisp strings, i.e., ASCII character sequences enclosed in double quotation marks, as in "doe:>nqthm>demo.lib". - A ``full file name'' is composed of two parts, the ``root name'' and the ``extension.'' The root name is separated from the extension by the ASCII dot character, ``.''. The format of both the root name and the extension are dictated entirely by the host file system. In the development of a given subject, e.g., the proof of correctness of the program FSTRPOS, the command file, the library files, the proof file, and the error message file all generally have the same root name, which on a Lisp machine might be "doe:>smith>fstrpos" and on a Unix system "/usr/smith/fstrpos". We use the extension of each file name to indicate the particular kind of data contained in the file. Commands that create or read files, such as NOTE-LIB and PROVE-FILE, take root names as their arguments and extend them by tacking on one of several fixed extension names according to the type of file to be read or written. For example, proofs generated by PROVEALL are written into a file with the proofs extension while error messages are written to the err extension. There are, in all, nine different extensions used by the system. The names used above, proofs and err, are just ``generic'' names used in this handbook. The actual strings used to form extensions may be specified by the user, by setting each of six global Lisp variables. Thus, the proofs extension of "/usr/smith/fstrpos" might be "/usr/smith/fstrpos.proofs" on one system and "doe:>smith>fstrpos.prf" on another. We make this precise in the definition below. Given a root name, file, we speak of nine different extensions of file, each known by a generic name. Each extension is formed by concatenating file, a dot, and then a character string (or Lisp symbol) associated with the generic name. To each generic name there corresponds a Lisp variable whose value is the associated character string. These variables may be set by the user. The generic names, the kind of data contained in such extensions, the Lisp variable concerned, and its initial setting are described below. events The PROVE-FILE program reads and executes the forms in the events extension of its file argument. The name used for the events extension is the value of the Lisp variable FILE-EXTENSION-EVENTS, which is initially "events". proofs The PROVEALL program opens a file with the proofs extension to contain a transcript of the event sequence being executed. In particular, each event form is printed into the proofs extension, and then the form is executed with all of its output written to the proofs extension-error messages, comments on definitions, proofs, time triples, etc.-and then the value of the completed form is printed into the proofs extension. See PROVEALL for the details. The name used for the proofs extension is the value of the Lisp variable FILE-EXTENSION-PROOFS, which is initially "proofs". The variant of PROVE-FILE that redirects terminal output, PROVE-FILE-OUT, also opens a proofs extension of its file argument and writes the transcript to it. err The PROVEALL program opens a file with the err extension to contain all WARNING, ERROR and FATAL ERROR messages generated during the PROVEALL. (These messages are also printed into the proofs extension as part of the transcript.) The err extension contains nothing but such messages and is a convenient summary of the anomalies in the event sequence. The name used for the err extension is the value of the Lisp variable FILE-EXTENSION-ERR, which is initially "err". lib The lib extension is one of two extensions in which the data base is saved by MAKE-LIB and restored by NOTE-LIB. The other is the lisp extension below. The data in the lib extension is written from and read into Lisp variables and property lists. The name used for the lib extension is the value of the variable FILE-EXTENSION-LIB and is initially "lib". lisp The lisp extension is used in connection with files that contain Common Lisp code. MAKE-LIB and NOTE-LIB use the the lisp extension for a file containing the Common Lisp definitions of the executable counterparts of the functions in the saved data base. COMPILE-UNCOMPILED-DEFNS uses the lisp extension when it creates a file to be compiled. These uses of the lisp extension all concern files created by the system in connection with executable counterparts. But the source files of the theorem prover itself are also Common Lisp files and, as noted in the Installation Guide, Chapter 13, the programs COMPILE-NQTHM and LOAD-NQTHM also use the lisp extension. The name used for the lisp extension is the value of the Lisp variable FILE-EXTENSION-LISP and is initially "lisp". bin A file with the bin extension should be the result of compiling the corresponding lisp extension. COMPILE- UNCOMPILE-DEFNS uses the bin extension to load the compiled file it creates. During installation of our system, COMPILE- NQTHM and LOAD-NQTHM (see Chapter 13) use the bin extension to load compiled files. The name used for the bin extension is the value of the Lisp variable FILE-EXTENSION-BIN. In general, FILE-EXTENSION-BIN should be set to the same extension used by the local compiler. That is, if your compiler puts the object code for file foo into foo.o then FILE-EXTENSION-BIN should be set to "o"; if your compiler puts the object code for file foo into foo.bin then FILE-EXTENSION- BIN should be set to "bin". However, the only use we make of FILE-EXTENSION-BIN is when one of the programs mentioned above LOADs the compiled code for a given root name. As far as we are aware, all implementations of the Common Lisp LOAD program now support the convention that, when no extension is used and a compiled file for the given root name exists, then the compiled file is LOADed. Thus, it is not necessary to know the extension used by the compiler-which is to say, one need not extend the root name to refer explicitly to the compiled file to be loaded. We therefore adopt the convention that when FILE-EXTENSION-BIN is NIL no extension is tacked on. This is the initial setting for FILE-EXTENSION-BIN. If your implementation of Common Lisp does not support the convention, you should set FILE-EXTENSION-BIN to the same string used by the local compiler. started The PROVE-FILE program, when observing its flag file protocol, signals the commencement of processing by creating the started extension of its file argument. The name used for the started extension is the value of the variable FILE-EXTENSION-STARTED and is initially "STARTED". proved The PROVE-FILE program, when observing its flag file protocol, signals the successful termination of processing by creating the proved extension of its file argument. The name used for the proved extension is the value of the variable FILE-EXTENSION-PROVED and is initially "proved". fail The fail extension is a file generated by PROVEALL and PROVE-FILE (when it is observing its flag file protocol) when the event sequence causes an error or a proof fails. The name used for the fail extension is the value of the Lisp variable FILE-EXTENSION-FAIL and is initially "fail". We now raise a further complication in the use of file names: most Lisps-or the underlying operating systems-provide default mechanisms by which our ``full file names'' are further elaborated before a unique file identifier is generated. For example, on Unix the user who is ``connected'' to the directory /usr/smith may find that the lisp extension of the root name "fstrpos", namely "fstrpos.lisp", actually identifies the file "/usr/smith/fstrpos.lisp". Similarly, by setting the appropriate ``default path names,'' the user on the Lisp Machine can arrange for a simple root name such as "fstrpos" to identify files with much more elaborate unique names. The Lisp variable *DEFAULT-NQTHM-PATH* may be used to determine the directory from which files are read and written while compiling, loading, or using the theorem prover. The initial value of *DEFAULT-NQTHM-PATH* is NIL, which means ``do nothing.'' However, if the value is non-NIL, then we merge that value, using the Common Lisp function MERGE-PATHNAMES, whenever we OPEN a file for reading or writing and whenever we LOAD a file. If you specify a full pathname when using functions such as NOTE-LIB, MAKE-LIB, and PROVEALL, then the value of *DEFAULT-NQTHM-PATH* is irrelevant. However, if you specify a non-NIL value for *DEFAULT-NQTHM-PATH* and you specify no directory in a file name passed to NOTE-LIB, MAKE-LIB, etc., then the file used will be on the directory specified by *DEFAULT-NQTHM-PATH*. When non-NIL, *DEFAULT-NQTHM-PATH* should be set to a string (not a pathname) that gives the full name of the relevant directory. It is important that the last character of the string be the characer that separates components of a pathname on your system, e.g., slash on a Unix system, colon on a Macintosh, or the greater-than character on a Symbolics Lisp Machine. Example values of *DEFAULT-NQTHM-PATH* are "/usr/smith/" and "doe:>nqthm>". Finally, when Nqthm opens a file for output it explicitly deletes any existing file by that name. 50. FUNCTIONALLY-INSTANTIATE General Forms: (FUNCTIONALLY-INSTANTIATE name rule-classes term old-name fs) and (FUNCTIONALLY-INSTANTIATE name rule-classes term old-name fs hints) Example Form: (FUNCTIONALLY-INSTANTIATE TIMES-PR-IS-TIMES-AC (REWRITE) (EQUAL (TIMES-AC L Z) (TIMES-PR L Z)) H-PR-IS-H-AC ((H TIMES) (H-PR TIMES-PR) (H-AC (LAMBDA (X Y) (TIMES-AC X Y))))) FUNCTIONALLY-INSTANTIATE is like PROVE-LEMMA in that it proves a theorem, term, and adds it to the data base as a theorem under the name name and as rules of the classes specified by rule-classes; however, term must be the functional instantiation under fs of some already proved theorem, named old-name. Rather than proving term directly, FUNCTIONALLY- INSTANTIATE attempts to verify that the axioms used in the proof of old-name are theorems under fs. FUNCTIONALLY-INSTANTIATE is an event command. It does not evaluate its arguments. name must be a new name, rule-classes must be a (possibly empty) list of rule classes, and term must be a term or the word *AUTO*. If old-name is a symbol, then the FORMULA DATA-BASE query for old-name must be some non-NIL formula old-term.(The case in which old-name is not a symbol is rarely used and we discuss it later.) fs must be a functional substitution; the domain of fs must consist of function symbols already introduced into the theory by the user via CONSTRAIN, DCL, or DEFN (i.e., the domain may not include symbols in the GROUND-ZERO theory nor functions introduced with ADD-SHELL) and the arity of each function in the domain of fs must be the arity of the corresponding function in the range. Unless term is *AUTO*, term must be the functional instantiation of old-term under fs, i.e., old-term\fs. (If term is *AUTO*, we treat it as though that were an abbreviation for old-term\fs below.) Finally, hints, if supplied, must be as required by the PROVE-LEMMA event (see page @pageref(hint-specs)). If the above syntactic restrictions are satisfied, FUNCTIONALLY- INSTANTIATE undertakes to prove term via functional instantiation. In particular, the theorem prover is called (with the hints provided) on the conjunction of the fs functional instances of the formulas of certain ADD-AXIOM, CONSTRAIN, and DEFN events. Such an event is involved iff (a) it uses as a function symbol some symbol in the domain of fs and (b) it is either (i) an ADD-AXIOM or (ii) a CONSTRAIN or DEFN that introduces a function symbol ``ancestral'' in old-term or some ADD-AXIOM. The user of the system need not understand what we mean by ``ancestral'' since the system determines the relevant formulas and prints them out before undertaking to prove them. However, we define the notion below. If any of the formulas to be instantiated use as a variable some variable that is free in any LAMBDA expression in the range of fs, then FUNCTIONALLY-INSTANTIATE aborts with an error and does not change the data base. Such aborts can always be avoided by choosing new variable names in fs. If the proof attempt is successful, term is stored in the data base as a theorem and rules of the classes specified by rule-classes are generated and stored as well. The name of each rule is name. If the proof attempt fails, FUNCTIONALLY- INSTANTIATE behaves as does PROVE-LEMMA: the ``failure banner'' is printed along with a time triple and NIL is returned. @label(ancestor) A function symbol fn is ancestral in a term if and only if fn is an ``ancestor'' of some symbol used as a function symbol in the term. We say that fn is an ancestor of g if and only if g was introduced by a DEFN or CONSTRAIN event, ev, and either fn is one of the function symbols introduced by ev (including g itself) or fn is an ancestor of a function symbol used in the axiom added by ev. That this definition of ancestral is sufficient to justify functional instantiation is the subject of the main proof in [2]. We wish to make it convenient to apply the same functional substitution to several different theorems in a sequence of FUNCTIONALLY-INSTANTIATE events, without having to prove the same constraints repeatedly. Therefore, FUNCTIONALLY-INSTANTIATE does not bother to prove the fs instance of a formula if any previous FUNCTIONALLY-INSTANTIATE did prove it. This requires searching through a record kept of the proof obligations of all previous FUNCTIONALLY-INSTANTIATE events. If there are many such events you may wish to limit the search to some particular set of past events. This can be done by using a non-symbol for old-name. If old-name is not a symbol then it must be a list of the form (old-name' name ... name ), where old-name' is a name 1 k whose FORMULA DATA-BASE query produces the non-NIL formula old-term in foregoing description, and each name is the name of a previous FUNCTIONALLY- i INSTANTIATE event whose proof obligations are to be searched. The search is limited to the name . i 51. Functional Substitution @label(functional-substitution) General Form: ((f g ) ... (f g )) 1 1 n n Example Form: ((H PLUS) (G (LAMBDA (X) (TIMES K X)))) As defined formally on page @pageref(formal-functional-substitution), a ``functional substitution'' is a function on a finite set of function symbols such that for each pair, < f, g>, in the substitution, g is a function symbol or LAMBDA expression and the arity of f is the arity of g. In our implementation, such substitutions are represented by lists of doublets as shown in the general form above. Each f must be a symbol and each g must be i i a function symbol or LAMBDA expression of the form (LAMBDA (a ... a ) body), 1 n where the a are distinct variable symbols and body is a term. The set of the i f is called the domain of the substitution and the set of the g is called i i the range. Functional substitutions have two distinct uses in our implementation and each use puts some additional restrictions on the substitution. Functional substitutions are used with the CONSTRAIN event to supply both arities and witnesses for the functions being introduced. In such use, the f i above must be new names and the LAMBDA expressions occurring among the g may i not contain free variables; CONSTRAIN uses the g as witnesses for the f i i while verifying that the axiom to be added is satisfiable and then CONSTRAIN introduces the f as function symbols with the same arities as the i corresponding g . The arity of (LAMBDA (a ... a ) body) is n. i 1 n Functional substitutions are also used with the FUNCTIONALLY- INSTANTIATE event, where they are used to specify how some theorem is to be functionally instantiated. In that usage, the f are required to be function symbols i already introduced into the theory by the user via CONSTRAIN, DCL, or DEFN (i.e., the f may not be GROUND-ZERO functions nor functions introduced with i ADD-SHELL) and the arity of f must be the arity of the corresponding g . i i 52. GENERALIZE GENERALIZE is one of the rule class tokens that may be given to ADD-AXIOM, CONSTRAIN, FUNCTIONALLY-INSTANTIATE or PROVE-LEMMA to indicate what kinds of rules should be generated from a formula. GENERALIZE rules are used in the generalization process, which is the fourth process tried (after simplification, destructor elimination, and use of equalities). 53. Hints to PROVE-LEMMA, CONSTRAIN and FUNCTIONALLY-INSTANTIATE General Form: ((USE (name (var term) ... (var term)) ... (name (var term) ... (var term))) (EXPAND term ... term) (DISABLE name ... name) (ENABLE name ... name) (DISABLE-THEORY theory-name ... theory-name) (ENABLE-THEORY theory-name ... theory-name) (HANDS-OFF fn ... fn) (INDUCT term) (DO-NOT-INDUCT T) (DO-NOT-GENERALIZE T) (NO-BUILT-IN-ARITH T)) The ``general form'' shown above is meant merely to be suggestive of the form taken by the hints argument to PROVE-LEMMA, CONSTRAIN and FUNCTIONALLY-INSTANTIATE. See page @pageref(hint-specs) for details. The hints argument to DEFN has a different form and is described on page @pageref(defn-hints). 54. Hints to DEFN General Form: ((relation-name measure-term) ...) Example Form: ((LESSP (DIFFERENCE (ADD1 MAX) I))) See page @pageref(defn-hints) for details on the form taken by the hints argument to DEFN. The hints argument to PROVE-LEMMA, CONSTRAIN and FUNCTIONALLY-INSTANTIATE takes a different form, described on page @pageref(hint-specs). 55. LEMMA General Forms: (LEMMA name rule-classes term) and (LEMMA name rule-classes term hints) Example Form: (LEMMA LEN-APP (REWRITE) (EQUAL (LEN (APP A B)) (PLUS (LEN A) (LEN B))) ((ENABLE LEN APP))) Some users prefer to operate in a mode in which all rules are disabled and a name must be explicitly enabled locally to be used in a proof.(This is sometimes called ``Bevier-mode'' after Bill Bevier who first used it extensively in [1].) This mode has the advantage of making the theorem prover respond quickly to most challenges, because there are usually so few options available to it. It also allows one to build up very large sets of rules without so much concern about how they act in concert. The disadvantage is that the user must ``sketch'' each proof by listing the rules involved. Theories are important in this connection because they allow groups of ``harmonious'' rules to be conveniently enabled in unison. Users often develop several theories corresponding to different situations that commonly arise in their project and then attack a given problem with the theories felt most appropriate. The LEMMA command makes operation in this mode convenient. The form (LEMMA name rule-classes term) is just an abbreviation for (PROVE-LEMMA name rule-classes term ((ENABLE-THEORY GROUND-ZERO) (DISABLE-THEORY T))). That is, when used without a hints argument LEMMA is like PROVE-LEMMA except that all non-primitive rule names are disabled. Little of interest can be proved by LEMMA when no hints are given. When a hint argument is supplied to LEMMA, a possibly modified version of it is passed to PROVE-LEMMA. See page @pageref(hint-specs) for a description of the hints argument to PROVE-LEMMA. Roughly speaking, the modified hint disables everything except the names specifically enabled by the user-supplied hint. Let hints be the user-supplied hint. We describe below the modified hint argument supplied to PROVE-LEMMA, hints'. - If hints contains no DISABLE-THEORY or ENABLE-THEORY hints, then hints' is obtained from hints by adding (ENABLE-THEORY GROUND-ZERO) and (DISABLE-THEORY T). - If hints contains any DISABLE-THEORY hint or an (ENABLE-THEORY T) hint, then hints' is hints. That is, if the supplied hints disable any theories or enable the universal theory, then LEMMA is just PROVE-LEMMA. - Otherwise, hints contains an ENABLE-THEORY hint (but not (ENABLE-THEORY T)) and does not contain a DISABLE-THEORY hint. Then hints' is obtained from hints by modifying the ENABLE-THEORY entry to include GROUND-ZERO (unless it is already there) and adding the hint (DISABLE-THEORY T). Note that it is possible to operate in both modes in the same session. Most users try to maintain a coherent and effective global data base of rules, using the global theory commands to keep the ``right'' set of rules enabled for each phase of the project. But when more control is needed, LEMMA can be used. By studying the modified hints LEMMA passes to PROVE-LEMMA (e.g., by reading the description above or by using PPE to print the PROVE-LEMMA event generated by a sample LEMMA command), the user can see how to achieve the same effect in the less commonly used commands CONSTRAIN and FUNCTIONALLY-INSTANTIATE. 56. MAINTAIN-REWRITE-PATH General Form: (MAINTAIN-REWRITE-PATH flg) Example Form: (MAINTAIN-REWRITE-PATH T) This routine turns on and off the maintenance of the rewrite path (see page @pageref(rewrite-path) for a discussion of rewrite paths and see the entries for ACCUMULATED-PERSISTENCE, BREAK-LEMMA, and BREAK-REWRITE for related features). The argument, flg, is evaluated and should be either T or NIL. If T, the rewrite path is henceforth maintained. If NIL, the rewrite path is not maintained. Maintenance of the stack involves storing into a data structure certain information about every call of the rewriter and degrades the performance to about 60% of its normal speed in proofs involving heavy use of replacement rules. Nevertheless, in deep proof developments we frequently maintain the rewrite path because of the information it provides us. BREAK-LEMMA calls MAINTAIN-REWRITE-PATH the first time a rule is monitored since the path must be maintained in case an interactive break occurs. UNBREAK-LEMMA does not disable path maintenance when the last rule is removed from the list of monitored lemmas. It merely prints a message that path maintenance is still enabled. The reason is that you may still be planning to use BREAK-REWRITE or ACCUMULATED-PERSISTENCE. If not, you can regain the normal efficiency by turning off the maintenance of the rewrite path. If path maintenance is disabled by the user while monitors are still installed on some lemma names, then a break will occur when those lemmas are activated, but path information will not be available. The rewrite path is not the Lisp control stack but a separate data structure. It persists even after an aborted computation. Therefore, if you are maintaining the rewrite path and abort some proof attempt (say, out of frustration over the time it is taking or because a stack overflow occurs) you can still inspect the path as it stood at the time of the abort. See BREAK-REWRITE. Warning: It is dangerous to interrupt the theorem prover in the middle of a proof and call MAINTAIN-REWRITE-PATH. This can lead to hard errors later in the proof attempt because, when the path is being maintained assumptions are made about its structure and these assumptions are false if the path has not been maintained from the initial entry into the rewriter. If the theorem prover is running silently for long periods and you wish to poke around with BREAK-REWRITE to see what is going on, and the rewrite path is not enabled, you are advised to abort the proof, enable path maintenance, and then start the proof from scratch. 57. MAKE-LIB General Forms: (MAKE-LIB file) and (MAKE-LIB file compile-flg) Example Form: (MAKE-LIB "demo") MAKE-LIB is the command-level routine for saving the data base so that it can be restored by NOTE-LIB. The arguments are evaluated. The first argument, file, should be a valid file root name (see page @pageref(file-names)). The second argument, if supplied, should be T or NIL; if not supplied, it defaults to NIL. The data base is saved to a pair of files, namely the lib and lisp extensions of file (see page @pageref(file-names)). Into the lisp extension of file MAKE-LIB writes the Lisp source code for the executable counterparts of all functions in the current data base. Into the lib extension it writes everything else in the data base. MAKE-LIB does not alter the data base. When the two files have been written, they are closed. If compile-flg is T, the Lisp source code for the executable counterparts is then compiled and the compiled code is then loaded. This will create a bin file extension corresponding to the just-created lisp file extension of file. MAKE-LIB returns a list containing the lib and lisp file names created. 58. META META is the first element in one of the rule class tokens that may be given to ADD-AXIOM, CONSTRAIN, FUNCTIONALLY-INSTANTIATE or PROVE-LEMMA to indicate what kinds of rules should be generated from a formula. The general form of the token is (META fn ... fn ). META rules are used in the simplification 1 n process, which is the first process tried. 59. Names-Events, Functions, and Variables In the formal treatment of the logic in Chapter @ref(logic) we defined the variable and function symbols of our logic as follows: Terminology. A sequence of characters, s, is a symbol if and only if (a) s is nonempty, (b) each character in s is a member of the set {A B C D E F G H I J K L M N O P Q R S T U V W X Y Z 0 1 2 3 4 5 6 7 8 9 $ ^ & * _ - + = ~ { } ? < >} and, (c) the first character of s is a letter, i.e., in the set {A B C D E F G H I J K L M N O P Q R S T U V W X Y Z}. Terminology. The variable symbols and function symbols of our language are the symbols other than T, F, and NIL. However, in the extended syntax we introduced the notion of ``well-formed'' s-expressions and their ``translations'' to formal terms. We then adopted the policy that all terms displayed thereafter (and used in the implementation) would in fact be well-formed s-expressions standing for their translations. The result of this is that there is a discrepancy between the set of legal names in the formal syntax and the set of names you can actually use in formulas. For example, QUOTE is a legal function name, but there is no way in the implementation to write down an application of the function symbol QUOTE, and an error is caused if you try to define QUOTE. We therefore give here the definitions of the legal names as that concept is practically defined by the extended syntax. The variable names permitted in the implementation are the symbols, excluding T, F, and NIL as above. The function names and event names permitted in the implementation are the symbols, as defined above, excluding the following: - CASE, COND, F, LET, LIST, LIST*, NIL, QUOTE, and T, and - any symbol, such as CADDR, which starts with a C, ends with an R and contains only As and Ds in between. A function or event name is old (or new) iff it is (or is not) a citizen of the data base (see page @pageref(DATA-BASE)). 60. NOTE-LIB General Forms: (NOTE-LIB file) and (NOTE-LIB file compile-flg) Example Form: (NOTE-LIB "demo") NOTE-LIB is the routine for restoring a data base saved by MAKE-LIB. The arguments are evaluated. The first argument, file, should be a valid file root name. The second argument, compile-flg, should be T or NIL; it defaults to NIL if not supplied. The lib and lisp extensions of file must exist and should have been created by MAKE-LIB (see the discussion of File Names, page @pageref[file-names). If compile-flg is T, the bin extension of file must exist and should have been created by the same call of MAKE-LIB (with compile-flg T) that created the lisp extension of file. NOTE-LIB destroys the data base extant when it is executed and configures the data base to be that which was extant when the corresponding MAKE-LIB for file was executed. If compile-flg is T, NOTE-LIB loads the compiled code for the executable counterparts of the functions in the incoming data base. Because Nqthm changes (slowly) over time, it is sometimes the case that a library file created by one release of Nqthm is in a different format than those created by another release. This is called a library incompatibility. When it occurs, i.e., when NOTE-LIB detects that the incoming library is in the wrong format, a message to that effect is printed. However, NOTE-LIB attempts to load the library anyway. While you should not trust the resulting data base, it can often be used to recover a list of events (e.g., EVENTS-SINCE) from which a new library can be constructed from scratch. NOTE-LIB returns a list containing the names of the two files read. Uncompiled Nqthm library files are portable from one host to another. That is, the brand of Common Lisp in use during MAKE-LIB is irrelevant to NOTE-LIB. A similar remark holds about the host processor. Thus, for example, library files created a Sparc workstation can be noted by a user running on a Mac II. Of course, the compiled file created when MAKE-LIB is given a second argument of T is generally not portable between Common Lisps or host processors. Thus, when noting a file from another system, do not give NOTE-LIB a second argument of T. ] 61. NQTHM Mode NQTHM mode refers to the set of axioms added to the data base by BOOT-STRAP. See the discussion of BOOT-STRAP on page @pageref(THM-mode). 62. PPE General Form: (PPE name) Example Form: (PPE 'REVERSE) PPE stands for ``PrettyPrint Event.'' The argument, name, is evaluated and should be a citizen of the data base. The command prints out the EVENT-FORM of name. 63. PROVE General Form: (PROVE term) Example Form: (PROVE '(PROPERP (REVERSE X))) PROVE is the theorem prover. The argument, term, is evaluated by Lisp and should be a term. PROVE attempts to prove term; it returns PROVED if the proof succeeds and NIL if the proof fails. The output is written to the terminal. There is no provision for hints. PROVE does not alter the data base. To silence PROVE so that no output is produced, execute (SETQ IO-FN #'(LAMBDA () NIL)). That is, bind or set the Common Lisp variable IO-FN to a no-op function of no arguments. To restore normal printing, restore IO-FN to its initial value. 64. PROVEALL @label(proveall) General Forms: (PROVEALL file events) and (PROVEALL file events compile-flg) Example Form: (PROVEALL "demo" '((DEFN REV1 (X A) (IF (NLISTP X) A (REV1 (CDR X) (CONS (CAR X) A)))) (PROVE-LEMMA REV1-IS-REV (REWRITE) (EQUAL (REV1 X A) (APPEND (REVERSE X) A))))) Note. At the time the first edition of this handbook was written, PROVEALL was the standard way to execute a sequence of event commands and collect the output into a file. It suffers however from the problem that its second argument, events, is a list of events and those events have to be created somehow, usually by reading them from a file. That creation process opens the possibility that Nqthm will somehow be corrupted. It also leaves open the possibility that the syntax of the events as displayed in the permanent record, i.e., the file from which they were read, is not strictly in Nqthm's extended syntax. For example, the source file might employ user-defined or implementation-dependent Common Lisp read macros. From such a permanent record it is often impossible to reconstruct what was actually proved. For the second edition, therefore, we introduced PROVE-FILE (see page @pageref(prove-file)) which is similar to PROVEALL but which also takes responsibility for reading the events from a specified file, enforces the extended syntax, and also enforces restrictions intended to ensure that the resulting data base is ``endorsed.'' We now prefer to use PROVE-FILE instead of PROVEALL. We have left PROVEALL in the system for the sake of compatibility. The arguments to PROVEALL are evaluated. The first argument, file, should be a file root name (see page @pageref[file-names]). Five or six extensions of file will be created, namely the proofs, err, lib, lisp, and, possibly, the bin and fail extensions. The second argument, events, should be a list of event forms to be executed. The third argument, compile-flg, should be T or NIL if supplied; if not supplied, it defaults to NIL. PROVEALL first opens the proofs and err extensions of file and arranges for the event commands and DO-EVENTS to print all their ``normal'' output to the proofs extension and all error messages to the err extension. PROVEALL then prints a header into the proofs extension, giving the current time and date. PROVEALL next uses DO-EVENTS to execute the event forms in events. DO-EVENTS executes each event form in turn until either they have all been executed or some form either causes an ERROR or FATAL ERROR or some PROVE-LEMMA fails. DO-EVENTS creates a complete transcript of the session in the proofs extension of file. In particular, the proofs extension will contain each event form executed, any WARNING or error messages caused, the justifications of each definition, the proof attempt for each PROVE-LEMMA, the time triple for each event, and the value of each event. The err extension will contain every WARNING, ERROR, and FATAL ERROR message printed in the proofs extension. Because the normal output of the event commands is being written to files, DO-EVENTS indicates its progress through events by printing just the event names to the terminal, each name being printed upon the commencement of the execution of the corresponding event. Upon termination of DO-EVENTS, PROVEALL prints a ``system description'' into the proofs extension. This description gives the names of the files that were loaded to produce the version of the theorem prover used in the proveall. The format used differs from one host system to the next. PROVEALL also prints to the proofs extension the total amount of time consumed by the run, by summing (componentwise) the time triples printed. PROVEALL then uses MAKE-LIB to save the data base, passing it the compile-flg argument. This creates both the lib and lisp extensions of file, and the bin extension if compile-flg is T. Note that if DO-EVENTS terminates prematurely because of an error or unsuccessful proof, the data base saved will be the one in which the terminal event was executed. The output from that event will be in the proofs extension. The failure can be reproduced by using NOTE-LIB to restore the data base created by PROVEALL and then executing the terminal event. Finally, if DO-EVENTS terminated prematurely, PROVEALL creates the fail extension of file and writes into it (and into the err extension) an ERROR message containing the event form that caused the failure. 65. PROVE-FILE @label(prove-file) General Forms: (PROVE-FILE file) and (PROVE-FILE file :CHECK-SYNTAX cs-flg :WRITE-FLAG-FILES wf-flg :PETITIO-PRINCIPII pp-flg) Example Forms: (PROVE-FILE "basic") and (PROVE-FILE "basic" :PETITIO-PRINCIPII T :WRITE-FLAG-FILES NIL) PROVE-FILE is the standard way to create an ``endorsed'' data base from a file purporting to be a sequence of Nqthm event commands.(We now prefer PROVE-FILE to the older PROVEALL, for the reasons given in the discussion of PROVEALL, page @pageref(proveall).) We define what we mean by an ``endorsed'' data base below, but the key property of such a data base is that we believe the formulas labeled ``theorems'' in it are actually theorems. PROVE-FILE evaluates its arguments. The first argument, file, should be a file root name (see page @pageref(file-names)), file must not end with the substring "tmp", and file.events, the events extension of file, should exist and contain Nqthm event commands as described below. In accordance with Common Lisp, the optional ``keyword arguments'' may be supplied in any order or be omitted. When omitted, the :CHECK-SYNTAX and :WRITE-FLAG-FILES arguments default to T; PETITIO-PRINCIPII defaults to NIL. PROVE-FILE is a read-eval-print loop similar to Common Lisp's LOAD but enforcing certain requirements on the forms read and evaluated. PROVE-FILE repeatedly reads a form from file.events, prints the form, checks the syntax of the form, executes the form and prints its value. If all the forms in file.events are successfully processed, PROVE-FILE returns T. If an unacceptable form is read, PROVE-FILE calls (MAKE-LIB file) to save the data base and returns NIL. By making the last form in file.events a MAKE-LIB form the user can arrange for successful termination to produce a library. All output produced during PROVE-FILE is directed to Common Lisp's *STANDARD-OUTPUT*, which is normally the terminal. Because PROVE-FILE prints the forms and their values, the text written to *STANDARD-OUTPUT* resembles an interactive session. The user wishing to direct the output to a file should see PROVE-FILE-OUT. PROVE-FILE observes a certain protocol of creating and deleting ``flag files'' to signal success or failure to a user who might be ``watching'' a PROVE-FILE in the background of some other activity. This protocol is explained below. Each form in the file.events must be one of those described below. In addition, the first form must be a BOOT-STRAP or NOTE-LIB and only the last form is permitted to be a MAKE-LIB. A form, form, may occur in file.events only if: - form is (BOOT-STRAP), (BOOT-STRAP NQTHM) or (BOOT-STRAP THM); - form is (NOTE-LIB str) or (NOTE-LIB str flg), where str is a string and flg is either T or NIL; - form is a call of ADD-AXIOM, ADD-SHELL, AXIOM, COMMENT, CONSTRAIN, DCL, DEFN, DEFTHEORY, DISABLE, DISABLE-THEORY, ENABLE, ENABLE- THEORY, FUNCTIONALLY-INSTANTIATE, LEMMA, PROVE-LEMMA, SET-STATUS, TOGGLE, TOGGLE-DEFINED-FUNCTIONS or UBT; - form is (COMPILE-UNCOMPILED-DEFNS "tmp")(PROVE-FILE may not be used with files that end in "tmp" so as to avoid the possibility of a collision of the library file created for file, namely file.lisp, and the temporary file created by COMPILE-UNCOMPILE-DEFNS, tmp.lisp. Such a collision is possible, even when file is not "tmp" since file might contain directory prefixes.); - form is (SETQ REDUCE-TERM-CLOCK n), where n is an integer; - form is (SETQ *COMPILE-FUNCTIONS-FLG* flg), where flg is either T or NIL; or - form is (MAKE-LIB str) or (MAKE-LIB str flg), where str is a string and is equal to the first argument of PROVE-FILE, file, and flg is either T or NIL. All of the event files in our collection of Nqthm benchmarks in the examples directory are processed successfully by PROVE-FILE and therefore illustrate the allowed format. The readtable used while reading forms from file.events supports only the Nqthm extended syntax (page @pageref(extended-syntax)). Thus, some legal Common Lisp forms, such as #3r102 (the integer eleven written in base three) and '#,(lisp-fn) (a QUOTEd constant created by executing the Common Lisp program lisp-fn), are disallowed in file.events; errors will be signalled when such forms are read. Caution. Because PROVE-FILE binds *READTABLE* to implement the Nqthm syntax, you may find it difficult to get out of an interactive break under PROVE-FILE. This is because our readtable prevents the use of keywords such as :q or :a, which are often chosen by implementors as the escape commands for interactive breaks. We try to restore the readtable appropriately before every error break, but circumstances beyond our control sometime prevent this. If an error occurs during PROVE-FILE and you are left in an interactive break and have difficulty (e.g., errors arise when you type a colon), we recommend that you execute (SETQ *READTABLE* (COPY-READTABLE NIL)), which will restore the host Lisp's readtable and allow you to type normally thereafter. The reason we prevent colons from occuring in Nqthm syntax is that the symbol SI::CAR, for example, might be CAR in some Lisps and not be CAR in others, depending on what symbols were imported into the SI package. If the :CHECK-SYNTAX keyword argument is supplied and NIL, then we do not use the Nqthm readtable or enforce restrictions on the forms in the file.events. A ``flag file'' protocol is observed by PROVE-FILE if the keyword argument :WRITE-FLAG-FILES is non-NIL, as it is by default. The protocol uses three extensions of file, started, fail, and proved. When called, PROVE-FILE creates file.started and deletes both file.proved and file.fail (when they exist). An error is caused if file.proved exists and cannot be deleted. Upon successful termination, PROVE-FILE creates file.proved and deletes file.started. Upon unsuccessful termination, PROVE-FILE creates file.fail. Thus, barring interference from other users, a sure way to check for successful termination of a background execution of PROVE-FILE is to confirm that file.proved exists and was created after the PROVE-FILE commenced (since it is possible that the attempt to delete the file failed and left an error message on the terminal of the processor on which it was running). The existence of a file.fail created after the PROVE-FILE commenced is a sure way to confirm the failure of PROVE-FILE. But failures may manifest themselves by nontermination or resource exhaustion that are not detectable with the flag file protocol. When file.proved is created, certain interesting statistics are written into it. These include the total time used in processing file.events, a note on the incompatibility of the library files noted if such an incompatibility has occurred in the session (see NOTE-LIB), the names of all nondefinitional axioms involved (including those in library files noted), and the names of all events targeted by the undo-back-through command UBT during the run. The :PETITIO-PRINCIPII argument, when non-NIL, makes PROVE-FILE skip all proof obligations. Thus, with this argument set, the forms in file.events are merely assumed to be admissible (though their syntax is checked). This is a fast way to almost reconstruct the data base created by a sequence of events. The reconstruction is not perfect because the logical dependencies discovered during proofs are not recorded. It is a handy way to experiment or to recover from system crashes. However, Warning. Nqthm is unsound when the :PETITIO-PRINCIPII argument to PROVE-FILE is used. No record of the use of :PETITIO-PRINCIPII is left in the data base or in libraries created by the user from the data base constructed by PROVE-FILE. When PETITIO-PRINCIPII is non-NIL, PROVE-FILE does not observe the flag file protocol, and hence, does not create file.proved even if the run is successful. Furthermore, no MAKE-LIB is done by such a PROVE-FILE and no output occurs. The routine SKIM-FILE is a convenient way to call PROVE-FILE with PETITIO-PRINCIPII set. We conclude with some motivational remarks about PROVE-FILE and the process of creating endorsed data bases. PROVE-FILE is a weak, file-based read-eval-print loop. Why not stick with the all-powerful Common Lisp read-eval-print loop and its file-based counterpart, load? During the formalization and proof development phase of an Nqthm project, we prefer the flexibility and sense of freedom one gets from dealing directly with Lisp, rather than with some pea-brained and constraining ``user interface.'' For example, we often find ourselves executing raw Common Lisp forms to ``compute'' the Nqthm forms we wish to evaluate. We enjoy being able to type arbitrary Common Lisp forms, define Lisp utilities and readmacros, and otherwise tailor the environment to our particular tastes. We thus recommend against the casual use of PROVE-FILE in the development phase of a project. But the Common Lisp interface is ``too powerful'' when it comes to soundness. Executing (SETQ TRUE FALSE) in the host Lisp will render Nqthm unsound. More subtle forms of unsoundness can creep in, e.g., by the accidental corruption of Nqthm's data base caused by destructive list processing operations performed by utility routines written by the user. As noted on page @pageref(undo-name), one of Nqthm's own utilities, UNDO-NAME, can render the system unsound. Therefore, we do not endorse as a theorem anything ``proved'' by Nqthm in a normal interactive session. When a proving project is entirely complete, we prefer to know that no idiotic, surreptitious, or untrusted Lisp code is present that would render our efforts meaningless. Thus it makes sense to have, as we do in PROVE-FILE, a loader that prohibits the intermingling of possibly dangerous Lisp forms with trusted Nqthm forms. When we have reached the end of a project we have often constructed a single events file, say project.events, that starts with a BOOT-STRAP. If we wish to preserve the final data base of the project, as we would if other projects build upon it, we insert a (MAKE-LIB "project") at the end of the file. We then undertake to ``certify'' the event list. We start by checking that there is no file named project.proved on the directory. Then we invoke (PROVE-FILE "project"). If this terminates with the creation of project.proved we inspect its contents to see that no inadvertent axioms were added.(One can develop an Nqthm proof in a top-down fashion by using ADD-AXIOM to state the lemmas one intends later to prove. One then proceeds to derive the main result from these unproven ``lemmas.'' Upon completing the main proof, one is then obligated to replace each of the ADD-AXIOMs with a suitable event list concluding in a PROVE-LEMMA. Occasionally an ADD-AXIOM is forgotten or overlooked and finds its way into what the user thought was the completed script.) We also look for UBTs in the script because the presence of undoing in an event list can lead to such confusing results as a single name being defined two different ways (at different times). Because projects that use Nqthm can be very large, taking years to complete, and can be worked on by many people, there is often the practical necessity to divide the events into a collection of several files which are chained together by NOTE-LIBs and MAKE-LIBs. To `certify root and branch' a collection of such files using PROVE-FILE, we start by making sure that there are no lib, lisp, bin, proved, or started file extensions on the directories in question, including those referred to in the NOTE-LIB forms that occur at the beginnings of the files to be certified. (Alternatively, we check that every file ``in sight'' has extension events.) This check will prevent the use of older libraries and thus avoid the risk of using libraries that are uncertified or otherwise out of date with respect to their source files. Then we execute a sequence of PROVE-FILE commands on the event files in question in an order consistent with the inner dependencies (calling PROVE-FILE on each file exactly once). If at the end there is a proved file for each of the event files, the certification is complete. Obviously, there should be no changes permitted to any of the files in sight (except, of course, the creation of new files by PROVE-FILE) during the execution of the PROVE-FILEs. The collection of example event files distributed with Nqthm illustrates this discipline. We recommend these examples to the reader. To maintain this collection we have mechanized the certification procedure with a Lisp script, distributed as driver.lisp in the examples subdirectory. @label(endorsed) Technically speaking, an endorsed data base is a data base created, in a fresh Nqthm, by a successful execution of PROVE-FILE, provided (a) the first event in the events file is either a BOOT-STRAP or a NOTE-LIB of an endorsed data base, and (b) no ``library incompatibilities'' were noted (see NOTE-LIB). Modulo the difficulties discussed below, we believe the ``theorems'' in an endorsed data base are indeed theorems. In particular, consider any (PROVE-LEMMA name rule-classes term hints) in the endorsed data base. Let h be the sequence of axiomatic acts in the data base prior to the event in question. Then we claim h is a history (i.e., the foregoing axiomatic acts are all admissible) and term can be proved directly from the axioms of some definitional/constrain extension of h. Inadequacies. We currently know of three senses in which PROVE-FILE fails to do fully the job that we intend. (1) Common Lisp syntax for integers is not entirely fixed by the Common Lisp standards. For example, 1.7J is given as an explicit example, on p. 341 of [8], of a character sequence that is a ``potential number,'' that is, a sequence that some Common Lisp might read as a number. If a Common Lisp were to read 1.7J as an integer, e.g., as the integer 17, then by running Nqthm in that Common Lisp one could prove the theorem (EQUAL 1.7J 17). But (EQUAL 1.7J 17) might be false, or might even cause an error in Nqthm in another Common Lisp. The solution to this problem is to check with your Lisp provider that no character strings that are ``potential numbers'' read as integers, except those satisfying the normal syntax for integers shared by all Common Lisp implementations. (2) It is not clear from the Common Lisp standard what files can be created by the compilation process. Typically, if you compile project.lisp, then project.x is created, for some extension x. However, AKCL takes this freedom to a rather liberal extent: when the variable COMPILER::*SPLIT-FILES* is non-NIL, as we have been forced to set it when doing some proofs, files with names 0project.o, 1project.o, 2project.o, ..., may be created during the compilation of project.lisp. Such names create a potential for collision with the compiled library of another events file, say one named 0project.events. Thus the AKCL user of PROVE-FILE should check that the name of no events file begins with a digit. We do not make this check mechanically, as we do the check for names that end in "tmp", because it is possible that some prefix of a name supplied to PROVE-FILE is a mere directory name, e.g., 2nd-try/project. (3) Unbalanced close parentheses at the top level are treated by Common Lisp's READ in an undefined, implementation dependent way. Most Lisps we use ignore unbalanced close parentheses, but some cause an error. Such parentheses are ``invalid'' according to [8]. A perfect implementation of PROVE-FILE, we think, would check for such parentheses and cause an error. 66. PROVE-FILE-OUT General Forms: (PROVE-FILE-OUT file) and (PROVE-FILE-OUT file :CHECK-SYNTAX cs-flg :WRITE-FLAG-FILES wf-flg :PETITIO-PRINCIPII pp-flg) Example Forms: (PROVE-FILE-OUT "basic") and (PROVE-FILE-OUT "basic" :PETITIO-PRINCIPII T :WRITE-FLAG-FILES NIL) PROVE-FILE-OUT is like PROVE-FILE except it arranges for all output to go to the proofs extension of file. That is, PROVE-FILE-OUT opens the file file.proofs and calls PROVE-FILE (on the same arguments given to PROVE-FILE-OUT) in such a way as to ensure that all output is written to file.proofs. The output file is closed upon termination and represents a complete transcript of the processing of file.events. Nothing is printed to the terminal. See PROVE-FILE. 67. PROVE-LEMMA @label(PROVE-LEMMA) General Forms: (PROVE-LEMMA name rule-classes term) and (PROVE-LEMMA name rule-classes term hints) Example Form: (PROVE-LEMMA REVERSE-REVERSE (REWRITE) (IMPLIES (PROPER X) (EQUAL (REVERSE (REVERSE X)) X))) and (PROVE-LEMMA TIMES-LIST-EQUAL-FACT (REWRITE) (IMPLIES (PERM (POSITIVES N) L) (EQUAL (TIMES-LIST L) (FACT N))) ;Hints: ((USE (PERM-TIMES-LIST (L1 (POSITIVES N)) (L2 L))) (DISABLE PERM-TIMES-LIST))) PROVE-LEMMA is an event command for proving a theorem and storing it and possibly some generated rules in the data base. It does not evaluate its arguments. name must be a new name and will be made the name of the event in the data base, rule-classes must be a (possibly empty) list of rule classes and term must be a well-formed term (see TRANSLATE). PROVE-LEMMA applies the theorem prover to term, printing commentary as the proof attempt proceeds. If the proof attempt is successful, term is stored in the data base as a theorem; in addition, rules of the classes specified by rule-classes are generated from term and stored. The name of each rule is name. An error is caused if term is unsuitable for some class in rule-classes and no change is made in the data base. When formulating input for PROVE-LEMMA you must be cognizant of the rule interpretation of term in addition to its mathematical content. See Chapter 11 for a detailed explanation of the effect of each type of rule and how rules are generated from formulas and rule classes. See Chapter 13 for advice about how to use rules. Note that if rule-classes is NIL then the term is stored as a theorem and will be available for USE hints (see below) but will generate no rules. If the proof attempt succeeds, PROVE-LEMMA prints ``Q.E.D.'' and a time triple for the event and returns the name of the new event, name. If the proof attempt fails, PROVE-LEMMA prints a ``failure banner'' ************** F A I L E D ************** and then a time triple. Then it returns NIL. When the theorem prover fails the only claim made is the trivial one that our heuristics did not lead to a proof. The system's remarks should not be interpreted to mean that the input formula is not a theorem, even if the last formula printed is F: the heuristics might have generalized the input formula before failing. That said, however, two caveats are in order. First, conjectures submitted for proof are frequently not theorems. Do not be too quick to dismiss a failed proof simply because the theorem prover is so weak. It is indeed weak, but you can't fool it either. If a point were awarded the opposition each time a player asserted an inconsistent belief, the theorem prover would never lose and would, in fact, win almost every session. Second, when it fails on theorems it is frequently because the proof you had in mind involves some step that has not been made explicit by your previously proved lemmas-or at least by their interpretation as rules. See Chapter 13 where we discussed the notion of the crucial ``check points'' in a proof attempt and what you should do at each. If worse comes to worse, you can essentially tell the system your proof via the hint argument to PROVE-LEMMA, which we describe at length below. @label(hint-specs) The hints argument permits the user to give the theorem prover some guidance in its proof attempt. If nonempty, hints must be a list of tuples. The CAR of each tuple must be one of the symbols listed below, where we describe the form and effect of each acceptable tuple. An error is caused if any element of hints fails to have the correct form or if there is more than one occurrence of any kind of hint. 67.1. USE Hints General Form: (USE (name (v t ) ... (v t )) 1 1,1 1,1 1,n 1,n 1 1 ... (name (v t ) ... (v t ))) k k,1 k,1 k,n k,n k k Example Form: (USE (LEMMA1 (X (CAR A)) (Y 0)) (LEMMA2 (X (SUB1 X)) (I X) (K (FACT X)))) A USE hint essentially forces the use of one or more instances of one or more previously proved theorems, definitions, or axioms. Each pair following the symbol USE specifies the name of a formula and a substitution. The USE hint creates the indicated instantiation of each formula and adds it as an explicit hypothesis to the conjecture, term, submitted to the theorem prover. More precisely, the conditions on USE hints are as follows. Each name must i be a citizen of the data base with a non-NIL associated FORMULA in DATA-BASE. It does not matter if name is enabled or disabled or if any rules were i generated for name . Each v must be a variable symbol, each t must be a i i,j i,j term, and v must be distinct from v if j /= k. i,j i,k Provided the above conditions are met, the effect of such a USE hint on the behavior of PROVE-LEMMA is to cause a modified (but provably equivalent) conjecture to be submitted to the theorem prover. Rather than submitting term, PROVE-LEMMA submits (IMPLIES (AND thm ... thm ) term) 1 k where thm is obtained by instantiating the FORMULA for name , replacing v i i i,j by t . i,j Observe that each thm is provably non-F-each is an instance of a theorem, i definition, or axiom. Hence, the submitted formula is equivalent to the input one. However, the careful reader might also note that if name is enabled and is i a well-constructed replacement rule, there is a very high likelihood that it will be used to eliminate thm from the modified conjecture. This renders the i hint useless. It is generally a good idea to DISABLE any REWRITE rules instantiated with a USE hint. The modified conjecture is often easier to prove because the necessary instances of the necessary theorems are explicitly present. Indeed, it is possible to reduce any noninductive proof in the logic to propositional calculus and equality reasoning after supplying all the necessary instances of lemmas.[We do not recommend such a wholesale use of USE simply because the number of lemmas and instances needed would often produce a modified conjecture that was too large for the combinatorial processing done by all known propositional decision engines.] 67.2. EXPAND Hints @label(EXPAND-details) General Form: (EXPAND t ... t ) 1 n Example Form: (EXPAND (PRIME1 X (SUB1 X))) Each t must be a term of the form (fn x ... x ) where fn is a defined i 1 k function. That is, each t must be a call of a defined function. Variable i symbols, calls of shell functions, and calls of undefined or constrained functions are prohibited. The EXPAND hint forces the expansion of each t i whenever it is encountered by the rewriter. The EXPAND hint is implemented simply by putting the (translated and with certain calls of IDENTITY expanded, as described below) t on a list that is i known to the rewriter. Whenever a function call is considered for expansion the list is checked. Thus, it is not necessary that the t occur in the input i conjecture. However, it is crucial that the exact form of the intended term be written in the hint. We give an example below. Suppose (SECOND X) is defined to be (CADR X). Suppose also that (TIMES I (SECOND X)) occurs in the input conjecture and the intended proof requires its expansion but the system does not expand it automatically. An EXPAND hint is called for. The hint (EXPAND (TIMES I (SECOND X))) will not work. By the time the rewriter considers expanding the TIMES expression, it will have become (TIMES I (CADR X)). Thus, to force the expansion of (TIMES I (SECOND X)) it is necessary to give the hint (EXPAND (TIMES I (CADR X)))! This is not generally a problem. The reason is that you will generally add EXPAND hints only in response to the failure of an earlier proof attempt. In that earlier attempt the term (TIMES I (CADR X)) will have appeared at the checkpoint where you expected its expansion to appear and you will have realized ``the theorem prover needs to expand that term.'' As with the left-hand sides of REWRITE rules, it is sometimes desired to write large constants in the terms to be expanded. An alternative is to write a variable-free expression that reduces to the desired constant and to embed that expression in a call to the IDENTITY function. The EXPAND hint replaces such expressions by their reduced values before storing them on the list inspected by the rewriter. Thus, when used in an EXPAND hint, (SUM A B 4294967296) and (SUM A B (IDENTITY (EXPT 2 32))) cause identical behavior, provided EXPT is defined as the exponentiation function. The IDENTITY function is given special treatment only here, in the EXPAND hint, and in the preprocessing of REWRITE rules. Otherwise, IDENTITY is not given any special treatment by the system. 67.3. DISABLE and ENABLE Hints General Forms: (DISABLE name ... name ) 1 n and (ENABLE name ... name ) 1 n Example Form: (DISABLE LEMMA1 TIMES-2-REWRITE) The DISABLE hint has the effect of disabling the listed rule names for the duration of the proof attempt in question. The ENABLE hint is analogous. We sometimes call these hints ``local'' enables and disables because they do not affect the status of the names in the data base. The effects of these hints are visible only during the proof attempt for which the hints were supplied. Each name must be a citizen of the data base. See page i @pageref(disable-discussion) for a discussion of the effect of enabling or disabling a name and why it is done. Roughly speaking, the effect of DISABLE is to prevent the theorem prover from using any of the named rules during the current proof attempt. ENABLE permits the named rules to be used even though they might be DISABLEd in the current data base. Using the DISABLE-THEORY and ENABLE-THEORY hints, all the names in a theory can be ``locally'' disabled or enabled. This raises questions of priority, e.g., ``What if a name is DISABLEd locally with a DISABLE hint but is a member of a theory that is enabled locally?'' Such questions are addressed in the following discussion of the DISABLE-THEORY and ENABLE-THEORY hints. 67.4. DISABLE-THEORY and ENABLE-THEORY Hints General Forms: (DISABLE-THEORY theory-name ... theory-name ) 1 n and (ENABLE-THEORY theory-name ... theory-name ) 1 n Example Form: (DISABLE-THEORY LIST-THEORY BAG-THEORY) The DISABLE-THEORY hint has the effect of disabling all the names in the listed theories. The ENABLE-THEORY hint is analogous. We sometimes call these hints ``local'' enables and disables because they do not affect the status of the names in the data base. The effects of these hints are visible only during the proof attempt for which the hints were supplied. Each theory-name must be a theory name, i.e., a name introduced with i DEFTHEORY or one of the two builtin theory names, GROUND-ZERO and T. See page @pageref(disable-discussion) for a discussion of the effect of enabling or disabling a name and why it is done. If the theory name T is used then no other theory name is permitted in the hint. Furthermore, if the hint (DISABLE-THEORY T) is supplied, then (ENABLE-THEORY T) may not be supplied and vice versa. The local status of a name during a proof may thus be affected by any of four hints, DISABLE, ENABLE, DISABLE-THEORY, and ENABLE-THEORY. The following algorithm is used to determine the status of a name during a proof attempt governed by any of these hints. - If the given name is included in an ENABLE hint, consider it enabled. - Otherwise, if the given name is included in a DISABLE hint, consider it disabled. - Otherwise, if the given name belongs to some theory named in an ENABLE-THEORY hint, consider it enabled. - Otherwise, if the given name belongs to some theory named in an DISABLE-THEORY hint, consider it disabled. - Otherwise, if there is an (ENABLE-THEORY T) hint (respectively, a (DISABLE-THEORY T) hint), consider it enabled (respectively, disabled). - Otherwise, simply check whether it is enabled or disabled in the global database. Thus, roughly speaking, the hints which explicitly mention rule names, DISABLE and ENABLE, are given priority over the theory-level hints, DISABLE-THEORY and ENABLE-THEORY; enabling is given priority over disabling. For example, one may give a hint that enables several relevant theories but then one may explicitly disable certain names within those theories. 67.5. HANDS-OFF Hints General Form: (HANDS-OFF fn ... fn ) 1 n Example Form: (HANDS-OFF PLUS TIMES QUOTIENT REMAINDER) The HANDS-OFF hint prevents the rewriter from trying any rule that rewrites a term beginning with one of the function symbols listed in the hint. Each fn i must be a function symbol. Each such name is added to a list known to the rewriter. Roughly speaking, if a function symbol is on this list then every every REWRITE stored under that symbol, including its definition, is locally disabled. Because the documentation of the HANDS-OFF feature was grossly incorrect in the first edition of this handbook, we describe it somewhat more carefully. When rewriting the target term (fn a ... a ), the rewriter first rewrites 1 k each a , say to a '. The rewriter then shifts its attention to (fn a ' ... i i 1 a '), which we here call the ``intermediate term.'' If all the a ' are k i explicit values and fn has an enabled executable counterpart, rewriter returns the explicit value obtained by reducing the intermediate term. If fn is EQUAL or a shell recognizer such as NUMBERP, built in rules are tried on the intermediate term. If the intermediate term is one of several special forms having to do with V&C$, certain built-in rules are tried. See the Reference Guide entries for REWRITE-APPLY$, REWRITE-APPLY-SUBR, REWRITE-CAR-V&C$, REWRITE-CAR-V&C-APPLY$, REWRITE-EVAL$, REWRITE-V&C$, and REWRITE-V&C-APPLY$, starting on page @pageref(rewrite-apply$). Otherwise, the rewriter determines whether fn is among the fn noted in the HANDS-OFF hint. If so, the i intermediate term is returned as the result of rewriting the target term. Otherwise, the rewriter tries to apply enabled REWRITE rules matching the intermediate term, including the definition of fn. 67.6. INDUCT Hints General Form: (INDUCT (fn v ... v )) 1 n Example Form: (INDUCT (PRIME1 X Y)) The INDUCT hint forces the theorem prover immediately into the induction process. Furthermore, rather than select an induction using its heuristics, the induction used is that suggested by (fn v ... v ). fn must be a 1 n recursively defined function, and the v must be distinct variables. The i induction suggested has exactly the same case analysis as in the body of the definition of fn. Those branches not leading to recursive calls are base cases. Those branches leading to k>0 recursive calls (fn t ... t ), ..., 1,1 1,n th (fn t ... t ) have k induction hypotheses. The i induction hypothesis k,1 k,n is obtained by instantiating each v by the corresponding term t from the j i,j th i recursive call. The output produced by the theorem prover in response to an INDUCT hint is very unenlightening: it prints nothing at all but simply produces the various cases as described above and proceeds to simplify each. 67.7. DO-NOT-INDUCT General Form and Example Form: (DO-NOT-INDUCT T) If present, the DO-NOT-INDUCT T hint causes the theorem prover to abort with failure as soon as it encounters a goal for which it would otherwise enter the induction process. (The second element of the hint can, in fact, be any Lisp object and is ignored.) 67.8. DO-NOT-GENERALIZE General Form and Example Form: (DO-NOT-GENERALIZE T) If present, the DO-NOT-GENERALIZE T hint disables the entire generalization process. (The second element of the hint can, in fact, be any Lisp object and is used as the value of an internal flag. If the flag setting is NIL the hint has no effect at all. Thus, the ``General Form'' is also the ``Example Form.'') 67.9. NO-BUILT-IN-ARITH General Form and Example Form: (NO-BUILT-IN-ARITH T) If present, the (NO-BUILT-IN-ARITH T) hint prevents the built-in linear arithmetic procedure from being used. We use this hint only to demonstrate the ability (or inability) of the system to prove by heuristic means the elementary theorems about LESSP and PLUS. (The second element of the hint can, in fact, be any Lisp object and is used as the value of an internal flag. If the flag setting is NIL the hint has no effect at all. Thus, the ``General Form'' is also the ``Example Form.'') 68. R-LOOP General and Example Form: (R-LOOP) R-LOOP permits the evaluation of terms in the logic. It is a Lisp style ``read-eval-print loop'' providing certain convenient nonlogical features through so-called ``special forms.'' (Noninteractive entrances to R-LOOP are provided via the functions R and S described at the end of this section.) Upon entry to R-LOOP the system prints a header indicating the values of certain ``switch settings'' explained below. Then R-LOOP prompts the user for type-in by printing a ``*'' and then waiting until an s-expression, t, has been typed. As usual in our system, one is actually typing to the standard Lisp reader. Line editing, redisplay of previously typed input, etc., are all available as however provided by the host Lisp system. In some Lisp systems, the user must type a carriage return after the s-expression before the system actually reads it; in other systems, the final balancing close parenthesis initiates the read. Once t has been read it is evaluated under the axioms and definitions as described below, unless t is one of the special forms also noted below. The process of evaluation will yield one of three possible outcomes: an error message indicating that t is not well-formed, a message indicating that t cannot be reduced to an explicit value, or an explicit value equivalent to t. In the latter case the value is printed. In all cases, R-LOOP then iterates by prompting for another s-expression. Here is a sample exchange: *(APPEND '(1 2 3) '(4 5 6)) ;user type-in '(1 2 3 4 5 6) ;R-LOOP's response Users familiar with the Lisp ``read-eval-print'' loop will notice a slight but disconcerting difference: in Lisp the exchange would have been *(APPEND '(1 2 3) '(4 5 6)) ;user type-in (1 2 3 4 5 6) ;Lisp's response Note the absence of the ' in Lisp's response. R-LOOP deals exclusively with terms-the ``values'' printed are terms, they just happen to all be explicit values and thus, when printed in our syntax, usually are preceded by the ' mark. (Numbers, T, F, and NIL are the only explicit values displayed without use of QUOTE notation.) By ``evaluation'' we mean the reduction of a term to an explicit value by a call-by-value style interpretation of the axioms and definitions. For example, to evaluate a term of the form (PERM x y), R-LOOP recursively reduces x and y to explicit values and then (effectively) instantiates the body of PERM with those values and reduces the result.(The ``R'' in ``R-LOOP'' in fact stands for ``reduce'' as we defined it in [4].) The evaluation performed by R-LOOP takes place under an assignment of explicit values to variable symbols. R-LOOP permits the user to set this assignment with the SETQ special form. This feature is provided so that the user can save the value of one evaluation for possible input to another. Thus, if X has the value 7 and Y has the value 8 then the evaluation of (TIMES X Y) is 56. If the term t is submitted for evaluation and produces the explicit value v, then it is a theorem that (EQUAL t v), under the equality hypotheses implicit in the current asignment of values to variables. Not all terms can be reduced to explicit values. Examples are variables not assigned values in the current R-LOOP assignment (i.e., ``unbound variables'' in the programmer's sense, ``undefined abbreviations'' in the mathematician's) and calls of undefined or constrained functions. Some terms which are provably equal to explicit values cannot be reduced to that explicit value by evaluation. For example, (IF V 3 3) is provably equal to 3 but does not reduce to 3 if V is ``unbound.'' When a term submitted for evaluation cannot be reduced to an explicit value by R-LOOP, the answer ``(NOT REDUCIBLE)'' is printed. R-LOOP has two mode switches that can be set by several special forms. One of the switches determines whether evaluation is ``traced'' and, if so, how. The other determines whether abbreviations are used when values are printed out. The trace mode may be full, partial, or off. When trace mode is off, no printing occurs during the evaluation of terms. The value is printed when the evaluation has completed successfully. When trace mode is not off, printing occurs during the evaluation of each term. Trace mode prints a step-by-step proof of the equivalence of the input term and the derived value. The difference between full and partial trace mode is only how large the printed steps are. In full trace mode, every application of substitutions of equals for equals into the input term is printed. In partial trace mode, we print only the ``major'' steps associated with function expansion. Suppose we define APP as APPEND: Definition. (APP X Y) = (IF (NLISTP X) Y (CONS (CAR X) (APP (CDR X) Y))) Below we illustrate the evaluation of (APP '(A) '(1 2 3)), first with trace mode off, then in full trace mode, and then in partial trace mode. Then, we illustrate (APP '(A B C) '(1 2 3)) in partial trace mode. (R-LOOP) Trace Mode: Off Abbreviated Output Mode: On Type ? for help. *(APP '(A) '(1 2 3)) '(A 1 2 3) *FULL-TRACE Trace Mode: Full *(APP '(A) '(1 2 3)) =(IF (NLISTP '(A)) '(1 2 3) (CONS (CAR '(A)) (APP (CDR '(A)) '(1 2 3)))) =(IF F '(1 2 3) (CONS (CAR '(A)) (APP (CDR '(A)) '(1 2 3)))) =(CONS (CAR '(A)) (APP (CDR '(A)) '(1 2 3))) =(CONS 'A (APP (CDR '(A)) '(1 2 3))) =(CONS 'A (APP NIL '(1 2 3))) =(CONS 'A (IF (NLISTP NIL) '(1 2 3) (CONS (CAR NIL) (APP (CDR NIL) '(1 2 3))))) =(CONS 'A (IF T '(1 2 3) (CONS (CAR NIL) (APP (CDR NIL) '(1 2 3))))) ='(A 1 2 3) *TRACE Trace Mode: Partial *(APP '(A) '(1 2 3)) =(CONS 'A (APP NIL '(1 2 3))) ='(A 1 2 3) *(APP '(A B C) '(1 2 3)) =(CONS 'A (APP '(B C) '(1 2 3))) =(CONS 'A (CONS 'B (APP '(C) '(1 2 3)))) =(CONS 'A (CONS 'B (CONS 'C (APP NIL '(1 2 3))))) ='(A B C 1 2 3) *OK Exiting R-LOOP. NIL The output abbreviation mode may be either on or off. The mode determines how the final explicit value of a term is displayed. When output abbreviation is on, explicit values are displayed in a way that does not require use of the ugly ``*1*'' prefix. When output abbreviation mode is off, explicit values are displayed in QUOTE notation. For example, (R-LOOP) Trace Mode: Off Abbreviated Output Mode: Off Type ? for help. *(PAIRLIST '(A B C) (LIST 1 2 3)) '((A . 1) (B . 2) (C . 3)) *(PAIRLIST '(A B C) (LIST 0 T F)) '((A . 0) (B . *1*TRUE) (C . *1*FALSE)) *ABBREV Abbreviated Output Mode: On *(PAIRLIST '(A B C) (LIST 1 2 3)) '((A . 1) (B . 2) (C . 3)) *(PAIRLIST '(A B C) (LIST 0 T F)) (LIST '(A . 0) (CONS 'B T) (CONS 'C F)) *OK Exiting R-LOOP. NIL In the session above we start with abbreviated output mode off. We evaluate two PAIRLISTs. The values of both are printed in QUOTE notation. But the value of the second one requires the use of *1*TRUE and *1*FALSE. Then we enter abbreviated output mode and re-evaluate both PAIRLISTs. The value of the first one is printed just as before. But the value of the second one is not printed in QUOTE notation. Instead, LIST and CONS are used to ``unquote'' enough of the value to expose those parts that would otherwise require use of the ``*1*'' prefix. Below we list the special forms recognized by R-LOOP. The special forms are, in general, well-formed terms that are simply not treated as terms when read at the top level by R-LOOP. OK Exit R-LOOP and return to its caller. If you invoked (R-LOOP) from the Lisp command interpreter (as opposed to from within some other Lisp program), OK returns you to the Lisp command interpreter. No harm results from exiting R-LOOP via Lisp interrupt characters (see ``Aborting Commands'' page @pageref[abort]). Variable assignments in the R-LOOP assignment are maintained from one call of R-LOOP to the next. (SETQ var term) In any s-expression of this form, var should be a variable symbol and term should be a term. This special form causes term to be evaluated under the current R-LOOP assignment and, if the evaluation succeeds and produces val, the current assignment is changed so that var has the value val. In addition, val is printed. If the evaluation of term fails, no change is made to the R-LOOP assignment. TRACE Set trace mode to ``partial.'' FULL-TRACE Set trace mode to ``full.'' UNTRACE Set trace mode to ``off.'' ABBREV Turn on abbreviated output mode. UNABBREV Turn off abbreviated output mode. ? Causes R-LOOP to print out a brief summary of the available special forms. Special forms are given special treatment only when they are the top-level s-expression read by R-LOOP. If, for example, the SETQ special form is used as a proper subterm in an s-expression, it is evaluated in the usual sense of the logic. For example, suppose X is 7 in the R-LOOP assignment, and the user types the s-expression (PLUS (SETQ X 3) X) to R-LOOP. Unless the user has defined the function SETQ in the logic, this s-expression is ill-formed. If SETQ has been defined, the value of this s-expression is the value of (PLUS (SETQ 7 3) 7). The R-LOOP assignment is maintained from one call of R-LOOP to the next within a given session with the theorem prover. A typical use of R-LOOP in a session is to enter it periodically after function definitions to test the suitability of the definitions or the validity of a conjecture being formulated. The variable assignment feature is often used to store test data, e.g., the state argument of an interpreter for a programming language being formalized. The variable assignment is not written to the library files created by MAKE-LIB. Unless otherwise saved, R-LOOP assignments are lost when the Lisp session terminates. The assignment is stored in an internal form as the value of the Lisp variable R-ALIST. This value may be printed and read back in via the usual Lisp print and read programs. The Lisp routine R is the heart of R-LOOP. R takes a single s-expression as its input, translates it, reduces it with respect to R-ALIST, and returns either the special value '(NOT REDUCIBLE) or the result of introducing abbreviations back into the reduced value. The Lisp routine S takes two arguments. The first must be a Lisp symbol representing a variable in the logic and the second must be an s-expression whose translation is an explicit value. S modifies R-ALIST so that the value of the variable is the given explicit value. 69. REDUCE-TERM-CLOCK General Form: REDUCE-TERM-CLOCK This Lisp variable may be set to any integer value. Its initial value is 100. The variable is used to prevent ``infinite loops'' in the executable counterparts of partial functions. In particular, the variable specifies the number of times such a function is permitted to recur before the execution is aborted. For example, suppose that we introduce the function APP with (DEFN APP (X Y) (EVAL$ T '(IF (EQUAL X (QUOTE NIL)) Y (CONS (CAR X) (APP (CDR X) Y))) (LIST (CONS 'X X) (CONS 'Y Y)))) Then suppose we enter R-LOOP and try to evaluate (APP '(A B C) '(1 2 3)). The answer, '(A B C 1 2 3), is quickly computed. However, if we try to evaluate (APP 0 1)) we get the message: APP aborted and R-LOOP reports that the term is (NOT REDUCIBLE). Because APP was introduced without a proof of termination, its executable counterpart, *1*APP, is coded so that no more than REDUCE-TERM-CLOCK recursions are permitted. Because (APP 0 1) is undefined by the above recursion, the limit on the number of recursions is exceeded. Whenever the limit is exceeded the message APP aborted is printed by *1*APP and the term involving that computation is considered irreducible. While this seems perfectly sensible in the case of an infinite loop, like (APP 0 1), it is less attractive in cases where APP is defined but the resource limitation imposed by REDUCE-TERM-CLOCK is insufficient to permit the computation to conclude. For example, (APP '(1 2 3 ... 100) NIL) cannot be computed if the REDUCE-TERM-CLOCK is set to 100. Because the executable counterparts of defined functions are also called during proof attempts, the message that a computation has been aborted may appear in the middle of a proof attempt-even a successful proof attempt. This message is extremely annoying because it is not coordinated with the rest of the theorem prover's output and hence destroys the organization of that output. Furthermore, when the limit is set very high and a term involving an infinite loop occurs in the theorem, much time is spent in the needless attempt to evaluate the executable counterpart. In this case, time can be saved by setting REDUCE-TERM-CLOCK to some small positive integer-ideally to the depth of the maximum computation required in the proof. But we eschew such hackery because we don't like finding proofs only because of resource limitations. When we are tempted to play with the setting of REDUCE-TERM-CLOCK, we more often disable the executable counterpart of the function involved, after proving REWRITE rules that exhibit the values of the necessary computations. If REDUCE-TERM-CLOCK is set to -1 then no attempt is made to limit the recursion. This may result in Lisp stack overflows during the proofs of theorems. The value of REDUCE-TERM-CLOCK is not saved in library files created by MAKE-LIB. Thus, its value is not properly restored by NOTE-LIB. Neither is its value restored by UNDO-BACK-THROUGH. These omissions are essentially due to the fact that we do not provide an event for manipulating the value of REDUCE-TERM-CLOCK, primarily because we think it would be so rarely used. In any case, the user is entirely responsible for maintaining the setting of REDUCE-TERM-CLOCK and failure to maintain it properly can conceivably prevent previously successful events from replaying. 70. REWRITE REWRITE is one of the rule class tokens that may be given to ADD-AXIOM, CONSTRAIN, FUNCTIONALLY-INSTANTIATE or PROVE-LEMMA to indicate what kinds of rules should be generated from a formula. REWRITE rules actually come in four different forms: type prescription rules, compound recognizer rules, replacement rules, and linear arithmetic rules. All four forms are used in the simplification process, which is the first process tried. In addition, type prescription rules are used throughout the system to help determine the type of a term. It is perhaps a mistake for us to lump together into the class ``REWRITE'' all four kinds of rules. Only replacement rules cause terms to be rewritten in the way traditionally associated with term rewrite systems. If a theorem built in as a REWRITE rule fails to cause rewriting, it may be that the rules generated from the theorem were not replacement rules. @label(rewrite-apply$) 71. REWRITE-APPLY$ REWRITE-APPLY$ is the name of a special-purpose simplifier built into Nqthm. It simplifies some expressions of the form (APPLY$ (QUOTE fn) args). Roughly speaking, if fn is a symbol that names a total function, then (APPLY$ (QUOTE fn) args) is rewritten to (fn (CAR args) ... (CAD...DR args)), where the appropriate number of arguments for fn are taken from args. This simplification is justified by theorems proved in [5]. If the name REWRITE-APPLY$ is disabled, this simplifier is not used. The name is a citizen (a satellite of GROUND-ZERO) so it can be enabled and disabled. It is initially enabled. 72. REWRITE-APPLY-SUBR REWRITE-APPLY-SUBR is the name of a special-purpose simplifier built into Nqthm. It simplifies some expressions of the form (APPLY-SUBR (QUOTE fn) args). If fn is a function symbol, (SUBRP 'fn) is T and fn is not ``erratic'' as defined below, then (APPLY-SUBR (QUOTE fn) args) is rewritten to (fn (CAR args) ... (CAD...DR args)), where the appropriate number of arguments for fn are taken from args. If (SUBRP 'fn) is F, (APPLY-SUBR (QUOTE fn) args) is rewritten to F. These simplifications are justified by SUBRP axiom and Axiom 55. The notion of ``erratic'' is quite subtle. At first sight, one is tempted to agree that if (APPLY-SUBR 'fn args) is (fn (CAR args) ... (CAD...DR args)), if (SUBRP 'fn) is T. Certainly it is true for the SUBRPs that are introduced implicitly by our axiomatic acts, because we add the corresponding axiom about APPLY-SUBR as part of the ``SUBRP axiom'' (page @pageref(subrp-axiom)). But it is consistent for the user to declare a new function symbol, say, G, of no arguments, and to add axioms specifying that (SUBRP 'G) is T but (APPLY-SUBR 'G ARGS) is (NOT (G)). Then clearly it would be incorrect to simplify (APPLY-SUBR 'G args) to (G). To avoid this we introduce the notion of ``erratic'' functions. @label(erratic) A function symbol is erratic if it was introduced with DCL or CONSTRAIN or else mentions an erratic function in its BODY. Note that we sweepingly consider all declared functions erratic, rather than more carefully analyze the available APPLY-SUBR axioms. If the name REWRITE-APPLY-SUBR is disabled, this simplifier is not used. The name is a citizen (a satellite of GROUND-ZERO) so it can be enabled and disabled. It is initially enabled. 73. REWRITE-CAR-V&C$ REWRITE-CAR-V&C$ is the name of a special-purpose simplifier built into Nqthm. It simplifies some expressions of the form (CAR (V&C$ T (QUOTE term) a)). Roughly speaking, if term is a term containing no erratic symbols and the domain of the alist a is manifest, we simplify (CAR (V&C$ T (QUOTE term) a)) to the appropriate instance of term, provided (V&C$ T (QUOTE term) a) is non-F, and to 0 otherwise. This simplification is justified by theorems proved in [5]. If the name REWRITE-CAR-V&C$ is disabled, this simplifier is not used. The name is a citizen (a satellite of GROUND-ZERO) so it can be enabled and disabled. It is initially enabled. 74. REWRITE-CAR-V&C-APPLY$ REWRITE-CAR-V&C-APPLY$ is the name of a special-purpose simplifier built into Nqthm. It simplifies some expressions of the form (CAR (V&C-APPLY$ (QUOTE fn) args)). Roughly speaking, if F is not a member of args and fn is a total function other than IF, then (CAR (V&C-APPLY$ (QUOTE fn) args)) simplifies to (fn (CAAR args) ... (CAAD...DR args)). This simplification is justified by theorems proved in [5]. If the name REWRITE-CAR-V&C-APPLY$ is disabled, this simplifier is not used. The name is a citizen (a satellite of GROUND-ZERO) so it can be enabled and disabled. It is initially enabled. 75. REWRITE-EVAL$ REWRITE-EVAL$ is the name of a special-purpose simplifier built into Nqthm. It simplifies some expressions of the form (EVAL$ T (QUOTE term) a) and some expressions of the form (EVAL$ T (CONS (QUOTE fn) args) a). For example, if term is tame and the domain of the alist a is manifest, then (EVAL$ T (QUOTE term) a) is just a certain instance of term. This simplification is justified by theorems proved in [5]. If the name REWRITE-EVAL$ is disabled, this simplifier is not used. The name is a citizen (a satellite of GROUND-ZERO) so it can be enabled and disabled. It is initially enabled. 76. REWRITE-V&C$ REWRITE-V&C$ is the name of a special-purpose simplifier built into Nqthm. It simplifies some expressions of the form (V&C$ flg form a), where flg is 'LIST or form is a QUOTEd tame term. The simplification just replaces the expression by non-F in situations where propositional equivalence is sufficient. This is justified by theorems proved in [5]. If the name REWRITE-V&C$ is disabled, this simplifier is not used. The name is a citizen (a satellite of GROUND-ZERO) so it can be enabled and disabled. It is initially enabled. 77. REWRITE-V&C-APPLY$ REWRITE-V&C-APPLY$ is the name of a special-purpose simplifier built into Nqthm. It simplifies some expressions of the form (V&C-APPLY$ (QUOTE fn) args). For example, if fn is a total function other than IF and only propositional equivalence is of interest, then (V&C-APPLY$ (QUOTE fn) args) is non-F provided F is not in args. This is justified by theorems proved in [5]. If the name REWRITE-V&C-APPLY$ is disabled, this simplifier is not used. The name is a citizen (a satellite of GROUND-ZERO) so it can be enabled and disabled. It is initially enabled. 78. Root Names See the discussion of File Names on page @pageref[file-names]. 79. Rule Classes A rule class is one of the symbols REWRITE, ELIM, or GENERALIZE or else a list of the form (META fn ... fn ) where each fn is the name of a function in the 1 n i logic. Rule classes are used to specify how a given axiom or theorem is to be stored as a rule in the data base. In Chapter 11 we describe in detail how rules are generated from formulas. 80. SET-STATUS @label(set-status) General Form: (SET-STATUS name citizens action-alist) Example Form: (SET-STATUS CLOSE-OFF-LAYER1 T ((BOOT-STRAP INITIAL) (ADD-SHELL ENABLE) ((DEFN *1*DEFN) ENABLE) (OTHERWISE DISABLE))) SET-STATUS is an event command that sweeps over a list of citizens and performs an action that may alter the enabled/disabled status of the citizen as a function of the type of event that introduced the citizen. See DISABLE for a general discussion of the effect and motivation behind enabling or disabling a name. See DEFTHEORY for a general discussion of the use of theories. SET-STATUS does not evaluate its arguments. The first argument, name, must be a new name. The second argument, citizens, denotes some list of citizens and must be of one of the forms below: - a theory name (as defined with DEFTHEORY or one of the builtin theory names GROUND-ZERO and T), denoting the value of the theory; - a list of citizens denoting itself; or - a pair of the form (ev . ev ) containing two event names, ev and 1 2 1 ev , denoting all of the citizens introduced in the inclusive 2 chronological interval bounded on one end by the event ev and on 1 the other by ev . 2 Note that when an event pair is used, choice of order is unimportant. Finally, the third argument, action-alist, must be a list of doublets, each of the form (key val), where each key is either a member of the set of words {BOOT-STRAP ADD-SHELL DEFN *1*DEFN ADD-AXIOM PROVE-LEMMA CONSTRAIN FUNCTIONALLY-INSTANTIATE OTHERWISE} or else is a proper list of members of that set, and each val is a member of the set {ENABLE DISABLE AS-IS INITIAL}, and where the following restrictions apply: - no key word may occur twice in action-alist, - the val INITIAL may be paired only with the key BOOT-STRAP, and - the last element of action-alist must have OTHERWISE as its key. The action-alist is used to determine a ``status action'' for citizens of the data base, as follows. If the citizen is the name of the executable counterpart of a function introduced with DEFN, then the status action is the val associated with the key *1*DEFN in action-alist, if there is one, and otherwise is the val associated with the key OTHERWISE. If the citizen is not such an executable counterpart, then its status action is the val associated with the kind of event command that created the citizen, if that key appears in the action-alist, and otherwise is the val associated with OTHERWISE. SET-STATUS creates a new event, named name. The only other effect of SET-STATUS is possibly to change the enable/disable status of the citizens in the list denoted by citizens. The new status is determined by the status action for the name. If the action is ENABLE, the citizen is made enabled by SET-STATUS. If the action is DISABLE, the citizen is made disabled by SET-STATUS. If the action is AS-IS the citizen's status is unchanged. Finally, if the action is INITIAL then the citizen was created by BOOT-STRAP and its status is restored to what it was at the conclusion of BOOT-STRAP. For example, the example command (SET-STATUS EXAMPLE (PRIME-FACTORS . GROUND-ZERO) ((BOOT-STRAP INITIAL) (ADD-SHELL ENABLE) ((DEFN *1*DEFN) ENABLE) ((PROVE-LEMMA ADD-AXIOM) DISABLE) (OTHERWISE AS-IS))) will create a new event named EXAMPLE and will possibly affect the status of all the names introduced in the inclusive interval from GROUND-ZERO through PRIME-FACTORS. In particular, it will leave all the satellites of GROUND-ZERO with the same status they had after the BOOT-STRAP that created them, it will enable all the satellites of all ADD-SHELLs, it will enable all defined functions and their executable counterparts, it will disable all PROVE-LEMMAs and ADD-AXIOMs, and it will leave all other citizens unchanged. Thus, for example, no FUNCTIONALLY-INSTANTIATE event is affected by this SET-STATUS A common use of SET-STATUS is in its guise as DISABLE-THEORY and ENABLE-THEORY, where it is used to set the status of all the names in a given theory. We find that big proof projects often proceed in stages. During one particular stage, a certain collection of theories is heavily used, while in a later stage, a different collection of theories is needed. While one can manage this with local hints, it may be preferable (depending on the extent of each stage) to use global commands to configure the system to use the right rules automatically. At the end of a stage one then disables the now uninteresting theories and develops and enables the appropriate new ones. In such projects we find useful such SET-STATUS commands as the following one. (SET-STATUS END-OF-STAGE-1 T ((BOOT-STRAP INITIAL) ((ADD-SHELL DEFN *1*DEFN) ENABLE) (OTHERWISE DISABLE))) This command essentially erects a barrier between one stage and the next. It restores the primitive rules (including shell rules) to their normal status, enables all definitions and executable counterparts, and disables everything else. Thus, the possibly hundreds of rules proved during ``stage 1'' are now inactive and we are ready to begin a completely new stage. If we find that we need rules that were proved during stage 1, we enable them explicitly when we discover they are needed. The reason we enable function symbols is that if we mention them in our subsequent work we will likely want them to behave as though we had just defined them; and if we do not mention them, their being enabled does not hurt us. Of course, we might want to DISABLE explicitly certain functions. Warning. In an effort to be efficient, SET-STATUS does not touch the status recorded for a name unless it must change it. This has a bizarre interaction with UNDO-NAME that is best explained by illustration. First, forget about SET-STATUS and consider how DISABLE events (actually, TOGGLE events) affect the status of a name. Suppose NAME is initially enabled and that at event a it is disabled by (DISABLE NAME). Suppose some theorems are proved after a but no status events occur. Finally, suppose that another (DISABLE NAME) occurs at event b. Clearly, NAME is disabled after b. But suppose event a is undone with UNDO-NAME. What then is the status of NAME? The answer is that NAME is still disabled because event b disabled it and has not been undone or overridden. Now consider the same scenario but this time use two SET-STATUS commands instead of the two DISABLE commands. For example, event a might be (SET-STATUS a (NAME . NAME) ((OTHERWISE DISABLE))) and b might be analogous. Because NAME is already disabled when event b is executed, event b has no effect on NAME. Thus, when a is undone with UNDO-NAME the status of NAME changes from disabled to enabled even though there is a subsequent SET-STATUS at event b that would have disabled it had event b actually been executed in the new context. We could have implemented SET-STATUS like TOGGLE so that it records the desired status regardless of the old status. We chose this implementation for efficiency: SET-STATUS is often used to map over thousands of names, many of which have already been disabled by previous sweeping SET-STATUS commands. We felt free to implement it this way, despite the difficulties with UNDO-NAME, because UNDO-NAME is already known not to maintain the integrity of the data base (see @pageref[undo-caveat). ] 81. SET-TIME-LIMIT General Forms: (SET-TIME-LIMIT) and (SET-TIME-LIMIT n) Example Form: (SET-TIME-LIMIT 10) SET-TIME-LIMIT is a Lisp routine that sets a limit on the amount of time that may be spent in the theorem prover. When the system notices that it has exceeded the limit, an error is signalled. When n is supplied, it must be a positive integer representing the time limit in seconds. (SET-TIME-LIMIT n) installs n as the limit. (SET-TIME-LIMIT) removes the limit. The system initially has no limit. The limit is not part of the data base and is not saved in library files. Thus, if you want a time limit during a given session, you must invoke SET-TIME-LIMIT in that session. Time limits are checked only during rewriting. There are other time-consuming loops in our system, such as ``clausification.'' Because of this, it is possible (but unusual) for the system to run considerably longer than the allotted time. 82. SKIM-FILE @label(skim-file) General Forms: (SKIM-FILE file) and (SKIM-FILE file :CHECK-SYNTAX cs-flg) Example Form: (SKIM-FILE "basic") SKIM-FILE is a convenient way to call PROVE-FILE with the :PETITIO-PRINCIPII keyword argument set to T and the :WRITE-FLAG-FILES keyword argument set to NIL. SKIM-FILE prints a message to the terminal before calling PROVE-FILE; the message reminds the user that SKIM-FILE may render Nqthm inconsistent and that output is suppressed while skimming. See PROVE-FILE (page @pageref(prove-file)) for details and pay special attention to the warning about :PETITIO-PRINCIPII. Roughly speaking, the effect of SKIM-FILE is to process all the event forms in file, merely assuming their admissibility. SKIM-FILE evaluates its arguments. The first argument, file, should be a file root name (see page @pageref(file-names)) and file.events, the events extension of file, should exist and contain Nqthm event commands as described in the documentation of PROVE-FILE. The keyword argument is optional; its meaning is as described in PROVE-FILE. 83. Time Triple A time triple is a triple of numbers printed at the end of event commands and indicating the amount of time used. The printed form of the triple is [ pre-post prove output ] where pre-post is the number of seconds spent verifying the syntactic preconditions of the command and generating and adding the appropriate rules to the data base, prove is the number of seconds spent in formal proof, and output is the number of seconds spent printing information to the user. For example, in a DEFN command, pre-post includes the time taken to check that the body of the definition involves no free variables, etc., as well as the time to preprocess the definition to compute such information as the induction schemes suggested; prove is the time taken to prove the admissibility formulas; and output is the time taken to print the message associated with acceptance of a definition. 84. THM Mode THM mode refers to the set of axioms added by BOOT-STRAP. The system can be brought up so that it supports a constructive variant of the logic described here. This is in fact the logic supported by our system before we introduced the nonconstructive function V&C$ and the quantifier FOR. See the discussion of BOOT-STRAP on page @pageref(THM-mode). 85. TOGGLE General Form: (TOGGLE new-name old-name flg) Example Forms: (TOGGLE TIMES-2-REWRITE-OFF TIMES-2-REWRITE T) and (TOGGLE REVERSE-ON REVERSE NIL) TOGGLE is an event command for setting the status of a citizen in the data base. new-name must be a new event name, old-name must be a citizen, and flg should be T or NIL. The name of the new event created is new-name. The effect of the event is to set the status of old-name to DISABLED if flg is T and to ENABLED if flg is NIL. TOGGLE then prints a time triple and returns new-name. The event commands DISABLE and ENABLE are both abbreviations for TOGGLE events. For details on the effect of disabling and enabling names, see the discussion of DISABLE. 86. TOGGLE-DEFINED-FUNCTIONS General Form: (TOGGLE-DEFINED-FUNCTIONS new-name flg) Example Form: (TOGGLE-DEFINED-FUNCTIONS DISABLE-ALL-COUNTERPARTS T) TOGGLE-DEFINED-FUNCTIONS is an event command. Its arguments are not evaluated. Roughly speaking, this command allows you to disable, globally, all executable counterparts, i.e., prevent all functions from automatically evaluating on explicit values. The first argument, new-name, must be a new event name. The second argument, flg, must be either T or NIL. The command sets the ``executable counterparts disabled'' flag of the data base to flg, creates a new event named new-name, prints a time triple, and returns new-name. The effect of the ``executable counterparts disabled'' flag is that, when non-NIL, no executable counterpart, other than shell constructors and base functions, are used during proofs. Thus, if the executable counterparts disabled flag is T, the expression (PLUS 3 4), for example, would not simplify to 7, except by repeated expansion of the definitional axiom or by REWRITE rules. Technically speaking, the flag is not stored explicitly in the data base. Instead, the node for new-name is stored, and the most recently executed TOGGLE-DEFINED-FUNCTIONS event in the graph determines the value of the flag. 87. TRANSLATE General Form: (TRANSLATE x) Example Form: (TRANSLATE '(TIMES X Y (CADDR U))) TRANSLATE is the Lisp procedure that maps user type-in into a well-formed term, or causes an error. The argument is evaluated. The value is then explored, abbreviations are expanded, and the result is checked for well-formedness. TRANSLATE returns the internal representation of the given term. We include TRANSLATE in this documentation simply so that you can experiment with the features of the Lisp reader to which you are typing. In Appendix I and example file examples/basic/parser.events we provide a formal definition of a function named TRANSLATE, corresponding to our notion in Chapter @ref(logic) of ``well-formedness'' and ``translation.'' The Lisp procedure TRANSLATE and the logical function TRANSLATE in Appendix I are closely related but are not identical. Both check for well-formedness. The Lisp procedure signals its absence with an error while the logical function returns F. But when the input is well-formed, the Lisp translator returns a term in our internal form while the logical function returns the formal term it denotes. In our internal form, all explicit value terms are represented in QUOTE notation. But the whole purpose of the logical translator is to explicate that notation by exhibiting the (often huge) nest of formal constructors. Thus, when '(ADD1 1) is given to the Lisp translator, (QUOTE 2) is returned. But when '(ADD1 1) is given to the logical translator, (ADD1 (ADD1 (ZERO))) is returned. 88. UBT General Forms: (UBT) and (UBT x) Example Forms: (UBT REVERSE) and (UBT 3) UBT is an abbreviated form of UNDO-BACK-THROUGH. The argument, x, is not evaluated and must be either an event name or a nonnegative integer. If x is th an integer it defaults to the x element of CHRONOLOGY (0-based counting, starting with the most recent event name). If no argument is provided, x defaults to the most recent event name. UBT removes from the data base every event from the most recent through x. The list of events forms removed, in chronological order, is stored in the global Lisp variable UNDONE-EVENTS. The list of events is suitable as the events argument to PROVEALL or DO-EVENTS; re-evaluating those events will reconstruct the data base. UBT returns the name of the oldest event removed, i.e., x or the name to which x defaulted. UBT is guaranteed to restore the data base to the state it was in immediately before event x was created. Using UBT thus preserves the integrity of the data base. UNDO-NAME may not. See page @pageref(undo-caveat). 89. UNBREAK-LEMMA General Forms: (UNBREAK-LEMMA x) or (UNBREAK-LEMMA) Example Form: (UNBREAK-LEMMA 'REVERSE-REVERSE) The argument, x, is optional. If supplied, it is evaluated. If x is the name of a rule that is being monitored, it is removed from the list of monitored rules. See BREAK-LEMMA. If x is NIL or not supplied, all rules are removed from the list of monitored rules. 90. UNDO-BACK-THROUGH General Form: (UNDO-BACK-THROUGH x) Example Form: (UNDO-BACK-THROUGH 'REVERSE) The argument, x, is evaluated and must be an event name. UNDO-BACK-THROUGH removes from the data base every event from the most recent through x. UNDO-BACK-THROUGH returns the list of event forms removed from the data base, in chronological order. The list returned is suitable as the events argument to PROVEALL or DO-EVENTS; re-evaluating those events will recreate the data base. UNDO-BACK-THROUGH is guaranteed to restore the data base to the state it was in immediately before event x was created. Using UNDO-BACK-THROUGH thus preserves the integrity of the data base. UNDO-NAME may not. See page @pageref(undo-caveat). 91. UNDO-NAME @label(undo-name) General Form: (UNDO-NAME name) Example Form: (UNDO-NAME 'REVERSE) The argument, x, is evaluated and must be an event name. UNDO-NAME removes from the data base x and ALL-DEPENDENTS of x (see the discussion of DATA-BASE on page @pageref(DATA-BASE)). UNDO-NAME returns the list of event forms removed from the data base, in chronological order. The list returned is suitable as the events argument of DO-EVENTS. Wishfully speaking, UNDO-NAME removes from the data base x and all of its logical dependents. This is in fact often the case, but we do not guarantee that it is always the case. The problem, as noted on page @pageref(undo-caveat), is that the theorem prover cannot track every use of certain kinds of rules and hence ALL-DEPENDENTS may not actually include all dependents. For this reason, UNDO-NAME prints a rather tiresome WARNING message every time it is called upon to remove any but the most recent event. UNDO-NAME is in fact correct when it removes only the most recent event and, more generally, when the events removed are those erased by UNDO-BACK-THROUGH. Warning: Because UNDO-NAME may not maintain the integrity of the data base, we do not endorse any proof constructed in a session in which UNDO-NAME has been used. We discuss the notion of an ``endorsed data base'' on page @pageref(endorsed). Notwithstanding the foregoing caveat, it should be said that in day-to-day interaction with the theorem prover we make heavy use of UNDO-NAME. A common situation is to have defined a function, fn, differently than intended but not discover it until several dependent events (e.g., functions using fn) have been created. When we discover the discrepancy our usual response is to execute (SETQ XXX (UNDO-NAME 'fn)) which undoes the introduction of fn and all of its dependents but leaves in place any events not dependent on fn. The Lisp variable XXX above is set to the list of events undone, starting with fn. Then we define fn ``properly.'' Finally, we execute (DO-EVENTS (CDR XXX)) which attempts to reconstruct the dependents of the old fn on top of the new definition of fn. The CDR above is necessary to skip past the first event of XXX, which is the old definition of fn. Of course, the DO-EVENTS may not succeed: the new definition of fn may not have the right properties. More often when the DO-EVENTS fails it is because proofs constructed the first time those events were processed cannot be found now because of additions to the data base that were not undone. The most common situation is that names that were enabled when the original events were processed are now disabled, or vice versa. It sometimes happens that rules added to the data base since the original definition of fn now lead the theorem prover astray. In general, we make free use of UNDO-NAME, behaving exactly as though it satisfied its wishful specification. However, after several days of such interactive work, and always upon reaching our final goal, we replay the entire list of events created since the last event in some endorsed data base. One way to ``replay'' an appropriate event sequence is to use UNDO-BACK-THROUGH to roll back to some endorsed event and simultaneously collect the event forms since then. Then PROVEALL or DO-EVENTS may be used to re-evaluate the events. However, our standard way of ensuring that Nqthm endorses our final goal is to use PROVE-FILE on the script file that we build as the permanent record of the project. See PROVE-FILE (page @pageref(prove-file)) for a discussion of the issues surrounding ``endorsement.'' PROVE-FILE also creates a coherent file containing all the proofs. We have never been burned by our use of UNDO-NAME and recommend its use provided its shortcomings are fully understood. To illustrate how badly UNDO-NAME can burn you we offer the following command sequence which concludes with a proof that T = F. (DEFN FN () 23) (PROVE-LEMMA FN-ARITY-IS-0 NIL (NLISTP (FORMALS 'FN))) (UNDO-NAME 'FN) (DEFN FN (X) 45) (PROVE-LEMMA FN-ARITY-IS-NON-0 NIL (LISTP (FORMALS 'FN))) (PROVE-LEMMA SURPRISE NIL (EQUAL T F) ((USE (FN-ARITY-IS-0) (FN-ARITY-IS-NON-0)))) The problem, of course, is that the UNDO-NAME above does not remove from the data base the theorem FN-ARITY-IS-0 because its dependence on FN is not recorded since neither the statement of the theorem nor the proof involve the function symbol FN. References 1. W. Bevier. A Verified Operating System Kernel. Ph.D. Th., University of Texas at Austin, 1987. 2. R.S. Boyer, D.M. Goldschlag, M. Kaufmann, J S. Moore. Functional Instantiation in First-Order Logic. Tech. Rept. Technical Report 44, Computational Logic, Inc., 1717 W. Sixth Street, Suite 290, Austin, TX 78703, October, 1989. 3. R.S. Boyer, D. Goldschlag, M. Kaufmann, J S. Moore. Functional Instantiation in First Order Logic. In Artificial Intelligence and Mathematical Theory of Computation: Papers in Honor of John McCarthy, V. Lifschitz, Ed., Academic Press, 1991, pp. 7-26. 4. R. S. Boyer and J S. Moore. Metafunctions: Proving Them Correct and Using Them Efficiently as New Proof Procedures. In The Correctness Problem in Computer Science, R. S. Boyer and J S. Moore, Eds., Academic Press, London, 1981. 5. R. S. Boyer and J S. Moore. "The Addition of Bounded Quantification and Partial Functions to A Computational Logic and Its Theorem Prover". Journal of Automated Reasoning 4, 2 (1988), 117-172. 6. Matthew Kaufmann. A User's Manual for an Interactive Enhancement to the Boyer-Moore Theorem Prover. Technical Report 19, Computational Logic, Inc., May, 1988. 7. J. R. Shoenfield. Mathematical Logic. Addison-Wesley, Reading, Ma., 1967. 8. G. L. Steele, Jr. Common Lisp The Language. Digital Press, 30 North Avenue, Burlington, MA 01803, 1984. 9. G. L. Steele, Jr. Common Lisp The Language, Second Edition. Digital Press, 30 North Avenue, Burlington, MA 01803, 1990. 10. W. Teitelman. INTERLISP Reference Manual. Xerox Palo Alto Research Center, 3333 Coyote Hill Road, Palo Alto, Ca., 1978. Table of Contents 1. A Precise Description of the Logic 2. Apologia 3. Outline of the Presentation 4. Formal Syntax 4.1. Terminology about Terms 4.2. Terminology about Theories 5. Embedded Propositional Calculus and Equality 5.1. Propositional Calculus with Equality 5.2. The Axioms for TRUE, FALSE, IF, and EQUAL 5.3. The Propositional Functions 6. The Shell Principle and the Primitive Data Types 6.1. Conventions 6.2. The Shell Principle 6.3. Natural Numbers-Axioms 12.n 6.4. Ordered Pairs-Axioms 19.n 6.5. Literal Atoms-Axioms 20.n 6.6. Negative Integers-Axioms 21.n 7. Explicit Value Terms 8. The Extended Syntax 8.1. Token Trees and Their Display 8.2. Readable Token Trees, S-Expressions and Readmacro Expansion 8.3. Some Preliminary Terminology 8.4. Well-Formed S-Expressions and Their Translations 8.5. QUOTE Notation 8.6. *1*QUOTE Escape Mechanism for User Shells 8.7. The Definition of the Extended Syntax 9. Ordinals 10. Useful Function Definitions 10.1. Boolean Equivalence 10.2. Natural Number Arithmetic 10.3. List Processing 11. The Formal Metatheory 11.1. The Quotation of Terms 11.2. V&C$ and EVAL$ 11.3. The SUBRP and non-SUBRP Axioms 12. Quantification 12.1. The Definition of FOR and its Subfunctions 12.2. The Extended Syntax for FOR-Abbreviations II 13. SUBRPs and non-SUBRPs 14. Induction and Recursion 14.1. Induction 14.2. The Principle of Definition 15. Contraints and Functional Instantiation 16. Reference Guide 17. Aborting or Interrupting Commands 18. ACCUMULATED-PERSISTENCE 19. ADD-AXIOM 20. ADD-SHELL 21. AXIOM 22. BACKQUOTE-SETTING 23. BOOT-STRAP 24. BREAK-LEMMA 25. BREAK-REWRITE 26. CH 27. CHRONOLOGY 28. COMMENT 29. COMPILE-UNCOMPILED-DEFNS 30. CONSTRAIN 31. DATA-BASE 32. DCL 33. DEFN 34. DEFTHEORY 35. DISABLE 35.1. A Bolt from the Blue 35.2. Nonrecursive Definitions 35.3. Hierarchical Rule Development 36. DISABLE-THEORY 37. DO-EVENTS 38. DO-FILE 39. ELIM 40. ENABLE 41. ENABLE-THEORY 42. Errors 43. Event Commands 44. EVENTS-SINCE 45. Executable Counterparts 46. Explicit Values 47. Extensions 48. FAILED-EVENTS 49. File Names 50. FUNCTIONALLY-INSTANTIATE 51. Functional Substitution 52. GENERALIZE 53. Hints to PROVE-LEMMA, CONSTRAIN and FUNCTIONALLY-INSTANTIATE 54. Hints to DEFN 55. LEMMA 56. MAINTAIN-REWRITE-PATH 57. MAKE-LIB 58. META 59. Names-Events, Functions, and Variables 60. NOTE-LIB 61. NQTHM Mode 62. PPE 63. PROVE 64. PROVEALL 65. PROVE-FILE 66. PROVE-FILE-OUT 67. PROVE-LEMMA 67.1. USE Hints 67.2. EXPAND Hints 67.3. DISABLE and ENABLE Hints 67.4. DISABLE-THEORY and ENABLE-THEORY Hints 67.5. HANDS-OFF Hints 67.6. INDUCT Hints 67.7. DO-NOT-INDUCT 67.8. DO-NOT-GENERALIZE 67.9. NO-BUILT-IN-ARITH 68. R-LOOP 69. REDUCE-TERM-CLOCK 70. REWRITE 71. REWRITE-APPLY$ 72. REWRITE-APPLY-SUBR 73. REWRITE-CAR-V&C$ 74. REWRITE-CAR-V&C-APPLY$ 75. REWRITE-EVAL$ 76. REWRITE-V&C$ 77. REWRITE-V&C-APPLY$ 78. Root Names 79. Rule Classes 80. SET-STATUS 81. SET-TIME-LIMIT 82. SKIM-FILE 83. Time Triple 84. THM Mode 85. TOGGLE 86. TOGGLE-DEFINED-FUNCTIONS 87. TRANSLATE 88. UBT 89. UNBREAK-LEMMA 90. UNDO-BACK-THROUGH 91. UNDO-NAME