Internal Note #157
Computational Logic, Inc.
October 17, 1989
** Draft **
A User's Manual for RCL
** DRAFT **
Matt Kaufmann
[This work was supported in part at Computational Logic, Inc.,
by the Defense Advanced Research Projects Agency, ARPA Orders
6082 and 9151. The views and conclusions contained in this
document are those of the author(s) and should not be interpreted
as representing the official policies, either expressed or
implied, of Computational Logic, Inc., the Defense Advanced
Research Projects Agency or the U.S. Government.]
Table of Contents
1. Introduction . . . . . . . . . . . . . . . . . . . . 1
2. DEFUN-RCL . . . . . . . . . . . . . . . . . . . . . . 1
3. DEFMACRO-RCL . . . . . . . . . . . . . . . . . . . . 3
4. DO-RCL . . . . . . . . . . . . . . . . . . . . . . . 4
5. TAGBODY . . . . . . . . . . . . . . . . . . . . . . . 5
6. PROCLAIM-RCL . . . . . . . . . . . . . . . . . . . . 6
6.1. SPECIAL proclamations . . . . . . . . . . . . . . 6
6.2. FORCE-AUXILIARY-FUNCTIONS proclamations . . . . . 6
6.3. INHIBIT-AUXILIARY-LEMMAS proclamations . . . . . 6
6.4. POSTPROCESS-DEFNS proclamations . . . . . . . . . 7
7. DECLARE . . . . . . . . . . . . . . . . . . . . . . . 8
7.1. HINTS declarations . . . . . . . . . . . . . . . 9
7.2. FUNCTIONS declarations . . . . . . . . . . . . . 9
7.3. EVENTS declarations . . . . . . . . . . . . . . . 9
7.4. POSTPROCESS declarations . . . . . . . . . . . . 9
8. GLOBAL SWITCHES AND UTILITIES . . . . . . . . . . . . 10
8.1. The switch *UNWIND-PROTECT-IN-RUN-RCL-EVENTS-FLG* 10
8.2. The switch *PRINT-SIMPLIFICATION-INFO-FLG* . . . 10
8.3. The switch *INSTRUMENT-FLG* . . . . . . . . . . . 11
8.4. The utility UBT-RCL . . . . . . . . . . . . . . . 11
8.5. The utility RCL-STATUS . . . . . . . . . . . . . 11
9. THE ALGORITHM . . . . . . . . . . . . . . . . . . . . 11
9.1. Creating the initial DEFNs . . . . . . . . . . . 11
9.2. Errors: The ERR function . . . . . . . . . . . . 12
9.3. Simplification of RCL state data structures . . . 13
9.4. Mutual recursion analysis . . . . . . . . . . . . 13
9.5. Trimming definitions . . . . . . . . . . . . . . 13
9.6. Eliminating superfluous parameters . . . . . . . 14
9.7. Recursion elimination . . . . . . . . . . . . . . 14
1. Introduction
This note is an update and extension of CLI Internal Note 110,
[1]. That note gives an introduction to an earlier version of
the Rose Common Lisp (RCL) system, which is a verification system
for a subset of Common Lisp in the following sense. The syntax
of the RCL language is a subset of the syntax of Common Lisp (as
defined by the Common Lisp manual [2]). The semantics of the RCL
language is consistent with the description in [2].
Soon there will be a technical report [3] that gives a more
rigorous account of the soundness of the RCL system. Actually, a
by-product of the approach in this note is a rather thorough (if
informal) account of semantic issues. Nevertheless, this note is
simply an attempt to document carefully how to use the RCL system
in its current form. A quick summary of the semantics of our
system is that it allows one to verify partial correctness of
programs in the usual sense, i.e. one proves properties that hold
of programs when they terminate in other than an error state.
The prerequisites for using this system are a working
knowledge of the Boyer-Moore theorem prover [4] and a little
knowledge of Common Lisp [2].
There are three basic ``commands'' of Common Lisp that are
supported in RCL: DEFUN-RCL, DEFMACRO-RCL, and PROCLAIM-RCL (for
proclaiming of special variables and other global state
settings). It is also permitted to submit several DEFUN-RCL and
DEFMACRO-RCL forms by using the command DO-RCL. The next three
sections document DEFUN-RCL and DEFMACRO-RCL and their
generalization DO-RCL. After that comes a discussion of how the
system handles TAGBODY forms. This is followed by sections that
describe the general PROCLAIM and DECLARE mechanisms, as well as
the various global switches and utilities that are available to
the user. We conclude with a summary of the algorithm that we
use, concentrating especially on the simplifications
(optimizations) that are performed.
First though, let us point out that all this is built on top
of the Boyer-Moore Theorem Prover [5, 4], also known as NQTHM,
and in fact is actually built on top of PC-NQTHM [6, 7], an
interactive ``proof-checker'' enhancement of NQTHM. There have
been a few modifications in the NQTHM database structure to
support RCL, but these shouldn't really be visible to the user.
However, one is not allowed to use NOTE-LIB inside RCL to read in
a library made under NQTHM (or PC-NQTHM) without RCL loaded, nor
is one allowed to use NOTE-LIB inside NQTHM (or PC-NQTHM) to read
in a library made under RCL.(implementation detail: we ensure
this by creating a different THEOREM-PROVER-LIBRARY-VERSION for
RCL) However, it's important to note that RCL is started up with
a library called startup loaded in, and hence the BOOT-STRAP
command should not be invoked.(We will probably explicitly
disallow BOOT-STRAP in future versions.) The startup library has
been built on top of libraries for bags, natural numbers,
integers, and vectors (really, lists with vector-type
operations), as documented in [8] and recently updated by Bill
Bevier and Matt Wilding.
We ignore system issues here, except to say that at CLInc, one
may start up this system by giving the shell command rcl.
Perhaps the most important modification of the NQTHM
implementation is that the definition of a legal name has been
altered. More precisely, the definition(of NQTHM's Lisp function
LEGAL-CHAR-CODE-SEQ, actually) has been altered so that
lower-case characters are now legal, and there are no special
restrictions on the first character of a symbol (other than the
restrictions on all the characters) except for one small one: if
the first character is `*' then the second character may not be
any of the characters `0' through `9'.(This is to avoid, at the
very least, name conflicts with the executable counterparts of
NQTHM functions. These functions all are of the form *1*.
This restriction also guarantees that *!*QUOTE is not an evg,
which is important in order for the DEFMACRO-RCL macros to expand
as expected.)
Actually, we also allow one additional non-alphanumeric
character in our symbols, namely, the period (.). However, when
a symbol appears in RCL code it is not allowed to start with a
period. We reserve such symbols for system use, in particular
.RCL-FLG, .MUTUAL-FLG, and .PLISTS (as described in the sections
that follow).
REMARK. The convention in this note is that all input is in
lower case. All list expressions in the output are in upper
case.
ACKNOWLEDGEMENTS I'd like to thank my colleagues at
Computational Logic, Inc., for pleasant and useful interactions.
In particular, Larry Smith provided lots of useful feedback
during the development of the current version of this system, and
Larry Akers, Bob Boyer, and J Moore also were extremely helpful
on a number of occasions.
2. DEFUN-RCL
Syntax: (defun-rcl {decl} {form}*)
Here, the syntactic restrictions on are the same as those
for NQTHM function names, but modified as described at the end of
the preceding section. For the discussion of DEFUN-RCL in this
section we'll ignore the issue of declarations (denoted {decl} in
the display above), returning to that in Section 7.(In the
current implementation we only allow at most one DECLARE form per
definition, which may however have many individual declarations;
see Section 7. However, we expect to remove this restriction in
a future implementation.)
The result of executing this form is the creation of an NQTHM
DEFN event with name *CL-. (In fact there can be more then
one event, as will be explained in Sections 5 and 7. But in the
simplest cases, where the system defaults are used and there are
no DECLARE forms or TAGBODY forms, a single NQTHM DEFN event is
created.) Moreover, as we will explain below, the DEFN has at
least one extra formal parameter, .RCL-FLG. For example, if the
user submits the command
>(defun-rcl app (x y)
(if (consp x)
(cons (car x) (app (cdr x) y))
y))
then the system responds by creating and executing an NQTHM DEFN
event:
Used no non-boot-strap lemmas or functions in the simplification process.
(DEFN *CL-APP
(.RCL-FLG X Y)
(IF (EQUAL .RCL-FLG T)
(IF (LISTP X)
(CONS (CAR X) (*CL-APP T (CDR X) Y))
Y)
F))
Linear arithmetic and the lemma CDR-LESSP establish that the measure
(COUNT X) decreases according to the well-founded relation LESSP in each
recursive call. Hence, *CL-APP is accepted under the principle of definition.
Note that:
(OR (OR (FALSEP (*CL-APP .RCL-FLG X Y))
(LISTP (*CL-APP .RCL-FLG X Y)))
(EQUAL (*CL-APP .RCL-FLG X Y) Y))
is a theorem.
[ 4.1 0.1 0.1 ]
*CL-APP
T
>
Recall that we call APP the corresponding NQTHM function for APP.
Let's observe that the system can easily prove
(prove-lemma *cl-app-append
(rewrite)
(equal (*cl-app t x y)
(append x y)))
Here then, briefly, is a description of the correspondence
between this DEFUN-RCL and this DEFN; again, we refer the reader
to [3] for a more rigorous explanation. In the example above,
the Common Lisp definition of APP has two formal parameters, X
and Y. The corresponding DEFN event defines *CL-APP to have three
formal parameters: .RCL-FLG, X, and Y.(.RCL-FLG was called
*SPECIAL-NAME* in [1]) In fact, .RCL-FLG will be the first formal
parameter in any such *CL- function definition. The idea is that
for any values x0 and y0, (*CL-APP T x0 y0) equals the value
returned by the evaluation of (APP X Y) in a Lisp environment in
which X and Y are bound respectively to x0 and y0.
In the example above, T is the only value of .RCL-FLG that is
of interest. However we can illustrate other values of .RCL-FLG
in the following example. Notice that the NQTHM function
*CL-TEST has not only the extra formal parameter .RCL-FLG and the
formal X from the definition of TEST, but also has the extra
formal parameter *UVW*. In general, all special variables whose
values that are relevant to the execution of an RCL function show
up as extra formals to the corresponding NQTHM function. Also,
all extra formals besides .RCL-FLG occur after the original
formal parameters in the list of formals, and are ordered
alphabetically. Here then is the example; explanation follows.
>(defun-rcl test (x)
(if (consp x)
(and (equal (car x) 3)
(progn (setq *uvw* (cdr x))
t))
(throw 'badtest x)))
Used the following non-boot-strap lemmas and functions in the simplification
process: *CL-AND.
(DEFN *CL-TEST
(.RCL-FLG X *UVW*)
(CASE .RCL-FLG
(*1*TRUE (IF (LISTP X)
(IF (EQUAL (CAR X) 3) 'T NIL)
X))
(*1*FALSE (IF (LISTP X) F '(THROW BADTEST)))
(*UVW* (IF (LISTP X)
(IF (EQUAL (CAR X) 3) (CDR X) *UVW*)
*UVW*))
(OTHERWISE F)))
[ 0.3 0.0 0.0 ]
*CL-TEST
T
>
For readers not too familiar with the CASE syntax modification
for Boyer-Moore logic, here is the body of the above DEFN written
in traditional user syntax.
(IF (EQUAL .RCL-FLG T)
(IF (LISTP X)
(IF (EQUAL (CAR X) 3) 'T NIL)
X)
(IF (EQUAL .RCL-FLG F)
(IF (LISTP X) F '(THROW BADTEST))
(IF (EQUAL .RCL-FLG '*UVW*)
(IF (LISTP X)
(IF (EQUAL (CAR X) 3) (CDR X) *UVW*)
*UVW*)
F)))
Let's consider what this DEFN event says about *CL-TEST for
each value of the input parameter .RCL-FLG. The case that
.RCL-FLG is T is analogous to the previous example. It says that
the value of the Lisp form (TEST X) for any particular X is
(IF (LISTP X) (IF (EQUAL (CAR X) 3) 'T NIL) X). This is just as
one would expect from looking at the definition of TEST, though
perhaps the case where (LISTP X) is false is worth a comment. In
this case the Lisp evaluation ends with evaluation of the form
(THROW 'BADTEST X), and we simply adopt the convention that the
value of a THROW is simply the value that was thrown (in this
case, the value of X). (This and other seemingly vague verbiage
can be made precise by defining an interpreter for RCL within the
Boyer-Moore logic. In fact we've done just that, though that
work is not yet polished.)
This observation leads naturally to the next case of .RCL-FLG,
namely where it equals F. In that case the value of *CL-TEST is
the value of the signal present after executing the Lisp form
(TEST X). We are thus led to the notion of a signal, which is an
NQTHM term that represents the ``error condition'' part of the
Lisp state. Normally this term is F, which denotes a ``normal''
state -- but when an exception is raised by THROW, CATCH, or even
GO (in a TAGBODY, cf. Section 5), the signal is no longer F. In
this case, the signal is F unless X is not a CONS pair (i.e. a
LISTP), in which case the signal '(THROW BADTEST) arises from the
THROW.
The next case for .RCL-FLG in the above example is where
.RCL-FLG is the special variable '*UVW*. Incidentally, although
it's not shown here, there needs to be a preceding event
(PROCLAIM-RCL '(SPECIAL *UVW*)) in order for this DEFUN-RCL form
not to cause an error (see Subsection 6.1). At any rate, in this
case of .RCL-FLG, the value of (TEST X) is intended to be the
value of *UVW*. Inspection of that case in the DEFN event will
show that the expected result is obtained, namely, *UVW* is
unchanged except in the case that (LISTP X) and
(EQUAL (CAR X) 3) hold, in which case *UVW* is set to (CDR X).
Notice that *UVW* is an extra formal parameter of *CL-TEST, i.e.
is a formal parameter of *CL-TEST which was not a formal
parameter of TEST.
Finally, in all remaining cases the value F is returned.
Notice that this means that we can specify that a given special
variable v is not changed by any terminating call
of a function FOO, by saying the following (where x1 ... xn are
the formals of *CL-FOO other than .RCL-FLG):
(*) (OR (EQUAL (*CL-FOO 'v x1 ... xn)
v)
(EQUAL (*CL-FOO 'v x1 ... xn)
F))
Let's see why (*) characterizes the property that the value of v
is never changed by an execution of a call of FOO. If v is not a
variable that is among the ``variables set'' of FOO, i.e. if 'v
is not one of the cases of .RCL-FLG, then *CL-FOO returns F (by
definition of *CL-FOO), and we're done. So suppose that v is one
of the ``variables set'' of FOO, i.e. 'v is one of the cases of
.RCL-FLG. For any terminating call of FOO, our spec is that
(*CL-FOO 'v ...) returns the value of v after that call. Since
this value can never be F (since (FALSE) is not a Common Lisp
value), (*) above is equivalent to the statement that the value
of v after running FOO is unchanged.
We have described briefly how a DEFUN-RCL form produces a DEFN
event. However, an additional effect recorded by the system is
to record five properties of the function being defined: its
VARIABLES-READ, VARIABLES-SET, RCL-STATE-VARS-READ,
RCL-STATE-VARS-SET, and ERROR-SIGNALS.(In the implementation,
these are actually properties stored on the property list of
*CL-.) These properties indicate the interaction of the
given function with the Lisp state. So in the TEST example
above, we have the following entries on the property list of
*CL-TEST:
VARIABLES-READ (*UVW*)
VARIABLES-SET (*UVW*)
RCL-STATE-VARS-READ NIL
RCL-STATE-VARS-SET NIL
ERROR-SIGNALS ((THROW BADTEST))
This information is used when another function is defined using
TEST. Consider the following example.
(defun-rcl newtest (x)
(let ((*uvw* *uvw*))
(setq *temp* nil)
(test (cons x x))))
This yields the following DEFN event. Notice that *UVW* is among
the special variables read (in fact the VARIABLES-READ property
of *CL-NEWTEST is simply the one-element list (*UVW*)), because
of the call to TEST. Also notice that *UVW* is not among the
VARIABLES-SET because of the protection of *UVW* afforded by the
LET in the definition of NEWTEST. Here the only special variable
set is *TEMP*.
(DEFN *CL-NEWTEST
(.RCL-FLG X *UVW*)
(CASE .RCL-FLG
(*1*TRUE (*CL-TEST T (CONS X X) *UVW*))
(*1*FALSE (*CL-TEST F (CONS X X) *UVW*))
(*TEMP* NIL)
(OTHERWISE F)))
Next let us observe that we have taken care in our treatment of
the Lisp function CATCH. So for example, the system is able to
deduce that the CATCH in the following example catches all
possible signals, so that the resulting signal is F:
>(defun-rcl catch-newtest (x)
(catch 'badtest (newtest x)))
Used no non-boot-strap lemmas or functions in the simplification process.
(DEFN *CL-CATCH-NEWTEST
(.RCL-FLG X *UVW*)
(CASE .RCL-FLG
(*1*TRUE (*CL-NEWTEST T X *UVW*))
(*TEMP* (*CL-NEWTEST '*TEMP* X *UVW*))
(OTHERWISE F)))
[ 0.2 0.0 0.0 ]
*CL-CATCH-NEWTEST
T
Later (Subsection 9.1) we will see how to coax the simplifier
into producing a syntactically simpler value for the case *TEMP*
above.
We conclude this section with a brief discussion of state
variables. At this time there is only one state variable,
.PLISTS. which represents the property lists in the Lisp state
as an association list, associating symbols with property-value
association lists. For example, if a Lisp state has only two
symbols with properties, X and Y, and if the property list of X
is (FOO 3 BAR 4) and of Y is (BLOB 5), then .PLISTS is the list
((X (FOO 3) (BAR 4)) (Y (BLOB 5))). The following example, which
follows a suggestion of Bob Boyer, illustrates the system's
handling of property lists. In each case we'll give the input in
lower-case and the resulting NQTHM DEFN event in upper-case.
Here *PUTPROP and *GETPROP are defined in the RCL "GROUND-ZERO"
(boot-strap) theory. For completeness, their definitions appear
at the end of this section; they correspond quite closely to
Lisp's traditional PUTPROP and GET functions.
(defun-rcl putprops (symbols mark prop)
;; Puts the value MARK on the PROP property of each symbol in the list SYMBOLS
(if (consp symbols)
(progn (putprop (car symbols) mark prop)
(putprops (cdr symbols) mark prop))
nil))
;; Notice in the recursive call below that the actual parameter in .PLISTS's position
;; is the result of having done a PUTPROP of PROP on the MARK property of
;; the first element of SYMBOLS.
(DEFN *CL-PUTPROPS
(.RCL-FLG SYMBOLS MARK PROP .PLISTS)
(CASE .RCL-FLG
(*1*TRUE NIL)
(.PLISTS (IF (LISTP SYMBOLS)
(*CL-PUTPROPS '.PLISTS
(CDR SYMBOLS)
MARK PROP
(*PUTPROP .PLISTS
(CAR SYMBOLS)
MARK PROP))
.PLISTS))
(OTHERWISE F)))
(defun-rcl checkmarks (symbols prop)
;; Returns the list of symbols in the list SYMBOLS that have a non-nil PROP property
(if (consp symbols)
(if (get (car symbols) prop)
(cons (car symbols)
(checkmarks (cdr symbols) prop))
(checkmarks (cdr symbols) prop))
nil))
(DEFN *CL-CHECKMARKS
(.RCL-FLG SYMBOLS PROP .PLISTS)
(IF (EQUAL .RCL-FLG T)
(IF (LISTP SYMBOLS)
(IF (EQUAL (*GETPROP .PLISTS
(CAR SYMBOLS)
PROP NIL)
NIL)
(*CL-CHECKMARKS T
(CDR SYMBOLS)
PROP .PLISTS)
(CONS (CAR SYMBOLS)
(*CL-CHECKMARKS T
(CDR SYMBOLS)
PROP .PLISTS)))
NIL)
F))
(defun-rcl int (x y)
;; Returns the intersection of the lists X and Y of symbols by first
;; initializing the INT property of each symbol in the list X with NIL, then
;; putting T on the INT property of each symbol in the list Y, and finally
;; returning those symbols in the list X that have a non-NIL INT property.
(putprops x nil 'int)
(putprops y 't 'int)
(checkmarks x 'int))
(DEFN *CL-INT
(.RCL-FLG X Y .PLISTS)
(CASE .RCL-FLG
(*1*TRUE (*CL-CHECKMARKS T X 'INT
(*CL-PUTPROPS '.PLISTS
Y 'T
'INT
(*CL-PUTPROPS '.PLISTS
X NIL 'INT
.PLISTS))))
(.PLISTS (*CL-PUTPROPS '.PLISTS
Y 'T
'INT
(*CL-PUTPROPS '.PLISTS
X NIL 'INT
.PLISTS)))
(OTHERWISE F)))
In fact, after giving a standard recursive definition of
INTERSECT in NQTHM and proving three lemmas, the following lemma
may be proved:
(prove-lemma *cl-int-is-intersect (rewrite)
(equal (*cl-int t x y plists)
(intersect x y)))
For reference, here are the two built-in function definitions
promised above, together with a definition of PUT-ASSOC needed
for the definition of *PUTPROP.
(*getprop plists symbol prop default) =
(let ((pair (assoc prop (cdr (assoc symbol plists)))))
(if pair
(cdr pair)
default))
(put-assoc key val alist) =
;; Adds (key . val) at the end if key is not already a key of alist
(if (listp alist)
(if (equal key (caar alist))
(cons (cons key val) (cdr alist))
(cons (car alist)
(put-assoc key val (cdr alist))))
(list (cons key val)))
(*putprop plists symbol value prop) =
(put-assoc symbol
(put-assoc prop value (cdr (assoc symbol plists)))
plists)
3. DEFMACRO-RCL
Syntax: (defmacro-rcl {decl}* {form}*)
The primary syntactic difference between such a form and a
DEFUN-RCL form is in the allowable ``shape'' of the formal
parameters. That is, the syntax for
allows any CONS structure built from legal symbols (``legal'' in
the sense described at the end of Section 1), including simply a
single atom. Here are some examples of legal DEFMACRO-RCL forms
and the DEFN forms they produce.
(defmacro-rcl lazy-car (x)
(if (and (consp x)
(equal (car x) 'cons))
(car (cdr x))
`(car ,x)))
(defmacro-rcl and x
;; from the startup file
(and-fn x))
(defmacro-rcl prog (bindings . body)
;; from the startup file
`(block nil
(let ,bindings
(tagbody ,@body))))
The DEFN forms produced by DEFMACRO-RCL tend to be quite ugly,
but fortunately it should rarely be necessary for a user to look
at them. The important thing about these DEFN forms (if indeed
anything is particularly important about them, fro the user's
point of view!) is that they always take two formal parameters:
.RCL-FLG (of course) and a parameter that is intended to
represent an entire call of the macro (including the macro
itself, which is the CAR of such a form). Here, for example, is
the DEFN event produced for the LAZY-CAR example above.
(DEFN *CL-LAZY-CAR
(.RCL-FLG LAZY-CAR-WHOLE)
(CASE .RCL-FLG
(*1*TRUE (IF (LISTP (CDR LAZY-CAR-WHOLE))
(IF (EQUAL (CDDR LAZY-CAR-WHOLE) NIL)
(IF (LISTP (CADR LAZY-CAR-WHOLE))
(IF (EQUAL (CAADR LAZY-CAR-WHOLE) 'CONS)
(*CL-CAR<> (CDADR LAZY-CAR-WHOLE))
(LIST 'CAR (CADR LAZY-CAR-WHOLE)))
(LIST 'CAR (CADR LAZY-CAR-WHOLE)))
'(MACROEXPAND-ERROR (TOO MANY ARGUMENTS)))
'(MACROEXPAND-ERROR (NOT ENOUGH ARGUMENTS))))
(*1*FALSE (IF (LISTP (CDR LAZY-CAR-WHOLE))
(IF (EQUAL (CDDR LAZY-CAR-WHOLE) NIL)
F
'(ERROR))
'(ERROR)))
(OTHERWISE F)))
The way macros work in RCL is intended to be essentially the
same as how they are specified to work in Common Lisp. That is,
once a DEFMACRO-RCL, say of a function FOO, has been accepted,
future DEFMACRO-RCL and DEFUN-RCL definitions will macroexpand
calls of FOO: the body of any future definition is traversed
(outside-in) as it is analyzed, and whenever a call of FOO is
encountered, FOO is run on its argument list (which is bound to
the formals of FOO as indicated by the structured
defmacro-lambda-list).[More precisely, *CL-FOO is run on T
together with the list of arguments (QUOTE x) as x ranges over
the arguments of FOO.] Of course, in the implementation this
means that the executable counterpart of *CL-FOO is run with its
.RCL-FLG parameter being T (T representing value, cf. Section 2.)
At this point the alert reader may have a couple of concerns.
One concern is: what if FOO depends on some values of special
variables or state variables? What values do we use for those
when we are executing FOO? At this time we don't carry around a
notion of the global Lisp state, so we simply disallow
DEFMACRO-RCLs that read any special variables or state variables.
We also disallow DEFMACRO-RCLs that SET any special variables or
state variables, since there's no mechanism for reflecting that
setting. Finally, any time that an RCL macro (say, FOO) is to be
executed, the system first calls the executable counterpart of
*CL-FOO with .RCL-FLG set to FALSE, to help to ensure that a real
compilation of that Lisp definition would not cause an
error.(More genuine certainty will be obtained when we implement
total correctness checking. For now, we only wish to claim that
when a DEFMACRO doesn't cause an error or fail to terminate, then
its meaning is reflected in the corresponding DEFMACRO-RCL.)
Finally, we should clarify a potential point of confusion.
Recall the correspondence between Lisp functions defined by
DEFUN-RCL and NQTHM DEFN functions discussed in the preceding
section. For DEFMACRO-RCL functions, there is a similar
correspondence -- similar, at least, if one thinks of a macro in
terms of the function that it defines, a function which takes
code and returns new code. Here are some examples that
illustrate *CL-LAZY-CAR, where LAZY-CAR was defined above using
DEFMACRO-RCL:
>(r-loop)
Abbreviated Output Mode: On
Type ? for help.
*(*cl-lazy-car t '(lazy-car x))
'(CAR X)
*(*cl-lazy-car t '(lazy-car (cons x y)))
'X
*(*cl-lazy-car f '(lazy-car (cons x y)))
F
*(*cl-lazy-car t '(lazy-car x y))
'(MACROEXPAND-ERROR (TOO MANY ARGUMENTS))
*(*cl-lazy-car f '(lazy-car x y))
'(ERROR)
To summarize this point: the *CL- function defined by DEFN to
``correspond'' to a DEFMACRO-RCL is intended to represent what is
called in Common Lisp the expansion function for the macro, i.e.
the function returned by the Lisp function MACRO-FUNCTION, and
not the result of evaluating the resulting form. One more
example should illustrate this point.
(*cl-lazy-car t '(lazy-car (cons (cdr '(1 2)) 7)))
= '(CDR '(1 2))
Notice that the right-hand side above is not '(2), even though
(using simplification with rewrite rules) it is the case that
(defun-rcl lazy-car-test ()
(lazy-car (cons (cdr '(1 2)) 7)))
produces
(DEFN *CL-LAZY-CAR-TEST
(.RCL-FLG)
(IF (EQUAL .RCL-FLG T) '(2) F))
Perhaps we should mention one subtlety. There are perhaps two
notions of ``recursive macro'' that one might imagine, but only
one of them (the reasonable one) is allowed here. Here is an
example of an acceptable ``recursive macro'' (one which takes
repeated CDRs at definition time, when possible):
(defmacro-rcl lazy-cdr* (x)
(if (and (consp x)
(equal (car x) 'cons))
(list 'lazy-cdr* (car (cddr x)))
(list 'cdr x)))
So for example, we have the following sample use of LAZY-CDR*.
Notice that the form (SETQ X 8) is not relevant but would have
been very relevant if LAZY-CDR* were an ordinary function that
evaluates all its arguments.
(defun-rcl foo (x)
(cons 3
(lazy-cdr* (cons (setq x 7)
(cons (setq x 8) x)))))
(DEFN *CL-FOO
(.RCL-FLG X)
(IF (EQUAL .RCL-FLG T)
(CONS 3 (*CL-CDR<> X))
F))
However, it is an error to actually call a macro before the
process of defining that macro (i.e. the execution of the
DEFMACRO-RCL or DO-RCL in which it is defined) is entirely
complete. That kind of recursion seems a sufficiently strange
thing to do that it seems difficult to think of a reasonable
example of how to violate this requirement with recursion. An
unreasonable example might be (defmacro-rcl boo (x) (if (consp x)
(boo (cdr x)) 3)).
4. DO-RCL
First we need a definition. Let's say that one DEFN form
depends on another if the body of the first contains a call of
the function defined by the other. If one has a sequence of DEFN
forms then this notion induces a binary relation on those forms,
which we will call the dependency relation. There is always a
smallest transitive-reflexive relation(i.e. preorder) R*
generated by a binary relation R on a set, namely x R* y iff
there is a sequence x = x R x R ... R x = y. Consider the
0 1 n
equivalence relation E on the field of R which is defined as
follows: x E y iff (x R* y and y R* x). In the case where R is
the dependency relation on a set of definitions, we will call the
equivalence classes of E the dependency classes.
We have seen how to use DEFUN-RCL and DEFMACRO-RCL. But what
do we do when our definitions may be mutually recursive? In this
case we may use DO-RCL. If the definitions turn
out not to be mutually recursive after all, then DO-RCL could
have been avoided in favor of submitting the definitions one
after the other (in the proper order). However, if there is
mutual recursion then one extra function is created for each
dependency class (see paragraph above) of size greater than 1.
That function has as its formal parameters the union of the
formal parameters of the definitions in that dependency class
together with one extra formal parameter, .MUTUAL-FLG (possibly
suffixed by a number to make it a new parameter). The auxiliary
functions will have names of the form =n where is
the first argument of DO-RCL and n is a number (chosen by the
system so that the resulting name will be new).(More on mutual
recursion in NQTHM may be found in [9]. Though there are some
minor differences in detail between the implementation described
there and the one described here, the principles are the same and
the pace is more leisurely there.)
Here is an example. Notice that MUT-1 and MUT-2 are mutually
recursive, as are MUT-3 and MUT-4.
(do-rcl mutts
(defun-rcl mut-1 (x)
(if (consp x)
(cons (car x) (mut-2 (cdr x)))
nil))
(defun-rcl mut-2 (x)
(if (consp x)
(cons (car x) (mut-1 (cdr x)))
nil))
(defun-rcl mut-3 (x)
(if (consp x)
(cons (car x) (mut-4 (cdr x)))
nil))
(defun-rcl mut-4 (x)
(if (consp x)
(cons (car x) (mut-3 (cdr x)))
nil))
)
The system is able to deduce the dependency graph, and it creates
the following DEFN events. Notice that *CL-MUT-1 and *CL-MUT-2
are in the same dependency class, as are *CL-MUT-3 and *CL-MUT-4.
MUTTS=0 is created for the first pair of functions, where its
parameter .MUTUAL-FLG determines whether the value of MUTTS=0
represents the value of *CL-MUT-2 or *CL-MUT-1, according to
whether .MUTUAL-FLG is '*CL-MUT-2 or not. (Similarly for
MUTTS=1, *CL-MUT-4, and *CL-MUT-3.)
(DEFN MUTTS=0
(.MUTUAL-FLG .RCL-FLG X)
(COND ((EQUAL .MUTUAL-FLG '*CL-MUT-2)
(IF (EQUAL .RCL-FLG T)
(IF (LISTP X)
(CONS (CAR X)
(MUTTS=0 '*CL-MUT-1 T (CDR X)))
NIL)
F))
((EQUAL .RCL-FLG T)
(IF (LISTP X)
(CONS (CAR X)
(MUTTS=0 '*CL-MUT-2 T (CDR X)))
NIL))
(T F)))
(DEFN *CL-MUT-2
(.RCL-FLG X)
(MUTTS=0 '*CL-MUT-2 .RCL-FLG X))
(DEFN *CL-MUT-1
(.RCL-FLG X)
(MUTTS=0 '*CL-MUT-1 .RCL-FLG X))
(DEFN MUTTS=1
(.MUTUAL-FLG .RCL-FLG X)
(COND ((EQUAL .MUTUAL-FLG '*CL-MUT-4)
(IF (EQUAL .RCL-FLG T)
(IF (LISTP X)
(CONS (CAR X)
(MUTTS=1 '*CL-MUT-3 T (CDR X)))
NIL)
F))
((EQUAL .RCL-FLG T)
(IF (LISTP X)
(CONS (CAR X)
(MUTTS=1 '*CL-MUT-4 T (CDR X)))
NIL))
(T F)))
(DEFN *CL-MUT-4
(.RCL-FLG X)
(MUTTS=1 '*CL-MUT-4 .RCL-FLG X))
(DEFN *CL-MUT-3
(.RCL-FLG X)
(MUTTS=1 '*CL-MUT-3 .RCL-FLG X))
If there are DECLARE forms then those forms are all gathered
together into a single set of DECLARE forms; see Section 7 for
details.
Finally, we note that for convenience we have arranged things
so that inside DO-RCL, one may use DEFUN or DEFMACRO in place of
DEFUN-RCL or DEFMACRO-RCL without any change in functionality
whatsoever.
5. TAGBODY
In general, additional *CL- functions may be created by
DEFUN-RCL or DEFMACRO-RCL to reflect iteration. We will call
these tagbody functions because the iteration form we support is
TAGBODY. (Many readers will prefer to use the PROG macro, whose
definition may be found in Section 3.) The idea is that each
call of TAGBODY is replaced by a new Lisp function of one
argument, that argument representing a tag giving the entry point
in that TAGBODY code. If the first form in the tagbody is not a
tag, i.e. is not an integer or a symbol, then the tag
TAGBODY-START (suffixed by a number to make it a new tag, if
necessary) is inserted as the first argument of the TAGBODY form;
this tag is then the one which the ``tagbody function'' is
initially called.
More precisely, the system implicitly defines a Lisp function
using DEFUN-RCL which we'll call a tagbody function. Its name is
created by suffixing -TAGBODY-0 to the name of the function in
which a tagbody occurs (at least for the first such tagbody that
the system encounters; later ones are then the result of
suffixing -TAGBODY-1, -TAGBODY-2, etc. to the main function
name). It has one formal parameter, TAG.(Actually, as usual with
such things, TAG is suffixed by a numeral if necessary in order
to avoid name clashes, this time with the lexical and special
variables in the given context.) This function is called
initially with its argument equaling the topmost tag in the
tagbody. Then the translation process creates an NQTHM DEFN
named by prefixing *CL- to the name of this tagbody function the
NQTHM function. However, let us note that this DEFN may be
optimized by the system in various ways; for example the formals
.RCL-FLG and TAG may be dropped. (More on such optimizations may
be found in Section 9.) The important thing is that the final
definition, which corresponds to the original DEFUN-RCL function
(e.g., *CL-LASTCDR corresponds to LASTCDR in the example below)
correctly models the behavior of that NQTHM function.
Let us look at a simple example. The RETURN-FROM form
reflects our adherence to the specification of DEFUN in Common
Lisp that there is an implicit BLOCK around the function body,
where the tag of that implicit BLOCK form equals the name of the
function being defined.
>(defun-rcl lastcdr (x)
(tagbody
loop
(if (consp x)
(setq x (cdr x))
(return-from lastcdr x))
(go loop)))
Used no non-boot-strap lemmas or functions in the simplification process.
(DEFN *CL-LASTCDR-TAGBODY-0
(X)
(IF (LISTP X)
(*CL-LASTCDR-TAGBODY-0 (CDR X))
X))
Linear arithmetic and the lemma CDR-LESSP establish that the measure
(COUNT X) decreases according to the well-founded relation LESSP in each
recursive call. Hence, *CL-LASTCDR-TAGBODY-0 is accepted under the principle
of definition.
[ 0.1 0.1 0.1 ]
*CL-LASTCDR-TAGBODY-0
(DEFN *CL-LASTCDR
(.RCL-FLG X)
(IF (EQUAL .RCL-FLG T)
(*CL-LASTCDR-TAGBODY-0 X)
F))
[ 0.1 0.0 0.0 ]
*CL-LASTCDR
T
>
Just as in the case of the main function (i.e. the NQTHM
function that corresponds to the one defined by DEFUN-RCL), the
NQTHM function that corresponds to a tagbody function may have
extra formal parameters for the special (and state) variables
that it needs (reads). Here is another example. Recall from
Sectio 3 that a PROG macroexpands into a TAGBODY; more on this
below.
>(defun-rcl rev1 (x)
(prog (acc)
loop
(when (not (consp x))
(return acc))
(setq acc (cons (car x) acc))
(setq x (cdr x))
(go loop)))
Used the following non-boot-strap lemmas and functions in the simplification
process: *CL-NOT-REWRITE, *CL-NOT<>-REWRITE, *CL-RETURN, *CL-WHEN, and
*CL-PROG.
(DEFN *CL-REV1-TAGBODY-0
(ACC X)
(IF (LISTP X)
(*CL-REV1-TAGBODY-0 (CONS (CAR X) ACC)
(CDR X))
ACC))
Linear arithmetic and the lemma CDR-LESSP inform us that the measure
(COUNT X) decreases according to the well-founded relation LESSP in each
recursive call. Hence, *CL-REV1-TAGBODY-0 is accepted under the definitional
principle. From the definition we can conclude that:
(OR (LISTP (*CL-REV1-TAGBODY-0 ACC X))
(EQUAL (*CL-REV1-TAGBODY-0 ACC X)
ACC))
is a theorem.
[ 0.1 0.1 0.1 ]
*CL-REV1-TAGBODY-0
(DEFN *CL-REV1
(.RCL-FLG X)
(IF (EQUAL .RCL-FLG T)
(*CL-REV1-TAGBODY-0 NIL X)
F))
Note that:
(OR (FALSEP (*CL-REV1 .RCL-FLG X))
(LITATOM (*CL-REV1 .RCL-FLG X))
(LISTP (*CL-REV1 .RCL-FLG X)))
is a theorem.
[ 0.1 0.0 0.0 ]
*CL-REV1
T
As mentioned above, notice that PROG is provided in the RCL
system, just as it is in Common Lisp. For example:
>(r-loop)
Abbreviated Output Mode: On
Type ? for help.
*(*cl-prog t '(prog (acc)
loop
(when (not (consp x))
(return acc))
(setq acc (cons (car x) acc))
(setq x (cdr x))
(go loop)))
'(BLOCK NIL
(LET (ACC)
(TAGBODY LOOP
(WHEN (NOT (CONSP X)) (RETURN ACC))
(SETQ ACC (CONS (CAR X) ACC))
(SETQ X (CDR X))
(GO LOOP))))
*
The important thing about this example, anyhow, is that ACC is
treated like a special variable from the point of view of the
TAGBODY form, as is easily seen from the macroexpanded form
(BLOCK NIL (LET (ACC) (TAGBODY ...))) above. This fact shows up
in the inclusion of ACC as an extra formal parameter in
*CL-REV1-TAGBODY-0. Interestingly, the body of this function
corresponds not to the value of the TAGBODY form but rather to
the value of ACC. We'll come back to this example in Section 9.
For now, suffice it to say that the original body of
*CL-REV1-TAGBODY-0 (before any simplification) was as follows;
but the main function *CL-REV1 only calls this function with
.RCL-FLG set to 'ACC, so the other branches of the CASE were
discarded by the system. The unsimplified body of
*CL-REV1-TAGBODY-0 is actually as follows.
(CASE .RCL-FLG
(*1*TRUE (IF (LISTP X)
(*CL-REV1-TAGBODY-0 T 'LOOP (CONS (CAR X) ACC) (CDR X))
ACC))
(*1*FALSE
(IF (LISTP X)
(*CL-REV1-TAGBODY-0 F 'LOOP (CONS (CAR X) ACC) (CDR X))
'(RETURN-FROM ())))
(ACC (IF (LISTP X)
(*CL-REV1-TAGBODY-0 'ACC 'LOOP (CONS (CAR X) ACC) (CDR X))
ACC))
(X (IF (LISTP X)
(*CL-REV1-TAGBODY-0 'X 'LOOP (CONS (CAR X) ACC) (CDR X)) X))
(OTHERWISE F))
6. PROCLAIM-RCL
Syntax: (proclaim-rcl (quote (kind . rest)) {event-name})
Here kind is one of SPECIAL, FORCE-AUXILIARY-FUNCTIONS,
INHIBIT-AUXILIARY-LEMMAS, or POSTPROCESS-DEFNS. (In general, the
list of such legal kinds is kept in the Lisp variable
*LEGAL-RCL-PROCLAMATION-TYPES*.) Notice that PROCLAIM-RCL is a
new kind of event (unlike DEFUN-RCL and DEFMACRO-RCL, which
create DEFN events but aren't themselves events). Hence it is
subject to the usual undoing mechanism, e.g. using the NQTHM
command UBT.(However, we do not attempt to track dependencies on
PROCLAIM-RCL events. In particular, if a DEFUN-RCL form uses a
special variable and the proclaiming of the variable is undone by
UNDO-NAME, then the database will be in a state that is not
re-creatable without using UNDO-NAME. This situation is
analogous to the situation with DISABLE and ENABLE events in
NQTHM.)
Also notice that some of the PROCLAIM-RCL proclamations also
make sense in a local setting; see Section 7.
6.1 SPECIAL proclamations
The event (PROCLAIM-RCL '(SPECIAL `)) declares the
variable `` to be special in the usual Lisp sense, i.e. to
have the property that it may be referenced in functions without
being passed explicitly. The following example should perhaps
suffice.
>(defun-rcl fff (x) (setq *zzz* x) 3)
Error: ERROR SIGNALLED BY RCL FUNCTION....
The variable *ZZZ* is neither lexical nor special in (SETQ *ZZZ* X)
Error signalled by EVAL.
Broken at DO-RCL-FN. Type :H for Help.
>>:q
Top level.
>(proclaim-rcl '(special *zzz*))
[ 0.0 0.0 0.0 ]
DEFVAR-*ZZZ*
>(defun-rcl fff (x) (setq *zzz* x) 3)
Used no non-boot-strap lemmas or functions in the simplification process.
(DEFN *CL-FFF
(.RCL-FLG X)
(CASE .RCL-FLG
(*1*TRUE 3)
(*ZZZ* X)
(OTHERWISE F)))
Recall that the event name for PROCLAIM-RCL is an optional
second argument. For SPECIAL proclamations we have a particular
way of assigning the default: (PROCLAIM-RCL '(SPECIAL ``))
generates a PROCLAIM-RCL event named DEFVAR-``. The same
effect could be obtained with (PROCLAIM-RCL '(SPECIAL ``)
DEFVAR-``), but if a different name is desired, a different
optional argument could be supplied, as in:
>(proclaim-rcl '(special *abc*) does-this-make-my-point?)
[ 0.0 0.0 0.0 ]
DOES-THIS-MAKE-MY-POINT?
>
6.2 FORCE-AUXILIARY-FUNCTIONS proclamations
An auxiliary function is a function defined by an NQTHM DEFN
event that was created in response to DEFUN-RCL, DEFMACRO-RCL, or
DO-RCL, but is not the NQTHM function corresponding to any
function defined explicitly by DEFUN-RCL or DEFMACRO-RCL.
The extra functions created by mutual recursion and by tagbody
forms are examples of auxiliary functions, but in this subsection
we will be concerned with another type of auxiliary function,
namely one that corresponds to the value, signal, or value of a
special or state variable after a call of a Lisp function. Let
us call these sub-functions. By ``Lisp function'' here we mean
any name defined by DEFUN-RCL or DEFMACRO-RCL, including those
DEFUN-RCL forms created behind-the-scenes for tagbody functions
(cf. Section 5).
The event (PROCLAIM-RCL '(FORCE-AUXILIARY-FUNCTIONS T)) causes
auxiliary functions to be created for each *CL- function arising
from a DEFUN-RCL or DEFMACRO-RCL definition (including functions
arising from TAGBODY forms; see Section 5): one for the value of
the function, one for the signal corresponding to the function,
and one for each special variable and state variable(i.e.,
.PLISTS) potentially set by the function. The auxiliary function
names are obtained from the main *CL- function name by suffixing
`<>' for the value, `<>signal' for the signal, and `' for a
special variable or state variable v. Here is an example.
(defun-rcl sweep1 (x)
(if (consp x)
(progn (sweep1 (cdr x))
(sweep1 (car x))
nil)
(setq ans (cons x ans))))
This definition of SWEEP1 generates DEFN events *CL-SWEEP1<> and
*CL-SWEEP1, for the value of a function call and of the
special variable ANS after executing a call (respectively).
(DEFN *CL-SWEEP1<>
(X ANS)
(IF (LISTP X) NIL (CONS X ANS)))
(DEFN *CL-SWEEP1
(X ANS)
(IF (LISTP X)
(*CL-SWEEP1 (CAR X)
(*CL-SWEEP1 (CDR X) ANS))
(CONS X ANS)))
(DEFN *CL-SWEEP1
(.RCL-FLG X ANS)
(CASE .RCL-FLG
(*1*TRUE (*CL-SWEEP1<> X ANS))
(ANS (*CL-SWEEP1 X ANS))
(OTHERWISE F)))
Notice that *CL-SWEEP1<>SIGNAL was not created. In fact, when
the system can determine that the signal is identically F, it
will not create an auxiliary function for the signal, preferring
instead to use F directly as the value of the signal (as part of
the "OTHERWISE" case).
Similarly, (PROCLAIM-RCL '(FORCE-AUXILIARY-FUNCTIONS NIL))
turns off this feature. The default is NIL, i.e. these auxiliary
functions are not created until the command (PROCLAIM-RCL
'(FORCE-AUXILIARY-FUNCTIONS T)) is given. (Of course,
(PROCLAIM-RCL '(FORCE-AUXILIARY-FUNCTIONS NIL)) would then turn
this feature off again.) These events are assigned names by
default: FORCE-AUXILIARY-FUNCTIONS-ON and FORCE-AUXILIARY-
FUNCTIONS-OFF (possibly with numeric suffixes, in order to create
new names for the events). However, as with all PROCLAIM-RCL
events the user is welcome to provide the name of the event as an
optional second argument, e.g. (PROCLAIM-RCL '(FORCE-AUXILIARY-
FUNCTIONS NIL) PROCLAIM-TEST).
It is an error to (FORCE-AUXILIARY-FUNCTIONS T) when auxiliary
functions are already forced or to (FORCE-AUXILIARY-FUNCTIONS
NIL) when they are already non-forced.
6.3 INHIBIT-AUXILIARY-LEMMAS proclamations
The event (PROCLAIM-RCL '(INHIBIT-AUXILIARY-LEMMAS T)) causes
auxiliary lemmas to be created and proved, as described below;
(PROCLAIM-RCL '(INHIBIT-AUXILIARY-LEMMAS NIL)) turns off this
feature. The default is NIL, i.e. auxiliary lemmas are not
inhibited; they will be created until (PROCLAIM-RCL '(INHIBIT-
AUXILIARY-LEMMAS T)) is executed. Notice that if there are no
auxiliary functions created then there will be no auxiliary
lemmas. The naming conventions for the resulting event are the
same as for FORCE-AUXILIARY-FUNCTIONS, except of course that the
defaults have a prefix of INHIBIT-AUXILIARY-LEMMAS rather than of
FORCE-AUXILIARY-FUNCTIONS.
One auxiliary lemma is created for each auxiliary sub-function
that is created by the mechanism of the preceding subsection,
i.e. that corresponds to the value, signal, or value of a special
or state variable after a call of a function defined by DEFUN-RCL
or DEFMACRO-RCL (including tagbody functions). All auxiliary
lemmas are run at the end of whatever other events are created by
DEFUN-RCL, DEFMACRO-RCL, or DO-RCL. Each such lemma is of the
following form, where (say) *cl-foo_suffix is the name of the
sub-function, *cl-foo is the function from which that
sub-function was derived, and flag refers to T, F, or v,
according to whether the sub-function corresponds to the value,
the signal, or the variable v (respectively).
(prove-lemma *cl-foo_suffix-rewrite
(rewrite)
(equal (*cl-foo flag ...args...)
(*cl-foo_suffix ...args...)))
Consider the example of SWEEP1 described in the preceding
subsection. In that example, two auxiliary functions were
created. The following lemmas would subsequently be created as
well, assuming that auxiliary lemmas were not inhibited (which,
once again, is the default).
(PROVE-LEMMA *CL-SWEEP1<>-REWRITE
(REWRITE)
(EQUAL (*CL-SWEEP1 T X ANS)
(*CL-SWEEP1<> X ANS)))
(PROVE-LEMMA *CL-SWEEP1-REWRITE
(REWRITE)
(EQUAL (*CL-SWEEP1 'ANS X ANS)
(*CL-SWEEP1 X ANS)))
To summarize, then, suppose that auxiliary lemmas are not
inhibited. (Again, this is the default.) Then it is the case
that at the end of the sequence of events that would otherwise be
executed, one lemma is created for each sub-function. Each such
lemma instructs the rewriter to replace various function calls
with calls of corresponding sub-functions in future
simplifications and proofs.
6.4 POSTPROCESS-DEFNS proclamations
The event (PROCLAIM-RCL '(POSTPROCESS-DEFNS NIL)) turns off a
feature that we call definition postprocessing. It turns out
that among the several kinds of simplifications that we do, there
is a kind of recursion elimination, done with a function
REPLACE-WITH-CONSTANTS-IN-DEFN.(Who cares, you may ask, what the
function is called? You probably only care if you have set
*INSTRUMENT-FLG* to T; see Section 8.) Now we cannot prove that
this optimization is sound in general(in fact we doubt that it
is, but have yet to produce an example) except under the
condition that the DEFN in question has already been accepted.
However, this optimization can be a useful one (an example will
follow below), so the default is that this optimization is always
attempted. If some simplification does indeed occur, then the
definition is undone (automatically by the system), the
simplified definition is simplified a final time, and finally the
new definition is submitted. Here is a simple example. The
function REV-LINEAR1 is one that is presumably used only for its
side-effect to the special variable ANS (which has presumably
been PROCLAIMed special already by a previous PROCLAIM-RCL
event). The idea is that the system can deduce that the value of
this function is always NIL.
>(DEFUN-RCL REV-LINEAR1
(X)
(IF (CONSP X)
(PROGN (SETQ ANS (CONS (CAR X) ANS))
(REV-LINEAR1 (CDR X)))
NIL))
Used no non-boot-strap lemmas or functions in the simplification process.
(DEFN *CL-REV-LINEAR1
(.RCL-FLG X ANS)
(CASE .RCL-FLG
(*1*TRUE (IF (LISTP X)
(*CL-REV-LINEAR1 T
(CDR X)
(CONS (CAR X) ANS))
NIL))
(ANS (IF (LISTP X)
(*CL-REV-LINEAR1 'ANS
(CDR X)
(CONS (CAR X) ANS))
ANS))
(OTHERWISE F)))
Linear arithmetic and the lemma CDR-LESSP can be used to establish that
the measure (COUNT X) decreases according to the well-founded relation LESSP
in each recursive call. Hence, *CL-REV-LINEAR1 is accepted under the
definitional principle. Observe that:
(OR (OR (FALSEP (*CL-REV-LINEAR1 .RCL-FLG X ANS))
(LITATOM (*CL-REV-LINEAR1 .RCL-FLG X ANS))
(LISTP (*CL-REV-LINEAR1 .RCL-FLG X ANS)))
(EQUAL (*CL-REV-LINEAR1 .RCL-FLG X ANS)
ANS))
is a theorem.
[ 0.2 0.2 0.1 ]
[[[[[ Replacing definition of *CL-REV-LINEAR1 with a simpler one: ]]]]]
(DEFN *CL-REV-LINEAR1
(.RCL-FLG X ANS)
(CASE .RCL-FLG
(*1*TRUE NIL)
(ANS (IF (LISTP X)
(*CL-REV-LINEAR1 'ANS
(CDR X)
(CONS (CAR X) ANS))
ANS))
(OTHERWISE F)))
Linear arithmetic and the lemma CDR-LESSP can be used to prove that the
measure (COUNT X) decreases according to the well-founded relation LESSP in
each recursive call. Hence, *CL-REV-LINEAR1 is accepted under the principle
of definition. Note that:
(OR (OR (FALSEP (*CL-REV-LINEAR1 .RCL-FLG X ANS))
(LITATOM (*CL-REV-LINEAR1 .RCL-FLG X ANS))
(LISTP (*CL-REV-LINEAR1 .RCL-FLG X ANS)))
(EQUAL (*CL-REV-LINEAR1 .RCL-FLG X ANS)
ANS))
is a theorem.
[ 0.1 0.1 0.1 ]
*CL-REV-LINEAR1
T
As we already mentioned above, the default is that this
feature is on, and (PROCLAIM-RCL '(POSTPROCESS-DEFNS NIL)) turns
it off. This feature can then be turned back on again with
(PROCLAIM-RCL '(POSTPROCESS-DEFNS T)). There are actually two
other legal settings that we expect to be used only rarely.
(PROCLAIM-RCL '(POSTPROCESS-DEFNS COMPLETE)) instructs the system
to attempt to simplify every definition(using essentially the
simplifier of PC-NQTHM, [6]), whether or not the simplification
done by REPLACE-WITH-CONSTANTS-IN-DEFN does anything. We would
expect that this kind of simplification is rarely going to do any
good by itself (in fact, see the example at the end of this
subsection), but we allow this COMPLETE setting anyhow in case
someone finds a use for it. The final legal setting is
CONSTANTS, i.e. the event form (PROCLAIM-RCL '(POSTPROCESS-DEFNS
CONSTANTS)) is allowed. This is just like the setting of T,
except that no further simplification is attempted after the
recursion elimination. The only use we expect for this setting
is when a user dislikes the forms produced by that further
simplification but still wants the recursion elimination provided
by REPLACE-WITH-CONSTANTS-IN-DEFN.
As with all PROCLAIM events, an optional second argument names
the event. The default event name is POSTPROCESS-, where
is NIL, T, COMPLETE, or CONSTANTS according to which of
these is supplied in the PROCLAIM-RCL event form. If such a name
is not new, then a numeral is suffixed.
Finally, here is an example showing how simplification can do
more harm than good, at least aesthetically.
>(defun-rcl bad (x) (if (equal x 3) (throw 'foo 7) nil))
Used no non-boot-strap lemmas or functions in the simplification process.
(DEFN *CL-BAD
(.RCL-FLG X)
(CASE .RCL-FLG
(*1*TRUE (IF (EQUAL X 3) 7 NIL))
(*1*FALSE (IF (EQUAL X 3) '(THROW FOO) F))
(OTHERWISE F)))
Observe that:
(OR (FALSEP (*CL-BAD .RCL-FLG X))
(NUMBERP (*CL-BAD .RCL-FLG X))
(LITATOM (*CL-BAD .RCL-FLG X))
(LISTP (*CL-BAD .RCL-FLG X)))
is a theorem.
[ 0.2 0.0 0.0 ]
[[[[[ Replacing definition of *CL-BAD with a simpler one: ]]]]]
(DEFN *CL-BAD
(.RCL-FLG X)
(COND ((EQUAL .RCL-FLG T)
(IF (EQUAL X 3) 7 NIL))
(.RCL-FLG F)
((EQUAL X 3) '(THROW FOO))
(T F)))
Observe that:
(OR (FALSEP (*CL-BAD .RCL-FLG X))
(NUMBERP (*CL-BAD .RCL-FLG X))
(LITATOM (*CL-BAD .RCL-FLG X))
(LISTP (*CL-BAD .RCL-FLG X)))
is a theorem.
[ 0.1 0.0 0.1 ]
*CL-BAD
T
Another example of definition postprocessing may be found in
Subsection 7.4.
7. DECLARE
Recall from Section 2 that an optional DECLARE form is allowed
immediately after the formal parameters of a definition and
before its body. In this section we describe the shapes that the
DECLARE forms may take as well as the effects that they have.
The general syntax is:
(declare (kind (event ...) (event ...))
1 1,1 1,k
1
...
(kind (event ...) (event ...)))
n n,1 n,k
n
Each kind must be distinct from the others and must be one of
i
HINTS, FUNCTIONS, EVENTS, or POSTPROCESS(i.e. one of those in the
Lisp variable *DECLARATIONS-LIST*). Events within the scope of
the same kind should be distinct, i.e. if j N j then event
1 2 i,j
1
N event , or else an error is caused. Each event is
i,j i,j
2
intended to be the name of an event that is run in the course of
carrying out the DEFUN-RCL, DEFMACRO-RCL, or DO-RCL in question;
a warning is issued when this is not the case.
Such DECLARE forms are also allowed when the definitions are
inside DO-RCL; in that case, they are merged together and used
together for each definition in that DO-RCL form. The merged
DECLARE form is obtained by appending all declarations of each
kind into a single declaration of that kind. The restrictions
and warnings discussed in the previous paragraph then apply to
this single merged declaration.
Here is an example with some comments. It provides a pretty
thorough summary, but we give more details on each kind of
declaration in the subsections that follow.
>(defun-rcl fff (x)
(declare
;; Create a sub-function *CL-FFF<> for the value from a call of FFF and
;; a sub-function *CL-FFF for the value of ANS after that call
(functions (*cl-fff t ans))
;; Prove the silly lemma SAMPLE just after running the event *CL-FFF
(events (*cl-fff (prove-lemma sample nil (equal x x))))
;; Append the hints-list (((LESSP (LENGTH X)))) to the back of the event *CL-FFF<>
;; and append the hints-list (((LESSP (COUNT ANS)))) to the back of the event *CL-FFF
(hints (*cl-fff<> ((lessp (length x))))
(*cl-fff ((lessp (count x))))))
;; end of declarations
(cond
((consp x)
(setq xxx (1- xxx))
(setq ans (1+ ans))
(fff (cdr x)))
(t x)))
Used the following non-boot-strap lemmas and functions in the simplification
process: *CL-COND.
;; The following is created because of the presence of T in the hint (functions (*cl-fff t ans)),
;; and the hint ((LESSP (LENGTH X))) is a result of the HINTS declaration.
;; This function represents the value returned by a call of FFF.
(DEFN *CL-FFF<>
(X)
(IF (LISTP X) (*CL-FFF<> (CDR X)) X)
((LESSP (LENGTH X))))
Linear arithmetic, the lemmas EQUAL-LENGTH-0 and SUB1-ADD1, and the
definitions of LESSP and LENGTH can be used to establish that the measure
(LENGTH X) decreases according to the well-founded relation LESSP in each
recursive call. Hence, *CL-FFF<> is accepted under the principle of
definition.
[ 0.1 0.5 0.0 ]
*CL-FFF<>
;; The following is created because of the presence of ANS in the hint
;; (functions (*cl-fff t ans)), and the hint ((LESSP (COUNT X)))
;; is a result of the HINTS declaration.
;; This function represents the value of the special variable ANS after a call of FFF.
(DEFN *CL-FFF
(X ANS)
(IF (LISTP X)
(*CL-FFF (CDR X) (IPLUS ANS 1))
ANS)
((LESSP (COUNT X))))
Linear arithmetic and the lemma CDR-LESSP inform us that the measure
(COUNT X) decreases according to the well-founded relation LESSP in each
recursive call. Hence, *CL-FFF is accepted under the principle of
definition. Note that:
(OR (OR (NUMBERP (*CL-FFF X ANS))
(NEGATIVEP (*CL-FFF X ANS)))
(EQUAL (*CL-FFF X ANS) ANS))
is a theorem.
[ 4.3 0.1 0.1 ]
*CL-FFF
(DEFN *CL-FFF
(.RCL-FLG X ANS XXX)
(CASE .RCL-FLG
(*1*TRUE (*CL-FFF<> X))
;; Notice that CL-FFF was not created since XXX was not specified
;; in the FUNCTIONS declaration.
(XXX (IF (LISTP X)
(*CL-FFF 'XXX
(CDR X)
(IPLUS ANS 1)
(IDIFFERENCE XXX 1))
XXX))
(ANS (*CL-FFF X ANS))
(OTHERWISE F)))
Linear arithmetic and the lemma CDR-LESSP can be used to establish that
the measure (COUNT X) decreases according to the well-founded relation LESSP
in each recursive call. Hence, *CL-FFF is accepted under the definitional
principle.
[ 0.2 0.1 0.1 ]
*CL-FFF
;; The following event was created just after *CL-FFF because of the events declaration.
(PROVE-LEMMA SAMPLE NIL (EQUAL X X))
This formula simplifies, obviously, to:
T.
Q.E.D.
[ 0.0 0.1 0.0 ]
SAMPLE
;; The final two lemmas were created because we had the default setting for auxiliary
;; lemmas not being inhibited.
(PROVE-LEMMA *CL-FFF<>-REWRITE
(REWRITE)
(EQUAL (*CL-FFF T X ANS XXX)
(*CL-FFF<> X)))
This formula simplifies, opening up the definitions of EQUAL and *CL-FFF, to:
T.
Q.E.D.
[ 0.0 0.1 0.0 ]
*CL-FFF<>-REWRITE
(PROVE-LEMMA *CL-FFF-REWRITE
(REWRITE)
(EQUAL (*CL-FFF 'ANS X ANS XXX)
(*CL-FFF X ANS)))
This conjecture simplifies, expanding EQUAL and *CL-FFF, to:
T.
Q.E.D.
[ 0.0 0.2 0.0 ]
*CL-FFF-REWRITE
T
>
It is important to note that in the absence of DECLARE forms,
the global state, as set by PROCLAIM-RCL and reported by
RCL-STATUS (see Subsection 8.5), is used. So for example, if
there had been no FUNCTIONS declaration, the same results as
above would be obtained if the defaults were modified by
(PROCLAIM-RCL (FORCE-AUXILIARY-FUNCTIONS T)), except that a
function *CL-FFF would also have been created, together with
a corresponding rewrite rule.
7.1 HINTS declarations
The example above showed a sample HINTS declaration:
(hints (*cl-fff<> ((lessp (length x))))
(*cl-fff ((lessp (count x)))))
As this example suggests, the syntax for HINTS declarations is
(HINTS (event hints hints ...)
1 1,1 1,2
...
(event hints hints ...))
n n,1 n,2
Each hints is appended to the end of the event named event
i,j i
before that event is run. Typically there is only one hint per
event, and one can think of the hint as the optional ``hints''
argument to the event.
7.2 FUNCTIONS declarations
The syntax for this form of declaration is
(FUNCTIONS (f x ... x )
1 1,1 1,n
1
...
(f x ... x )))
k k,1 k,n
k
where each f is a distinct name of an NQTHM function that one
i
expects to be created by the DEFUN-RCL, DEFMACRO-RCL, or DO-RCL
form that is being processed. The distinctness requirement is
enforced, but if the only ``error'' is that function names are
given that turn out not to name functions that become defined,
then the execution proceeds happily and only a warning (not an
error) is issued.
In the presence of such a declaration in a DEFUN-RCL or
DEFMACRO-RCL form, the global situation for FORCE-AUXILIARY-
FUNCTIONS (see Subsection 6.2) for the function in question is
ignored. Such a declaration instructs the system that for each
of the functions f , auxiliary functions will be created
i
according to the following rules. If x is T, then f <> will
i,j i
be created to represent the value of f , in the sense described
i
in Section 6 above. If x is F then f <>signal will be created
i,j i
to represent the signal of f , also in the sense described in
i
Section 6 above, while if x is a special variable or state
i,j
variable v then f will similarly be created to represent the
i
value of v after a call of f . Note however that just as with
i
the proclamation (FORCE-AUXILIARY-FUNCTIONS T), an auxiliary
function for the signal, for a special variable, or for a state
variable will only be created when it ``makes sense'' to do so.
For the signal, this means that if the system can see that the
signal is always F then it will not bother to create such a
function. For a special variable or state variable, the system
will not bother to create such a function when it can deduce that
a call of the function does not alter the value of that variable.
For example, the declaration
(declare (functions (*cl-sweep1 ans)))
instructs the system that regardless of the global state, the
system should create a sub-function *CL-SWEEP1 of *CL-SWEEP1
if it cannot determine that ANS is unchanged by every call of
SWEEP1; and, it should not create any other sub-functions
auxiliary to SWEEP1.
More generally, x is also allowed instead to be a pair (v
i,j
name), where v is as above (i.e. something that we have already
allowed to be x ) and name is the name that we wish to give the
i,j
auxiliary function (which should be a new name). So for example,
the declaration
(declare (functions (*cl-sweep1 t (ans foo))))
would result in a the creations of functions just as in the
SWEEP1 example above, except that the sub-function corresponding
to ANS would be called FOO instead of *CL-SWEEP1.
7.3 EVENTS declarations
The syntax for EVENTS declarations is
(EVENTS (event x ... x )
1 1,1 1,n
1
...
(event x ... x ))
k k,1 k,n
k
where each x is an event of type PROVE-LEMMA, DEFN, ADD-AXIOM,
i,j
CONSTRAIN, DCL, FUNCTIONALLY-INSTANTIATE, PROCLAIM-RCL, ENABLE,
DISABLE, or TOGGLE(Implementation note: the list of event types
is stored in the Lisp variable *ALL-EVENT-TYPES*.). In the
presence of such a hint, it is the case that immediately after
completion of event (where 1 L i L k), the events in the list
i
(x ... x ) are run in sequence.
i,1 i,n
i
7.4 POSTPROCESS declarations
The syntax for POSTPROCESS declarations is
(postprocess (f status )
1 1
...
(f status ))
k k
where each status is T, NIL, COMPLETE, or CONSTANTS. Such a
i
declaration has the effect that for each name f that is the name
i
of a DEFN event, definition postprocessing will have status
status for that definition, in the sense of Subsection 6.4.
i
Here is an example. Because of the postprocess declaration
below, the body of the auxiliary function *CL-BBB<> is simplified
to a constant but the auxiliary function *CL-BBB is not,
even though it could be.
>(defun-rcl bbb (x)
(declare (functions (*cl-bbb t ans))
(postprocess (*cl-bbb<> t)
(*cl-bbb nil)))
(if (consp x)
(bbb (cdr x))
(progn (setq ans 3) 4)))
Used no non-boot-strap lemmas or functions in the simplification process.
(DEFN *CL-BBB<>
(X)
(IF (LISTP X) (*CL-BBB<> (CDR X)) 4))
Linear arithmetic and the lemma CDR-LESSP can be used to prove that the
measure (COUNT X) decreases according to the well-founded relation LESSP in
each recursive call. Hence, *CL-BBB<> is accepted under the definitional
principle. Note that (NUMBERP (*CL-BBB<> X)) is a theorem.
[ 0.1 0.1 0.1 ]
[[[[[ Replacing definition of *CL-BBB<> with a simpler one: ]]]]]
(DEFN *CL-BBB<> (X) 4)
WARNING: X is in the arglist but not in the body of the definition of
*CL-BBB<>.
Observe that (NUMBERP (*CL-BBB<> X)) is a theorem.
[ 0.1 0.0 0.0 ]
*CL-BBB<>
(DEFN *CL-BBB
(X)
(IF (LISTP X)
(*CL-BBB (CDR X))
3))
Linear arithmetic and the lemma CDR-LESSP can be used to prove that the
measure (COUNT X) decreases according to the well-founded relation LESSP in
each recursive call. Hence, *CL-BBB is accepted under the definitional
principle. Note that (NUMBERP (*CL-BBB X)) is a theorem.
[ 0.1 0.1 0.1 ]
*CL-BBB
(DEFN *CL-BBB
(.RCL-FLG X ANS)
(CASE .RCL-FLG
(*1*TRUE (*CL-BBB<> X))
(ANS (*CL-BBB X))
(OTHERWISE F)))
WARNING: ANS is in the arglist but not in the body of the definition of
*CL-BBB.
From the definition we can conclude that:
(OR (FALSEP (*CL-BBB .RCL-FLG X ANS))
(NUMBERP (*CL-BBB .RCL-FLG X ANS)))
is a theorem.
[ 0.1 0.0 0.1 ]
*CL-BBB
8. GLOBAL SWITCHES AND UTILITIES
Recall that the global state may be examined by submitting the
command (RCL-STATUS), which reports the settings induced by
PROCLAIM-RCL events (cf. Section 6) as well as the settings of
certain user-settable Lisp variables. Those variables --
*UNWIND-PROTECT-IN-RUN-RCL-EVENTS-FLG*, *PRINT-SIMPLIFICATION-
INFO-FLG*, and *INSTRUMENT-FLG* -- are described in this section.
The settings of these variables have no effect on the database;
in particular, they have no effect on the libraries created by a
PROVEALL. This is why we have chosen not to implement these
switches using the PROCLAIM-RCL mechanism. Nevertheless, they
can be helpful to the user while he is interacting with the
system. The utilities UBT-RCL and RCL-STATUS are also described
in this section.
8.1 The switch *UNWIND-PROTECT-IN-RUN-RCL-EVENTS-FLG*
Default: T
The default setting ensures that the system automatically
unwinds the database state when an error occurs in the middle of
a DEFUN-RCL, DEFMACRO-RCL, or DO-RCL form. That is, if such a
form does not run to completion successfully (this includes the
possibility that there is some event created by the form that
fails), then all events that have been created by this form are
undone so that the database (as reflected by the Lisp variable
CHRONOLOGY) is the same as the database in place at the time the
form was submitted.
If one wishes to leave the events in place up to the failed
event, one may (SETQ *UNWIND-PROTECT-IN-RUN-RCL-EVENTS-FLG* NIL).
This feature can be useful if, for example, a DEFN fails to be
accepted and one wants to explore the problem in the context of
the auxiliary functions that were accepted before the problem
function.
8.2 The switch *PRINT-SIMPLIFICATION-INFO-FLG*
Default: T
This flag is the cause of the simplification message printed
just before the printing of each DEFN event that arises from an
RCL definition. That message is suppressed when *PRINT-
SIMPLIFICATION-INFO-FLG* is NIL. However, when this flag is not
NIL, the system tells the user which lemmas may have been used in
the simplification process(Using the PC-NQTHM rewriter). In
general, lemmas that are part of the ``boot-strap''(to be
precise, that are defined in the Lisp global variable
BOOT-STRAP-INSTRS, which is modified from NQTHM by the RCL source
file boot.lisp) are not mentioned here; however, in the special
case where *PRINT-SIMPLIFICATION-INFO-FLG* is BOOT, the system
prints these out as well. Here is an example.
>*print-simplification-info-flg*
T
>(defun-rcl foo (x) (if (consp x) (cons (car x) 3) nil))
Used no non-boot-strap lemmas or functions in the simplification process.
(DEFN *CL-FOO
(.RCL-FLG X)
(IF (EQUAL .RCL-FLG T)
(IF (LISTP X) (CONS (CAR X) 3) NIL)
F))
Observe that:
(OR (FALSEP (*CL-FOO .RCL-FLG X))
(LITATOM (*CL-FOO .RCL-FLG X))
(LISTP (*CL-FOO .RCL-FLG X)))
is a theorem.
[ 0.2 0.0 0.0 ]
*CL-FOO
T
>(ubt)
*CL-FOO
>(setq *print-simplification-info-flg* nil)
NIL
>(defun-rcl foo (x) (if (consp x) (cons (car x) 3) nil))
(DEFN *CL-FOO
(.RCL-FLG X)
(IF (EQUAL .RCL-FLG T)
(IF (LISTP X) (CONS (CAR X) 3) NIL)
F))
Observe that:
(OR (FALSEP (*CL-FOO .RCL-FLG X))
(LITATOM (*CL-FOO .RCL-FLG X))
(LISTP (*CL-FOO .RCL-FLG X)))
is a theorem.
[ 0.1 0.0 0.1 ]
*CL-FOO
T
>(ubt)
*CL-FOO
>(setq *print-simplification-info-flg* 'boot)
BOOT
>(defun-rcl foo (x) (if (consp x) (cons (car x) 3) nil))
Used the following lemmas and functions in the simplification process:
*CL-CONS<>-REWRITE, NOT, *CL-CAR<>-IS-CAR, NON-NILP-*CL-CONSP<>, and
NON-NILP-EXPANDER.
(DEFN *CL-FOO
(.RCL-FLG X)
(IF (EQUAL .RCL-FLG T)
(IF (LISTP X) (CONS (CAR X) 3) NIL)
F))
Observe that:
(OR (FALSEP (*CL-FOO .RCL-FLG X))
(LITATOM (*CL-FOO .RCL-FLG X))
(LISTP (*CL-FOO .RCL-FLG X)))
is a theorem.
[ 0.1 0.0 0.0 ]
*CL-FOO
T
>
8.3 The switch *INSTRUMENT-FLG*
Default: NIL
When *INSTRUMENT-FLG* is non-NIL, information is printed to
the screen whenever any of the simplification routines discussed
in Section 9 have an effect. The messages are perhaps a bit
obscure, but we expect them to be of interest mainly to people
who are already quite familiar with these routines, say by having
read [3].
If output is being directed to a file by PROVEALL, then this
information is written to the file with extension ``.err''. In
the special case that *INSTRUMENT-FLG* is FILE-ONLY, this
information will only be printed when during a PROVEALL.(More
precisely, it will only be printed when ERR-FILE is not NIL.)
Finally, *INSTRUMENT-FLG* is also allowed to be a list of zero or
more of the six routines discussed in Section 9: ELIMINATE-
EXCESS-VARIABLES-SET, DROP-EXCESS-FORMALS, OPEN-FORWARD-
REFERENCES, RCL-TRIM-DEFNS-WITH-RESTRICTIONS, ELIMINATE-
SUPERFLUOUS-PARAMETERS, and REPLACE-WITH-CONSTANTS-IN-DEFN.
8.4 The utility UBT-RCL
Before explaining this utility in detail, let us explain
simply what we expect to be the most common usage:
(UBT-RCL T)
instructs the system to undo at least one event, back through the
start of the most recent event sequence created by DEFUN-RCL,
DEFMACRO-RCL, or DO-RCL. In fact, (UBT-RCL T) is an anomalous
case, being equivalent to (UBT-RCL 0 T). Other than this
anomalous case, the general syntax for UBT-RCL is as follows:
details are given below.
(UBT-RCL &OPTIONAL n flag)
where n is a non-negative integer or an event name (just as for
the nqthm utility UBT) and a non-NIL flag argument means,
roughly, ``undo further if necessary back to the start of a
DEFUN-RCL, DEFMACRO-RCL, or DO-RCL form.'' Here is a more
careful description.
Recall that the NQTHM utility UBT takes an optional argument
(default: 0) and pops that many events off the (history)
chronology if the argument is a positive integer, and otherwise,
assuming that the argument is the name of an event, undoes all
events up to and including the given named event. UBT-RCL is
similar, but is intended to make it possible to consider all
events caused by a single DEFUN-RCL, DEFMACRO-RCL, or DO-RCL as a
single event for the purpose of undoing. In fact it works
exactly as does UBT, with the following additional action. If
the earliest event undone is the corresponding NQTHM function for
some Lisp function defined by the user with DEFUN-RCL or
DEFMACRO-RCL (possibly inside DO-RCL), or if the optional second
argument is supplied (and is not NIL), then the system undoes
events back up to (and not including) the most recent ``starting
point''. By a ``starting point'' we mean an event immediately
before a sequence of one or more events arising from a DEFUN-RCL,
DEFMACRO-RCL, or DO-RCL form.
8.5 The utility RCL-STATUS
The command RCL-STATUS (actually, a Lisp function of no
arguments) is rather self-explanatory. Here is an example.
>(rcl-status)
List of current RCL special variables: (*TEMP* *UVW*)
... Current value of *UNWIND-PROTECT-IN-RUN-RCL-EVENTS-FLG* is NIL.
... Current value of *PRINT-SIMPLIFICATION-INFO-FLG* is T.
... Current value of *INSTRUMENT-FLG* is T.
... Definition postprocessing status: T.
... Auxiliary functions forced? NO.
... Auxiliary lemmas inhibited? NO.
NIL
>
9. THE ALGORITHM
This final section gives an informal introduction to our
translation algorithm, especially to the various
optimizations/simplifications that are performed. A rigorous
account will appear in [3].
9.1 Creating the initial DEFNs
The basic algorithm, loosely stated, is a symbolic execution
of code. That is, the body of a Lisp definition is traversed,
and as this takes place, the resulting Lisp state is maintained
at every point of the execution. Let us call these
representations of Lisp state RCL-state data structures. Each
RCL-state structure has four components(actually 5, but the fifth
one is for the code itself, and we choose not to explain that
here). One component is the ``binding stack'', which associates
values with variables (both lexical and special). One component
is for the ``state variables''; currently the only state variable
is .PLISTS, which represents the property lists as an association
list associating symbols with lists of pairs of the form (CONS
property value). One component represents the ``signal'', which
is normally F (false), representing absence of a condition, but
which becomes ('THROW ) when a THROW form is encountered
whose first argument evaluates to , and rather similarly for
RETURN-FROM, GO, and ERR, which is an RCL approximation to the
Common Lisp function ERROR (see the next subsection). The final
component is for the value of the form. The values of each
variable in the binding stack, as well as .PLISTS, the signal,
and the value, are all terms in the NQTHM logic. The initial
assumption is that no function depends on or sets the (global)
value of any special variable (or .PLISTS), nor does any function
cause any signal other than F. After the function (or functions,
if one has multiple definitions, as is generally the case with
DO-RCL) is thus processed, an account is taken of which
additional variables might be read or set after all, and the
process is repeated. Each time the process is repeated, any new
variables that are discovered to be potentially set or read are
thus noted, and variables already noted as set or read are never
un-noted, so since these variable sets are finite, the monotone
nature of this procedure guarantees termination.
The result of this stage is essentially an association of
NQTHM function names with their formals (including .RCL-FLG and
perhaps extra formals from special and state variables) and
RCL-state data structures.(Implementation note: this stage is
represented by the Lisp function DEFUN-RCL=RESULT-LIST.)
There can actually be quite a bit of simplification done even
at this initial stage, since the PC-NQTHM simplifier is used
throughout this stage. Consider the following example from
Section 2. (The definition of the RCL function TEST had already
been processed at that point.)
>(defun-rcl newtest (x)
(let ((*uvw* *uvw*))
(setq *temp* nil)
(test (cons x x))))
Used no non-boot-strap lemmas or functions in the simplification process.
(DEFN *CL-NEWTEST
(.RCL-FLG X *UVW*)
(CASE .RCL-FLG
(*1*TRUE (*CL-TEST T (CONS X X) *UVW*))
(*1*FALSE (*CL-TEST F (CONS X X) *UVW*))
(*TEMP* NIL)
(OTHERWISE F)))
[ 0.2 0.0 0.0 ]
*CL-NEWTEST
T
>
Suppose that we wanted the value of the signal to be printed out
explicitly, rather than by way of reference to *CL-TEST. Then
one could prove the following rewrite rule before submitting the
(DEFUN-RCL NEWTEST ...) form.
(prove-lemma *cl-test-f-rewrite (rewrite)
(equal (*cl-test f x *uvw*)
(if (listp x) f '(throw badtest))))
The DEFN event below differs from the one above in that it has
used the above rewrite rule to replace the *1*FALSE branch of the
CASE with (IF (LISTP (CONS X X)) F '(THROW BADTEST)), which in
turn simplifies to F. In fact, no explicit case for the signal is
even constructed at all in the DEFN event below, and in fact the
ERROR-SIGNALS property of *CL-NEWTEST is NIL.
>(defun-rcl newtest (x)
(let ((*uvw* *uvw*))
(setq *temp* nil)
(test (cons x x))))
Used the following non-boot-strap lemmas and functions in the simplification
process: *CL-TEST-F-REWRITE.
(DEFN *CL-NEWTEST
(.RCL-FLG X *UVW*)
(CASE .RCL-FLG
(*1*TRUE (*CL-TEST T (CONS X X) *UVW*))
(*TEMP* NIL)
(OTHERWISE F)))
[ 0.2 0.0 0.0 ]
*CL-NEWTEST
T
>
Obviously this example is contrived, but it does serve to
illustrate two points. First, rewrite rules are used in the
translation of RCL definitions. Second, functions are not
automatically expanded in the simplification process; the call of
(*CL-TEST F X *UVW*) in the *1*FALSE case above did not open up
until we proved a rewrite rule to tell it to do so. One final
rather subtle fact: such rules generally need to be proved ahead
of time, i.e. they cannot be done by way of EVENTS declarations
(cf. Subsection 7.3). This is because simplification with
rewrite rules is only done before the processing of any events is
begun. (There is one unusual exception, namely, simplification
with rewrite rules may be done by definition postprocessing, cf.
Subsections 6.4 and 7.4. But this is rather rare.)
9.2 Errors: The ERR function
Before we go on to describe the next step in the translation
algorithm, let us discuss one useful subtlety in our notion of
signal. Recall that we are only claiming a partial correctness
semantics, in the sense that functions defined by DEFUN-RCL are
represented by NQTHM functions that correspond only on those
inputs, and for those Lisp states, where evaluation terminates
and in fact terminates in other than an error. For the purposes
of this notion, ``error'' includes only those Lisp states where
the signal is (ERROR). This semantics turns out to be quite
convenient, as illustrated by the example in the appendix.
Roughly speaking, for any call of a Lisp function that is not
among the ones currently being translated to NQTHM, we ``cheat''
by assuming that that call cannot cause signal of (ERROR), and we
have heuristics to take advantage of that assumption. For any
call of a Lisp function that is among the ones currently being
translated to NQTHM, no such special treatment is afforded.
Hence, one may use the RCL function ERR to sometimes signal an
error so that the current function can be accepted, and yet not
pay the price of a case split on the error signal when later
functions call this one.
Here is a rather involved, but very illustrative example, of
this treatment of ERR. Here we use ERR indirectly by way of the
macro ASSERT, which is included in the startup library:
(defmacro-rcl assert (form)
`(or ,form
(err '(assertion failed for ,form))))
For readers not comfortable with backquote, here is the same
definition expressed without backquote.
(defmacro-rcl assert (form)
(list 'or
form
(list 'err
(list 'quote
(list 'assertion
'failed
'for
form)))))
Here then is a transcript of a successful PROVEALL which runs
directly on top of the startup library and illustrates the use of
ASSERT (in the (DEFUN-RCL FACT ...) form below).
^L
(ENABLE IPLUS-NUMBERP)
[ 0.0 0.0 0.0 ]
IPLUS-NUMBERP-ON
^L
(ENABLE IDIFFERENCE-NUMBERP)
[ 0.0 0.0 0.0 ]
IDIFFERENCE-NUMBERP-ON
^L
(ENABLE IQUOTIENT-NUMBERP)
[ 0.0 0.0 0.0 ]
IQUOTIENT-NUMBERP-ON
^L
(ENABLE ILESSP-NUMBERP)
[ 0.0 0.0 0.0 ]
ILESSP-NUMBERP-ON
^L
(ENABLE IZEROP-NUMBERP)
[ 0.0 0.0 0.0 ]
IZEROP-NUMBERP-ON
^L
(ENABLE NUMBERP-IS-INTEGERP)
[ 0.0 0.0 0.0 ]
NUMBERP-IS-INTEGERP-ON
^L
(PROVE-LEMMA LESSP-0-NUMBERP
(REWRITE)
(IMPLIES (LESSP 0 X) (NUMBERP X)))
WARNING: LESSP-0-NUMBERP will slow down the theorem-prover because it will
cause backward chaining on every instance of a primitive type expression.
This simplifies, unfolding LESSP, to:
T.
Q.E.D.
[ 0.1 0.0 0.0 ]
LESSP-0-NUMBERP
^L
(PROVE-LEMMA ILESSP-0-LESSP
(REWRITE)
(IMPLIES (NUMBERP X)
(EQUAL (ILESSP X Y) (LESSP X Y)))
((ENABLE ILESSP)))
<<<..... short proof omitted .....>>>
Q.E.D.
[ 0.1 0.7 0.0 ]
ILESSP-0-LESSP
^L
(DEFUN-RCL FACT
(N)
(PROG ((ACC 1))
LOOP
(ASSERT (AND (< 0 ACC) (< 0 N)))
(WHEN (EQUAL N 1) (RETURN ACC))
(SETQ ACC (* N ACC))
(SETQ N (1- N))
(GO LOOP)))
Used the following non-boot-strap lemmas and functions in the simplification
process: NUMBERP-IS-INTEGERP, ITIMES-NUMBERP, LESSP-0-NUMBERP, *CL-RETURN,
*CL-WHEN, ILESSP-0-LESSP, NON-NILP-*CL-<<>, *CL-AND, *CL-OR, *CL-ASSERT, and
*CL-PROG.
(DEFN *CL-FACT-TAGBODY-0
(.RCL-FLG ACC N)
(COND ((EQUAL .RCL-FLG T)
(IF (LESSP 0 ACC)
(IF (LESSP 0 N)
(IF (EQUAL N 1)
ACC
(*CL-FACT-TAGBODY-0 T
(TIMES N ACC)
(IDIFFERENCE N 1)))
'(ASSERTION FAILED FOR
(AND (< 0 ACC) (< 0 N))))
'(ASSERTION FAILED FOR
(AND (< 0 ACC) (< 0 N)))))
((LESSP 0 ACC)
(IF (LESSP 0 N)
(IF (EQUAL N 1)
'(RETURN-FROM NIL)
(*CL-FACT-TAGBODY-0 F
(TIMES N ACC)
(IDIFFERENCE N 1)))
'(ERROR)))
(T '(ERROR))))
Linear arithmetic, the lemmas COUNT-NUMBERP, IDIFFERENCE-NUMBERP, and
DIFFERENCE-ADD1-ARG2, and the definitions of DIFFERENCE, LESSP, and EQUAL
establish that the measure (COUNT N) decreases according to the well-founded
relation LESSP in each recursive call. Hence, *CL-FACT-TAGBODY-0 is accepted
under the definitional principle. Observe that:
(OR (OR (NUMBERP (*CL-FACT-TAGBODY-0 .RCL-FLG ACC N))
(LISTP (*CL-FACT-TAGBODY-0 .RCL-FLG ACC N)))
(EQUAL (*CL-FACT-TAGBODY-0 .RCL-FLG ACC N)
ACC))
is a theorem.
[ 0.4 3.2 0.1 ]
*CL-FACT-TAGBODY-0
(DEFN *CL-FACT
(.RCL-FLG N)
(CASE .RCL-FLG
(*1*TRUE (*CL-FACT-TAGBODY-0 T 1 N))
(*1*FALSE (IF (EQUAL (*CL-FACT-TAGBODY-0 F 1 N)
'(RETURN-FROM NIL))
F
(*CL-FACT-TAGBODY-0 F 1 N)))
(OTHERWISE F)))
Note that:
(OR (FALSEP (*CL-FACT .RCL-FLG N))
(NUMBERP (*CL-FACT .RCL-FLG N))
(LISTP (*CL-FACT .RCL-FLG N)))
is a theorem.
[ 0.2 0.0 0.0 ]
*CL-FACT
T
^L
(DEFN FACTORIAL
(N)
(IF (ZEROP N)
1
(TIMES N (FACTORIAL (SUB1 N)))))
Linear arithmetic, the lemma COUNT-NUMBERP, and the definition of ZEROP
can be used to establish that the measure (COUNT N) decreases according to the
well-founded relation LESSP in each recursive call. Hence, FACTORIAL is
accepted under the principle of definition. From the definition we can
conclude that (NUMBERP (FACTORIAL N)) is a theorem.
[ 0.1 0.8 0.1 ]
FACTORIAL
^L
(PROVE-LEMMA FACT-FACTORIAL
(REWRITE)
(IMPLIES (AND (NOT (ZEROP N))
(NOT (ZEROP ACC)))
(EQUAL (*CL-FACT-TAGBODY-0 T ACC N)
(TIMES ACC (FACTORIAL N)))))
<<<..... proof omitted .....>>>
Q.E.D.
[ 0.1 20.8 0.6 ]
FACT-FACTORIAL
^L
(PROVE-LEMMA FACT-FACTORIAL-MAIN
(REWRITE)
(IMPLIES (NOT (ZEROP N))
(EQUAL (*CL-FACT T N) (FACTORIAL N))))
WARNING: Note that the rewrite rule FACT-FACTORIAL-MAIN will be stored so as
to apply only to terms with the nonrecursive function symbol *CL-FACT.
<<<..... short proof omitted .....>>>
Q.E.D.
[ 0.1 1.3 0.0 ]
FACT-FACTORIAL-MAIN
9.3 Simplification of RCL state data structures
At this stage we take the association of names to RCL-state
structures and repeatedly perform three kinds of optimizations,
in sequence, until there is no further change.(Implementation
note: the iterative repeating of these three optimizations is
performed by the Lisp function SIMPLIFY-DEFUN-RCL=RESULT-LIST.)
OPEN-FORWARD-REFERENCES takes functions that were introduced
for TAGBODY forms and opens up recursive calls for values of
.RCL-FLG and the TAG that are ``safe''. Here we say the a pair
(representing .RCL-FLG and the TAG) is safe if in the
branch of the body of the function corresponding to .RCL-FLG = x
and TAG = y, all the recursive calls of the function have TAG
parameters that occur strictly below y in the TAGBODY code.
DROP-EXCESS-FORMALS eliminates formal parameters that are no
longer needed for a function because they do not appear in its
associated RCL-state data structure.
ELIMINATE-EXCESS-VARIABLES-SET adjusts the RCL-state data
structure corresponding to a function, by noting special and
state variables that are unchanged (even though the
implementation conservatively ``guessed'' that they might be
changed) by execution of the function.
9.4 Mutual recursion analysis
Now that each function is associated with an appropriate
RCL-state structure, the association of RCL-state data structures
with names is used to create tentative DEFN events: the
variables-read are used to extend the formal parameter lists of
the original function(s); .RCL-FLG is added as a formal
parameter; and the body is a CASE statement on .RCL-FLG with one
case for the value, one case for the signal (if the system hasn't
deduced that it's always F), and one case for each variable set.
Then the mutual recursion analysis is done to create and order
the dependency classes, in the sense described in Section
4.(Implementation note: the function RCL-MUTUAL-DEFNS actually
performs this stage and the last, as well as the process of
turning RCL-state structures into DEFN events.)
9.5 Trimming definitions
Suppose now that we have a sequence of definitions, one of
which corresponds to our original DEFUN-RCL or DEFMACRO-RCL form
(or, more than one in the case that a DO-RCL form with more than
one definition was submitted), and the rest of which we have
called auxiliary. In fact, then, it should be permissible to
modify the auxiliary function definitions, as long as this has no
effect on the main functions. That is the idea behind what we
call ``trimming definitions''(Implementation note: this stage is
performed by the function RCL-TRIM-DEFNS-WITH-RESTRICTIONS.).
Here is an example that illustrates this process. The point
here is that the main function, *CL-REV1, only calls the function
*CL-REV1-TAGBODY-0 once, with the first two arguments in that
call being '*1*TRUE (i.e. T) and 'LOOP. It turns out that if we
modify the definition of *CL-REV1-TAGBODY-0 to be ``restricted''
to the branch of its definition in which its first two arguments
have those values, then the resulting definition is
``equivalent'' to the original, from the point of view of
*CL-REV1. We have set *INSTRUMENT-FLG* to the one-element list
(RCL-TRIM-DEFNS-WITH-RESTRICTIONS) (cf. preceding footnote) in
order to track this optimization. Sorry about the mess: please
read '*1*TRUE as T and '*1*FALSE as F.
>(defun-rcl rev1 (x)
(prog (acc)
loop
(when (not (consp x))
(return acc))
(setq acc (cons (car x) acc))
(setq x (cdr x))
(go loop)))
********************
RCL-TRIM-DEFNS-WITH-RESTRICTIONS
........................................
((*CL-REV1-TAGBODY-0
(.RCL-FLG TAG ACC X)
(IF (EQUAL .RCL-FLG '*1*TRUE)
(IF (LISTP X)
(*CL-REV1-TAGBODY-0 '*1*TRUE
'LOOP
(CONS (CAR X) ACC)
(CDR X))
ACC)
(IF (EQUAL .RCL-FLG '*1*FALSE)
(IF (LISTP X)
(*CL-REV1-TAGBODY-0 '*1*FALSE
'LOOP
(CONS (CAR X) ACC)
(CDR X))
'(RETURN-FROM NIL))
(IF (EQUAL .RCL-FLG 'ACC)
(IF (LISTP X)
(*CL-REV1-TAGBODY-0 'ACC
'LOOP
(CONS (CAR X) ACC)
(CDR X))
ACC)
(IF (EQUAL .RCL-FLG 'X)
(IF (LISTP X)
(*CL-REV1-TAGBODY-0 'X
'LOOP
(CONS (CAR X) ACC)
(CDR X))
X)
'*1*FALSE)))))
(*CL-REV1 (.RCL-FLG X)
(IF (EQUAL .RCL-FLG '*1*TRUE)
(*CL-REV1-TAGBODY-0 '*1*TRUE
'LOOP
'NIL
X)
'*1*FALSE)))
........................................
((*CL-REV1-TAGBODY-0 (.RCL-FLG TAG ACC X)
(IF (LISTP X)
(*CL-REV1-TAGBODY-0 '*1*TRUE
'LOOP
(CONS (CAR X) ACC)
(CDR X))
ACC))
(*CL-REV1 (.RCL-FLG X)
(IF (EQUAL .RCL-FLG '*1*TRUE)
(*CL-REV1-TAGBODY-0 '*1*TRUE
'LOOP
'NIL
X)
'*1*FALSE)))
********************
Used the following non-boot-strap lemmas and functions in the simplification
process: *CL-NOT-REWRITE, *CL-NOT<>-REWRITE, *CL-RETURN, *CL-WHEN, and
*CL-PROG.
(DEFN *CL-REV1-TAGBODY-0
(ACC X)
(IF (LISTP X)
(*CL-REV1-TAGBODY-0 (CONS (CAR X) ACC)
(CDR X))
ACC))
Linear arithmetic and the lemma CDR-LESSP inform us that the measure
(COUNT X) decreases according to the well-founded relation LESSP in each
recursive call. Hence, *CL-REV1-TAGBODY-0 is accepted under the definitional
principle. From the definition we can conclude that:
(OR (LISTP (*CL-REV1-TAGBODY-0 ACC X))
(EQUAL (*CL-REV1-TAGBODY-0 ACC X)
ACC))
is a theorem.
[ 0.1 0.1 0.1 ]
*CL-REV1-TAGBODY-0
(DEFN *CL-REV1
(.RCL-FLG X)
(IF (EQUAL .RCL-FLG T)
(*CL-REV1-TAGBODY-0 NIL X)
F))
Note that:
(OR (FALSEP (*CL-REV1 .RCL-FLG X))
(LITATOM (*CL-REV1 .RCL-FLG X))
(LISTP (*CL-REV1 .RCL-FLG X)))
is a theorem.
[ 0.1 0.0 0.0 ]
*CL-REV1
T
>
9.6 Eliminating superfluous parameters
The system is now ready to try once again to eliminate extra
formal parameters. However, while DROP-EXCESS-FORMALS (discussed
above in Subsection 9.3) is performed on RCL-state data
structures, the function ELIMINATE-SUPERFLUOUS-PARAMETERS is
applied to tentative DEFN events. Also, if analysis shows some
formal parameters to be irrelevant to the value of the function,
then at this stage we are even willing to drop .RCL-FLG and the
original formal parameters of the DEFUN if they are among the
superfluous formals, as long as the function in question is not
one of the original functions defined by the user. So for
example, if we had set *INSTRUMENT-FLG* to T, we would have seen
the following additional output immediately after the output for
RCL-TRIM-DEFNS-WITH-RESTRICTIONS (and before the DEFN of
*CL-REV1-TAGBODY-0) in the preceding subsection's example.
********************
ELIMINATE-SUPERFLUOUS-PARAMETERS:
(CALLED DROP-EXCESS-FORMALS-TERM ON CHANGED-FORMALS-ALIST OF
((*CL-REV1-TAGBODY-0 (ACC X)
(.RCL-FLG TAG ACC X)))
AND NAME *CL-REV1-TAGBODY-0 AND ORIGINAL FORMALS
(.RCL-FLG TAG ACC X))
........................................
;; Previous body of *CL-REV1-TAGBODY-0
(IF (LISTP X)
(*CL-REV1-TAGBODY-0 '*1*TRUE
'LOOP
(CONS (CAR X) ACC)
(CDR X))
ACC)
........................................
;; Revised body of *CL-REV1-TAGBODY-0
(IF (LISTP X) (*CL-REV1-TAGBODY-0 (CONS (CAR X) ACC) (CDR X)) ACC)
********************
;; The following output corresponds to the definition of *CL-REV1.
********************
ELIMINATE-SUPERFLUOUS-PARAMETERS:
(CALLED DROP-EXCESS-FORMALS-TERM ON CHANGED-FORMALS-ALIST OF
((*CL-REV1-TAGBODY-0 (ACC X)
(.RCL-FLG TAG ACC X)))
AND NAME *CL-REV1 AND ORIGINAL FORMALS
(.RCL-FLG X))
........................................
;; Previous body of *CL-REV1
(IF (EQUAL .RCL-FLG '*1*TRUE)
(*CL-REV1-TAGBODY-0 '*1*TRUE
'LOOP
'NIL
X)
'*1*FALSE)
........................................
;; Revised body of *CL-REV1
(IF (EQUAL .RCL-FLG '*1*TRUE) (*CL-REV1-TAGBODY-0 'NIL X) '*1*FALSE)
********************
9.7 Recursion elimination
The final major simplification is recursion elimination in
certain circumstances. This is exactly the optimization that was
called ``definition postprocessing'' in Subsections 6.4 and 7.4.
As we mentioned before, unlike the other optimizations, we only
trust the soundness of this one if the definition in question is
already acceptable before the optimization. The rough idea is
that if one has a branch of a definition such that the ``only way
out'' is with a fixed constant value, then one can replace that
branch by that constant.(Implementation note: this function is
called REPLACE-WITH-CONSTANTS-IN-DEFN.) See Subsection 6.4 for
an example.
REFERENCES
1. M. Kaufmann, ``A Verification System for a Subset of Common
Lisp'', Internal Note 110, Computational Logic, Inc.,
January 1989.
2. Guy L. Steele Jr., Common LISP: The Language, Digital
Press, 1984.
3. M. Kaufmann, ``Rose Common Lisp: A Lisp Verification
System'', Technical Report, Computational Logic, Inc., to
appear.
4. R. S. Boyer and J S. Moore, A Computational Logic Handbook,
Academic Press, Boston, 1988.
5. R. S. Boyer and J S. Moore, A Computational Logic, Academic
Press, New York, 1979.
6. M. Kaufmann, ``A User's Manual for an Interactive
Enhancement to the Boyer-Moore Theorem Prover'', Technical
Report 19, Computational Logic, Inc., May 1988.
7. M. Kaufmann, ``Addition of Free Variables to an Interactive
Enhancement of the Boyer-Moore Theorem Prover'', Tech.
report 42, Computational Logic, Inc., 1717 West Sixth
Street, Suite 290 Austin, TX 78703, 1989.
8. W. Bevier, ``A Library for Hardware Verification'',
Internal Note 57, Computational Logic, Inc., June 1988.
9. M. Kaufmann, ``A mutual recursion and dependency analysis
tool for NQTHM'', Internal Note 99, Computational Logic,
Inc., November 1988.
`