Nqthm-1992 Logic and Reference Guide
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