BIBLIOGRAPHY

Parent topic:  MISCELLANEOUS
Home

Below is a list of notes and reports pertaining to ACL2.

R. Boyer, M. Kaufmann, and J Moore, ``A short note on some advantages of Acl2.'' CLI Internal Note 215, Jan., 1991. See the files reports/note-215-acl2-advantages.* under the ACL2 source directory.

``High-level Correctness of ACL2: A Story.'' See the file reports/story.txt under the ACL2 source directory.

M. Kaufmann and J Moore, ``Design Goals for ACL2.'' CLI Technical Report 101, August, 1994. See the files reports/acl2-design.* under the ACL2 source directory.

BREAKS

Parent topic:  MISCELLANEOUS
Home

Example:
Broken at PROVE.  Type :H for Help.
>>:Q


ACL2 !>

If a break occurs, e.g. because of a bug in ACL2 or a user interrupt, the break will run a Common Lisp read-eval-print loop, not an ACL2 read-eval-print loop. This may not be obvious if the prompts in the two loops are similar. Because you are typing to a Common Lisp evaluator, you must be careful. It is possible to damage your ACL2 state in irreparable ways by executing non-ACL2 Common Lisp. It is even possible to disrupt and render inaccurate the interrupted evaluation of a simple ACL2 expression.

Quitting from the break (as with :q in AKCL) will return to the innermost ACL2 read-eval-print loop. Before the loop is continued, any pending cleanup forms from acl2-unwind-protects are evaluated (unless acl2::*acl2-panic-exit-flg* is non-nil, in which case no cleanup is done).

If at any time you type the token #. to either a raw lisp break or to the ACL2 read-eval-print loop, an abort is executed. Control is passed to the outermost ACL2 read-eval-print loop (lp). Again, unwind-protection cleanup forms are executed first.

CHECK-SUM

Parent topic:  MISCELLANEOUS
Home

A ``check sum'' is an integer in some fixed range computed from the printed representation of an object, e.g., the sum, modulo 2**32, of the ascii codes of all the characters in the printed representation.

Ideally, you would like the check sum of an object to be uniquely associated with that object, like a fingerprint. It could then be used as a convenient way to recognize the object in the future: you could remember the check sum (which is relatively small) and when an object is presented to you and alleged to be the special one you could compute its check sum and see if indeed it was. Alas, there are many more objects than check sums (after all, each check sum is an object, and then there's t). So you try to design a check sum algorithm that maps similar looking objects far apart, in the hopes that corruptions and counterfeits -- which appear to be similar to the object -- have different check sums. Nevertheless, the best you can do is a many-to-one map. If an object with a different check sum is presented, you can be positive it is not the special object. But if an object with the same check sum is presented, you have no grounds for positive identification.

The basic check sum algorithm in ACL2 is called check-sum-obj, which computes the check sum of an ACL2 object. Roughly speaking, we scan the print representation of the object and, for each character encountered, we multiply the ascii code of the character times its position in the stream (modulo a certain prime) and then add (modulo a certain prime) that into the running sum. This is inaccurate in many senses (for example, we don't always use the ascii code and we see numbers as though they were printed in base 127) but indicates the basic idea.

ACL2 uses check sums to increase security in the books mechanism; see certificate.

COMMAND

Parent topic:  MISCELLANEOUS
Home

...the word ``command'' usually refers to a top-level form whose evaluation produces a new logical world.

Typical commands are:
(defun foo (x) (cons x x))
(defthm consp-foo (consp (foo x)))
(defrec pair (hd . tl) nil)

Both events and commands leave landmarks on the world that enable us to determine how the given world was created from the previous one. Most of your interactions will occur at the command level, i.e., you type commands, you print previous commands, and you undo back through commands. Commands are denoted by command descriptors. See command-descriptor.

COMMAND-DESCRIPTOR

Parent topic:  MISCELLANEOUS
Home

Examples:


:max      ; the command most recently typed by the user
:x        ; synonymous with :max
(:x -1)   ; the command before the most recent one
(:x -2)   ; the command before that
:x-2      ; synonymous with (:x -2)
5         ; the fifth command typed by the user
1         ; the first command typed by the user
0         ; the last command of the system initialization
-1        ; the next-to-last initialization command
:min      ; the first command of the initialization
fn        ; the command that introduced the logical name fn
(:search (defmacro foo-bar))
          ; the first command encountered in a search from :max to
          ; 0 that either contains defmacro and foo-bar in the 
          ; command form or contains defmacro and foo-bar in some 
          ; event within its block.

The recorded history of your interactions with the top-level ACL2 command loop is marked by the commands you typed that changed the logical world. Each such command generated one or more events, since the only way for you to change the logical world is to execute an event function. See command and see events. We divide history into ``command blocks,'' grouping together each world changing command and its events. A ``command descriptor'' is an object that can be used to describe a particular command in the history of the ongoing session.

Each command is assigned a unique integer called its ``command number'' which indicates the command's position in the chronological ordering of all of the commands ever executed in this session (including those executed to initialize the system). We assign the number 1 to the first command you type to ACL2. We assign 2 to the second and so on. The non-positive integers are assigned to ``prehistoric'' commands, i.e., the commands used to initialize the ACL2 system: 0 is the last command of the initialization, -1 is the one before that, etc.

The legal command descriptors are described below. We use n to denote any integer, sym to denote any logical name (see logical-name), and cd to denote, recursively, any command descriptor.

 command                   command
descriptor                described


:max   -- the most recently executed command (i.e., the one with
          the largest command number)
:x     -- synonymous with :max
:x-k   -- synonymous with (:x -k), if k is an integer and k>0
:min   -- the earliest command (i.e., the one with the smallest
          command number and hence the first command of the system
          initialization)
n      -- command number n  (If n is not in the
          range :min<=n<=:max, n is replaced by the nearest of :min
          and :max.)
sym    -- the command that introduced the logical name sym
(cd n) -- the command whose number is n plus the command number of
          the command described by cd
(:search pat cd1 cd2)
          In this command descriptor, pat must be either an atom or
          a true list of atoms and cd1 and cd2 must be command
          descriptors.  We search the interval from cd1 through cd2
          for the first command that matches pat.  Note that if cd1
          occurs chronologically after cd2, the search is
          ``backwards'' through history while if cd1 occurs
          chronologically before cd2, the search is ``forwards''.  A
          backwards search will find the most recent match; a
          forward search will find the chronologically earliest
          match.  A command matches pat if either the command form
          itself or one of the events in the block contains pat (or
          all of the atoms in pat if pat is a list).
(:search pat)
          the command found by (:search pat :max 0), i.e., the most
          recent command matching pat that was part of the user's
          session, not part of the system initialization.

CONSTRAINT

Parent topic:  MISCELLANEOUS
Home

Suppose that a given theorem, thm, is to be functionally instantiated using a given functional substitution, alist, as described in :DOC lemma-instance. What is the set of proof obligations generated? It is the set of all terms, tm, such that (a) tm mentions some function symbol in the domain of alist, and (b) either tm arises from the ``constraint'' on a function symbol ancestral in thm or some defaxiom or (ii) tm is the body of a defaxiom. Here, a function symbol is ``ancestral'' in thm if either it occurs in thm, or it occurs in the definition of some function symbol that occurs in thm, and so on.

The remainder of this note explains what we mean by ``constraint'' in the words above.

In a certain sense, function symbols are introduced in essentially two ways. The most common way is to use defun (or when there is mutual recursion, mutual-recursion or defuns). There is also a mechanism for introducing ``witness functions''; see defchoose. The documentation for these events describes the axioms they introduce, which we will call here their ``definitional axioms.'' These definitional axioms are generally the constraints on the function symbols that these axioms introduce.

However, when a function symbol is introduced in the scope of an encapsulate event, its constraints may differ from the definitional axioms introduced for it. For example, suppose that a function's definition is local to the encapsulate; that is, suppose the function is introduced in the signature of the encapsulate. Then its constraints include, at the least, those non-local theorems and definitions in the encapsulate that mention the function symbol.

Actually, it will follow from the discussion below that if the signature is empty for an encapsulate, then the constraint on each of its new function symbols is exactly the definitional axiom introduced for it. Intuitively, we view such encapsulates just as we view include-book events. But the general case, where the signature is not empty, is more complicated.

In the discussion that follows we describe in detail exactly which constraints are associated with which function symbols that are introduced in the scope of an encapsulate event. In order to simplify the exposition we make two cuts at it. In the first cut we present an over-simplified explanation that nevertheless captures the main ideas. In the second cut we complete our explanation by explaining how we view certain events as being ``lifted'' out of the encapsulate, resulting in a possibly smaller encapsulate, which becomes the target of the algorithm described in the first cut.

At the end of this note we present an example showing why a more naive approach is unsound.

Finally, before we start our ``first cut,'' we note that constrained functions always have guards of T. This makes sense when one considers that a constrained function's ``guard'' only appears in the context of a local defun, which is skipped. Note also that any information you want ``exported'' outside an encapsulate event must be there as an explicit definition or theorem. For example, even if a function foo has output type (mv t t) in its signature, the system will not know (true-listp (foo x)) merely on account of this information. Thus, if you are using functions like foo (constrained mv functions) in a context where you are verifying guards, then you should probably provide a :type-prescription rule for the constrained function, for example, the :type-prescription rule (true-listp (foo x)).

First cut at constraint-assigning algorithm. Quite simply, the formulas introduced in the scope of an encapsulate are conjoined, and each function symbol introduced by the encapsulate is assigned that conjunction as its constraint.

Clearly this is a rather severe algorithm. Let us consider two possible optimizations in an informal manner before presenting our second cut.

Consider the (rather artificial) event below. The function before1 does not refer at all, even indirectly, to the locally-introduced function sig-fn, so it is unfortunate to saddle it with constraints about sig-fn.

(encapsulate
 ((sig-fn (x) t))


 (defun before1 (x)
   (if (consp x)
       (before1 (cdr x))
     x))


 (local (defun sig-fn (x) (cons x x)))


 (defthm sig-fn-prop
   (consp (sig-fn x)))
 )

(defun before1 (x)
  (if (consp x)
      (before1 (cdr x))
    x))


(encapsulate
 ((sig-fn (x) t))


 (local (defun sig-fn (x) (cons x x)))


 (defthm sig-fn-prop
   (consp (sig-fn x)))
 )

More generally, suppose an event in an encapsulate event does not mention any function symbol in the signature of the encapsulate, nor any function symbol that mentions any such function symbol, and so on. (We might say that no function symbol from the signature is an ``ancestor'' of any function symbol occurring in the event.) Then we imagine moving the event, so that it appears in front of the encapsulate. We don't actually move it, but we pretend we do when it comes time to assign constraints. Thus, such definitions only introduce definitional axioms as the constraints on the function symbols being defined, and such theorems introduce no constraints.

Once this first optimization is performed, we have in mind a set of ``constrained functions.'' These are the functions introduced in the encapsulate that would remain after moving some of them out, as indicated above. Consider the collection of all formulas introduced by the encapsulate, except the definitional axioms, that mention these constrained functions. So for example, in the event below, no such formula mentions the function symbol after1.

(encapsulate
 ((sig-fn (x) t))


 (local (defun sig-fn (x) (cons x x)))


 (defthm sig-fn-prop
   (consp (sig-fn x)))


 (defun after1 (x)
   (sig-fn x))
 )

We may summarize the observations above as follows, after which we conclude with a more elaborate example.

Second cut at constraint-assigning algorithm. Given an encapsulate event, first move, to just in front of it and in the same order, all definitions and theorems for which none of the functions declared in the signature is ancestral. (In fact perform this process recursively, handling nested encapsulates.) Now collect up all formulas introduced in the encapsulate other than the definitional axioms, and restrict the set of constrained functions to those that are ancestral in at least one such formula. Finally, assign all formulas introduced in the resulting encapsulate as the common constraint on all function symbols that are introduced in the resulting encapsulate. (Thus, we imagine that the definitions of functions that are omitted from this list of function symbols, together with all non-definitional formulas omitted from this list of formulas, are moved outside the encapsulate, to just after it.)

Implementation note. In the implementation we do not actually move events, but we create constraints that pretend that we did.

Here is an example illustrating our constraint-assigning algorithm. It builds on the preceding examples.

(encapsulate
 ((sig-fn (x) t))


 (defun before1 (x)
   (if (consp x)
       (before1 (cdr x))
     x))


 (local (defun sig-fn (x) (cons x x)))


 (defthm sig-fn-prop
   (consp (sig-fn x)))


 (defun during (x)
   (if (consp x)
       x
     (cons (car (sig-fn x))
           17)))


 (defun before2 (x)
   (before1 x))


 (defthm before2-prop
   (atom (before2 x)))


 (defthm during-prop
   (implies (and (atom x)
                 (before2 x))
            (equal (car (during x))
                   (car (sig-fn x)))))


 (defun after1 (x)
   (sig-fn x))


 (defchoose after2 (x) (u)
   (and (< u x) (during x)))
 )

(SIG-FN X) is axiomatized to return one result.


In addition, we export AFTER2, AFTER1, DURING-PROP, BEFORE2-PROP, BEFORE2,
DURING, SIG-FN-PROP and BEFORE1.


The following constraint is associated with both of the functions DURING
and SIG-FN:


(AND (EQUAL (DURING X)
            (IF (CONSP X)
                X (CONS (CAR (SIG-FN X)) 17)))
     (CONSP (DURING X))
     (CONSP (SIG-FN X))
     (IMPLIES (AND (ATOM X) (BEFORE2 X))
              (EQUAL (CAR (DURING X))
                     (CAR (SIG-FN X)))))

We conclude by asking (and to a certain extent, answering) the following question: Isn't there an approach to assigning constraints that avoids over-constraining more simply than our ``second cut'' above? Perhaps it seems that given an encapsulate, we should simply assign to each locally defined function the theorems exported about that function. If we adopted that simple approach the events below would be admissible.

(encapsulate
 ((foo (x) t))
 (local (defun foo (x) x))
 (defun bar (x)
   (foo x))
 (defthm bar-prop
   (equal (bar x) x)
   :rule-classes nil))


(defthm foo-id
  (equal (foo x) x)
  :hints (("Goal" :use bar-prop)))


; The following event is not admissible in ACL2.


(defthm ouch!
  nil
  :rule-classes nil
  :hints
  (("Goal" :use
    ((:functional-instance foo-id
                           (foo (lambda (x) (cons x x))))))))

It's tempting to think we can fix this by including definitions, not just theorems, in constraints. But consider the following slightly more elaborate example. The problem is that we need to include as a constraint on foo not only the definition of bar, which mentions foo explicitly, but also abc, which has foo as an ancestor.

(encapsulate
 ((foo (x) t))
 (local (defun foo (x) x))
 (local (defthm foo-prop
          (equal (foo x) x)))
 (defun bar (x)
   (foo x))
 (defun abc (x)
   (bar x))
 (defthm abc-prop
   (equal (abc x) x)
   :rule-classes nil))


(defthm foo-id
  (equal (foo x) x)
  :hints (("Goal" :use abc-prop)))


; The following event is not admissible in ACL2.


(defthm ouch!
  nil
  :rule-classes nil
  :hints
  (("Goal" :use
    ((:functional-instance foo-id
                           (foo (lambda (x) (cons x x)))
                           (bar (lambda (x) (cons x x))))))))

COPYRIGHT

Parent topic:  MISCELLANEOUS
Home

``ACL2'' is an acronym for ``A Computational Logic for Applicative Common Lisp.'' ACL2 is copyrighted by Computational Logic, Inc. All rights reserved. For copyright and license information, see the file "LICENSE". Also see acknowledgements.

COROLLARY

Parent topic:  MISCELLANEOUS
Home

This is a low-level system function at the present time. See pr and see pr! instead. Also see rule-classes for the use of the symbol :corollary in specifying a rule class.

CURRENT-PACKAGE

Parent topic:  MISCELLANEOUS
Home

Current-package is an ld special (see ld). The accessor is (current-package state) and the updater is (set-current-package val state), or more conventionally, (in-package val). The value of current-package is actually the string that names the package. (Common Lisp's ``package'' objects do not exist in ACL2.) The current package must be known to ACL2, i.e., it must be one of the initial packages or a package defined with defpkg by the user.

When printing symbols, the package prefix is displayed if it is not the current-package and may be optionally displayed otherwise. Thus, if current-package is "ACL2" then the symbol 'ACL2::SYMB may be printed as SYMB or ACL2::SYMB, while 'MY-PKG::SYMB must be printed as MY-PKG::SYMB. But if current-package is "MY-PKG" then the former symbol must be printed as ACL2::SYMB while the latter may be printed as SYMB.

In Common Lisp, current-package also affects how objects are read from character streams. Roughly speaking, read and print are inverses if the current-package is fixed, so reading from a stream produced by printing an object must produce an equal object.

In ACL2, the situation is more complicated because we never read objects from character streams, we only read them from object ``streams'' (channels). Logically speaking, the objects in such a channel are fixed regardless of the setting of current-package. However, our host file systems do not support the idea of Lisp object files and instead only support character files. So when you open an object input channel to a given (character file) we must somehow convert it to a list of ACL2 objects. This is done by a deus ex machina (``a person or thing that appears or is introduced suddenly and unexpectedly and provides a contrived solution to an apparently insoluble difficulty,'' Webster's Ninth New Collegiate Dictionary). Roughly speaking, the deus ex machina determines what sequence of calls to read-object will occur in the future and what the current-package will be during each of those calls, and then produces a channel containing the sequence of objects produced by an analogous sequence of Common Lisp reads with *current-package* bound appropriately for each.

A simple rule suffices to make sane file io possible: before you read an object from an object channel to a file created by printing to a character channel, make sure the current-package at read-time is the same as it was at print-time.

DEFAULT-DEFUN-MODE

Parent topic:  MISCELLANEOUS
Home

When a defun is processed and no :mode xarg is supplied, the function default-defun-mode is used. To find the default defun-mode of the current ACL2 world, type (default-defun-mode (w state)). See defun-mode for a discussion of defun-modes. To change the default defun-mode of the ACL2 world, type one of the keywords :program or :logic.

The default ACL2 prompt displays the current default defun-mode by showing the character p for :program mode, and omitting it for :logic mode; see default-print-prompt. The default defun-mode may be changed using the keyword commands :program and :logic, which are equivalent to the commands (program) and (logic). Each of these names is documented separately: see program and see logic. The default defun-mode is stored in the table acl2-defaults-table and hence may also be changed by a table command. See table and also see acl2-defaults-table. Both mode-changing commands are events.

While events that change the default defun-mode are permitted within an encapsulate or the text of a book, their effects are local in scope to the duration of the encapsulation or inclusion. For example, if the default defun-mode is :logic and a book is included that contains the event (program), then subsequent events within the book are processed with the default defun-mode :program; but when the include-book event completes, the default defun-mode will still be :logic. Commands that change the default defun-mode are not permitted inside local forms.

DEFAULT-PRINT-PROMPT

Parent topic:  MISCELLANEOUS
Home

Example prompt:
ACL2 p!s>

p     ; when (default-defun-mode (w state)) is :program
!     ; when guard checking is on
s     ; when (ld-skip-proofsp state) is t

Also see ld-prompt to see how to install your own prompt.

Here are some examples with ld-skip-proofsp nil.

ACL2 !>    ; logic mode with guard checking on
ACL2 >     ; logic mode with guard checking off
ACL2 p!>   ; program mode with guard checking on
ACL2 p>    ; program mode with guard checking off

ACL2 >     ; guard checking off, ld-skip-proofsp nil
ACL2 s>    ; guard checking off, ld-skip-proofsp t
ACL2 !>    ; guard checking on, ld-skip-proofsp nil
ACL2 !s>   ; guard checking on, ld-skip-proofsp t

DEFUN-MODE

Parent topic:  MISCELLANEOUS
Home

Two ``defun-modes'' are supported, :program and :logic. Roughly speaking, :program mode allows you to prototype a function for execution without any proof burdens, while :logic mode allows you to add a new definitional axiom to the logic. The system comes up in :logic mode. Execution of functions whose defun-mode is :program may render ACL2 unsound! See defun-mode-caveat.

When you define a function in the ACL2 logic, that function can be run on concrete data. But it is also possible to reason deductively about the function because each definition extends the underlying logic with a definitional axiom. To insure that the logic is sound after the addition of this axiom, certain restrictions have to be met, namely that the recursion terminates. This can be quite challenging.

Because ACL2 is a programming language, you often may wish simply to program in ACL2. For example, you may wish to define your system and test it, without any logical burden. Or, you may wish to define ``utility'' functions -- functions that are executed to help manage the task of building your system but functions whose logical properties are of no immediate concern. Such functions might be used to generate test data or help interpret the results of tests. They might create files or explore the ACL2 data base. The termination arguments for such functions are an unnecessary burden provided no axioms about the functions are ever used in deductions.

Thus, ACL2 introduces the idea of the ``defun-mode'' of a function. The :mode keyword of defun's declare xarg allows you to specify the defun-mode of a given definition. If no :mode keyword is supplied, the default defun-mode is used; see default-defun-mode.

There are two defun-modes, each of which is written as a keyword:

:program -- logically undefined but executable outside deductive contexts.

:logic -- axiomatically defined as per the ACL2 definitional principle.

It is possible to change the defun-mode of a function from :program to :logic. We discuss this below.

We think of functions having :program mode as ``dangerous'' functions, while functions having :logic mode are ``safe.'' The only requirement enforced on :program mode functions is the syntactic one: each definition must be well-formed ACL2. Naively speaking, if a :program mode function fails to terminate then no harm is done because no axiom is added (so inconsistency is avoided) and some invocations of the function may simply never return. This simplistic justification of :program mode execution is faulty because it ignores the damage that might be caused by ``mis-guarded'' functions. See defun-mode-caveat.

We therefore implicitly describe an imagined implementation of defun-modes that is safe and, we think, effective. But please see defun-mode-caveat.

The default defun-mode is :logic. This means that when you defun a function the system will try to prove termination. If you wish to introduce a function of a different defun-mode use the :mode xargs keyword. Below we show fact introduced as a function in :program mode.

(defun fact (n)
  (declare (xargs :mode :program))
  (if (or (not (integerp n)) (= n 0))
      1
    (* n (fact (1- n)))))

ACL2 !>(fact 3)

However, the ACL2 theorem prover knows no axioms about fact. In particular, if the term (fact 3) arises in a proof, the theorem prover is unable to deduce that it is 6. From the perspective of the theorem prover it is as though fact were an undefined function symbol of arity 1. Thus, modulo certain important issues (see defun-mode-caveat), the introduction of this function in :program mode does not imperil the soundness of the system -- despite the fact that the termination argument for fact was omitted -- because nothing of interest can be proved about fact. Indeed, we do not allow fact to be used in logical contexts such as conjectures submitted for proof.

It is possible to convert a function from :program mode to :logic mode at the cost of proving that it is admissible. This can be done by invoking

(verify-termination fact)

(defun fact (n)
  (declare (xargs :mode :logic))
  (if (or (not (integerp n)) (= n 0))
      1
    (* n (fact (1- n)))))

Technically, verify-termination submits a redefinition of the :program mode function. This is permitted, even when ld-redefinition-action is nil, because the new definition is identical to the old (except for its :mode and, possibly, other non-logical properties).

See guard for a discussion of how to restrict the execution of functions. Guards may be ``verified'' for functions in :logic mode; see verify-guards.