ACL2 copyright, license, sponsorship

ACL2 Version 2.4 -- A Computational Logic for Applicative Common Lisp Copyright (C) 1999 University of Texas at Austin

This version of ACL2 is a descendent of ACL2 Version 1.9, Copyright (C) 1997 Computational Logic, Inc. See the documentation topic NOTES-2-0.

This program is free software; you can redistribute it and/or modify it under the terms of the GNU General Public License as published by the Free Software Foundation; either version 2 of the License, or (at your option) any later version.

This program is distributed in the hope that it will be useful, but WITHOUT ANY WARRANTY; without even the implied warranty of MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the GNU General Public License for more details.

You should have received a copy of the GNU General Public License along with this program. See the file LICENSE. If not, write to the Free Software Foundation, Inc., 675 Mass Ave, Cambridge, MA 02139, USA.

Written by: Matt Kaufmann and J Strother Moore email: and Department of Computer Sciences University of Texas at Austin Austin, TX 78712-1188 U.S.A.

Please also see acknowledgements.


the corollary formula of a rune

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.


the package used for reading and printing

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.


the default defun-mode of defun'd functions

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.


the default prompt printed by ld

Example prompt:
ACL2 p!s>
The prompt printed by ACL2 displays the current package, followed by a space, followed by zero or more of the three characters as specified below, followed by the character > printed one or more times, reflecting the number of recursive calls of ld. The three characters in the middle are as follows:
p     ; when (default-defun-mode (w state)) is :program
!     ; when guard checking is on
s     ; when (ld-skip-proofsp state) is t
See default-defun-mode, see set-guard-checking, and see ld-skip-proofsp.

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
Here are some examples with default-defun-mode of :logic.
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


determines whether a function definition is a logical act

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))
    (* n (fact (1- n)))))
No axiom is added to the logic as a result of this definition. By introducing fact in :program mode we avoid the burden of a termination proof, while still having the option of executing the function. For example, you can type
ACL2 !>(fact 3)
and get the answer 6. If you type (fact -1) you will get a hard lisp error due to ``infinite recursion.''

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)
which is equivalent to submitting the defun of fact, again, but in :logic mode.
(defun fact (n)
  (declare (xargs :mode :logic))
  (if (or (not (integerp n)) (= n 0))
    (* n (fact (1- n)))))
This particular event will fail because the termination argument requires that n be nonnegative. A repaired defun, for example with = replaced by <=, will succeed, and an axiom about fact will henceforth be available.

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.


functions with defun-mode of :program considered unsound

Technically speaking, in the current implementation, the execution of functions having defun-mode :program may damage the ACL2 system in a way that renders it unsound. See defun-mode for a discussion of defun-modes. That discussion describes an imagined implementation that is slightly different from this one. This note explains that the current implementation is open to unsoundness.

For discussion of a different soundness issue that is also related to function execution, see generalized-booleans.

The execution of a function having defun-mode :program may violate Common Lisp guards on the subroutines used. (This may be true even for calls of a function on arguments that satisfy its guard, because ACL2 has not verified that its guard is sufficient to protect its subroutines.) When a guard is violated at runtime all bets are off. That is, no guarantees are made either about the answer being ``right'' or about the continued rationality of the ACL2 system itself.

For example, suppose you make the following defun:

(defun crash (i) (declare (xargs :mode :program :guard (integerp i))) (car i))

Note that the declared guard does not in fact adequately protect the subroutines in the body of crash; indeed, satisfying the guard to crash will guarantee that the car expression is in violation of its guard. Because this function is admitted in :program-mode, no checks are made concerning the suitability of the guard. Furthermore, in the current ACL2 implementation, crash is executed directly in Common Lisp. Thus if you call crash on an argument satisfying its guard you will cause an erroneous computation to take place.

ACL2 !>(crash 7)

Error: Caught fatal error [memory may be damaged]
There is no telling how much damage is done by this errant computation. In some lisps your ACL2 job may actually crash back to the operating system. In other lisps you may be able to recover from the ``hard error'' and resume ACL2 in a damaged but apparently functional image.



ACL2 DOES NOT YET PROVIDE ANY MEANS OF REGAINING ASSURANCES OF SOUNDNESS AFTER THE INTRODUCTION OF A FUNCTION IN :PROGRAM MODE, EVEN IF IT IS ULTIMATELY CONVERTED TO :LOGIC MODE (since its execution could have damaged the system in a way that makes it possible to verify its termination and guards unsoundly).



This hopeless state of current affairs will change, we think. We think we have defined our functions ``correctly'' in the sense that they can be converted, without ``essential'' modification, to :logic mode. We think it very unlikely that a mis-guarded function in :program mode (whether ours or yours) will cause unsoundness without some sort of hard lisp error accompanying it. We think that ultimately we can make it possible to execute your functions (interpretively) without risk to the system, even when some have :program mode. In that imagined implementation, code using functions having :program mode would run more slowly, but safely. These functions could be introduced into the logic ex post facto, whereupon the code's execution would speed up because Common Lisp would be allowed to execute it directly. We therefore ask that you simply pretend that this is that imagined implementation, introduce functions in :program mode, use them as convenient and perhaps ultimately introduce some of them in :logic mode and prove their properties. If you use the system this way we can develop (or dismiss) this style of formal system development. BUT BE ON THE LOOKOUT FOR SCREWUPS DUE TO DAMAGE CAUSED BY THE EXECUTION OF YOUR FUNCTIONS HAVING :PROGRAM MODE!


an alternative to mutual-recursion

 (evenlp (x)
   (if (consp x) (oddlp (cdr x)) t))
 (oddlp (x)
   (if (consp x) (evenlp (cdr x)) nil)))

General Form: (DEFUNS defuns-tuple1 ... defuns-tuplen)

is equivalent to
  (DEFUN . defuns-tuple1)
  (DEFUN . defuns-tuplen))
In fact, defuns is the more primitive of the two and mutual-recursion is just a macro that expands to a call of defun after stripping off the defun at the car of each argument to mutual-recursion. We provide and use mutual-recursion rather than defuns because by leaving the defuns in place, mutual-recursion forms can be processed by the Emacs tags program. See mutual-recursion.


to disallow forced case splits

General Form:
ACL2 !>:disable-forcing   ; disallow forced case splits
See force for a discussion of forced case splits.

Disable-forcing is a macro that disables the executable counterpart of the function symbol force; see force. When you want to disable forcing in hints, use a form such as:

:in-theory (disable (:executable-counterpart force))


determine whether a given name or rune is disabled


:disabledp foo ; returns a list of all disabled runes whose base ; symbol is foo (see rune) (disabledp 'foo) ; same as above (i.e., :disabledp foo) :disabledp (:rewrite bar . 1) ; returns t if the indicated rune is ; disabled, else nil (disabledp (:rewrite bar . 1)); same as immediately above

Also see pr, which gives much more information about the rules associated with a given event.

Disabledp takes one argument, an event name or a rune. In the former case it returns the list of disabled runes associated with that name (in the sense that the rune's ``base symbol'' is that name; see rune). In the latter case it returns t if the given rune is disabled, and nil otherwise.


the well-founded less-than relation on ordinals up to epsilon-0

If x and y are both e0-ordinalps (see e0-ordinalp) then (e0-ord-< x y) is true iff x is strictly less than y. e0-ord-< is well-founded on the e0-ordinalps. When x and y are both nonnegative integers, e0-ord-< is just the familiar ``less than'' relation (<).

e0-ord-< plays a key role in the formal underpinnings of the ACL2 logic. In order for a recursive definition to be admissible it must be proved to ``terminate.'' By terminate we mean that the arguments to the function ``get smaller'' as the function recurses and this sense of size comparison must be such that there is no ``infinitely descending'' sequence of ever smaller arguments. That is, the relation used to compare successive arguments must be well-founded on the domain being measured.

The most basic way ACL2 provides to prove termination requires the user to supply (perhaps implicitly) a mapping of the argument tuples into the ordinals with some ``measure'' expression in such a way that the measures of the successive argument tuples produced by recursion decrease according to the relation e0-ord-<. The validity of this method rests on the well-foundedness of e0-ord-< on the e0-ordinalps.

Without loss of generality, suppose the definition in question introduces the function f, with one formal parameter x (which might be a list of objects). Then we require that there exist a measure expression, (m x), that always produces an e0-ordinalp. Furthermore, consider any recursive call, (f (d x)), in the body of the definition. Let hyps be the conjunction terms (each of which is either the test of an if in the body or else the negation of such a test) describing the path through the body to the recursive call in question. Then it must be a theorem that

  (IMPLIES hyps (E0-ORD-< (m (d x)) (m x))).
When we say e0-ord-< is ``well-founded'' on the e0-ordinalps we mean that there is no infinite sequence of e0-ordinalps such that each is smaller than its predecessor in the sequence. Thus, the theorems that must be proved about f when it is introduced establish that it cannot recur forever because each time a recursive call is taken (m x) gets smaller. From this, and the syntactic restrictions on definitions, it can be shown (as on page 44 in ``A Computational Logic'', Boyer and Moore, Academic Press, 1979) that there exists a function satisfying the definition; intuitively, the value assigned to any given x by the alleged function is that computed by a sufficiently large machine. Hence, the logic is consistent if the axiom defining f is added.

See e0-ordinalp for a discussion of the ordinals and how to compare two ordinals.

The definitional principle permits the use of relations other than e0-ord-< but they must first be proved to be well-founded on some domain. See well-founded-relation. Roughly put, alternative relations are shown well-founded by providing an order-preserving mapping from their domain into the ordinals. See defun for details on how to specify which well-founded relation is to be used.


a recognizer for the ordinals up to epsilon-0

Using the nonnegative integers and lists we can represent the ordinals up to epsilon-0. The ACL2 notion of ordinal is the same as that found in nqthm-1992 and both are very similar to the development given in ``New Version of the Consistency Proof for Elementary Number Theory'' in The Collected Papers of Gerhard Gentzen, ed. M.E. Szabo, North-Holland Publishing Company, Amsterdam, 1969, pp 132-213.

The following essay is intended to provide intuition about ordinals. The truth, of course, lies simply in the ACL2 definitions of e0-ordinalp and e0-ord-<.

Very intuitively, think of each non-zero natural number as by being denoted by a series of the appropriate number of strokes, i.e.,

0             0
1             |
2             ||
3             |||
4             ||||
...           ...
Then ``omega,'' here written as w, is the ordinal that might be written as
w             |||||...,
i.e., an infinite number of strokes. Addition here is just concatenation. Observe that adding one to the front of w in the picture above produces w again, which gives rise to a standard definition of w: w is the least ordinal such that adding another stroke at the beginning does not change the ordinal.

We denote by w+w or w*2 the ``doubly infinite'' sequence that we might write as follows.

w*2           |||||... |||||... 
One way to think of w*2 is that it is obtained by replacing each stroke in 2 (||) by w. Thus, one can imagine w*3, w*4, etc., which leads ultimately to the idea of ``w*w,'' the ordinal obtained by replacing each stroke in w by w. This is also written as ``omega squared'' or w^2, or:
w             |||||... |||||... |||||... |||||... |||||... ...
We can analogously construct w^3 by replacing each stroke in w by w^2 (which, it turns out, is the same as replacing each stroke in w^2 by w). That is, we can construct w^3 as w copies of w^2,
 3              2       2       2       2
w              w  ...  w  ...  w  ...  w ... ...
Then we can construct w^4 as w copies of w^3, w^5 as w copies of w^4, etc., ultimately suggesting w^w. We can then stack omegas, i.e., (w^w)^w etc. Consider the ``limit'' of all of those stacks, which we might display as follows.
That is epsilon-0.

Below we begin listing some ordinals up to epsilon-0; the reader can fill in the gaps at his or her leisure. We show in the left column the conventional notation, using w as ``omega,'' and in the right column the ACL2 object representing the corresponding ordinal.

  ordinal            ACL2 representation

0 0 1 1 2 2 3 3 ... ... w '(1 . 0) w+1 '(1 . 1) w+2 '(1 . 2) ... ... w*2 '(1 1 . 0) (w*2)+1 '(1 1 . 1) ... ... w*3 '(1 1 1 . 0) (w*3)+1 '(1 1 1 . 1) ... ...

2 w '(2 . 0) ... ...

2 w +w*4+3 '(2 1 1 1 1 . 3) ... ...

3 w '(3 . 0) ... ...

w w '((1 . 0) . 0) ... ...

w 99 w +w +4w+3 '((1 . 0) 99 1 1 1 1 . 3) ... ...

2 w w '((2 . 0) . 0)

... ...

w w w '(((1 . 0) . 0) . 0) ... ...

Observe that the sequence of e0-ordinalps starts with the nonnegative integers. This is convenient because it means that if a term, such as a measure expression for justifying a recursive function (see e0-ord-<) must produce an e0-ordinalp it suffices for it to produce a nonnegative integer.

The ordinals listed above are listed in ascending order. This is the ordering tested by e0-ord-<.

The ``epsilon-0 ordinals'' of ACL2 are recognized by the recursively defined function e0-ordinalp. The base case of the recursion tells us that nonnegative integers are epsilon-0 ordinals. Otherwise, an epsilon-0 ordinal is a cons pair (o1 . o2), where o1 is a non-0 epsilon-0 ordinal, o2 is an epsilon-0 ordinal, and if o2 is not an integer then its car (which, by the foregoing, must be an epsilon-0 ordinal) is no greater than o1. Thus, if you think of a (non-integer) epsilon-0 ordinal as a list, each element is an non-0 epsilon-0 ordinal, the ordinals are listed in weakly descending order, and the final cdr of the list is an integer.

The function e0-ord-< compares two epsilon-0 ordinals, x and y. If both are integers, e0-ord-< is just x<y. If one is an integer and the other is a cons, the integer is the smaller. Otherwise, the ordinals in their cars are compared recursively and determines which is smaller unless the cars are equal, in which case the ordinals in their cdrs are compared.

Fundamental to ACL2 is the fact that e0-ord-< is well-founded on epsilon-0 ordinals. That is, there is no ``infinitely descending chain'' of such ordinals. See proof-of-well-foundedness.


forms that may be embedded in other events

(defun hd (x) (if (consp x) (car x) 0))
(local (defthm lemma23 ...))
(progn (defun fn1 ...)
       (local (defun fn2 ...))

General Form: An embedded event form is a term, x, such that

x is a call of an event function other than DEFPKG (see the documentation for events for a listing of the event functions);

x is of the form (LOCAL x1) where x1 is an embedded event form;

x is of the form (PROGN x1 ... xn), where each xi is an embedded event form;

x is of the form (VALUE &), where & is any term;

x macroexpands to one of the forms above.

An exception: an embedded event form may not set the acl2-defaults-table when in the context of local. Thus for example, the form
(local (table acl2-defaults-table :defun-mode :program))
is not an embedded event form, nor is the form (local (program)), since the latter sets the acl2-defaults-table implicitly. An example at the end of the discussion below illustrates why there is this restriction.

When an embedded event is executed while ld-skip-proofsp is 'include-book, those parts of it inside local forms are ignored. Thus,

   (progn (defun f1 () 1)
          (local (defun f2 () 2))
          (defun f3 () 3))
will define f1, f2, and f3 when ld-skip-proofsp is nil but will define only f1 and f3 when ld-skip-proofsp is 'include-book.


Encapsulate and include-book place restrictions on the kinds of forms that may be processed. These restrictions insure that the non-local events (which will ultimately be processed with ld-skip-proofs t) are indeed admissible provided that the sequence of local and non-local events is admissible when ld-skip-proofs is nil.

Local permits the hiding of an event or group of events in the sense that local events are processed when we are trying to establish the admissibility of a sequence of embedded events but are ignored when we are constructing the world produced by assuming that sequence. Thus, for example, a particularly ugly and inefficient :rewrite rule might be made local to an encapsulate that ``exports'' a desirable theorem whose proof requires the ugly lemma.

To see why we can't allow just anything in as an embedded event, consider allowing the form

(if (ld-skip-proofsp state)
    (defun foo () 2)
    (defun foo () 1))
followed by
(defthm foo-is-1 (equal (foo) 1)).
When we process the events with ld-skip-proofsp, nil the second defun is executed and the defthm succeeds. But when we process the events with ld-skip-proofsp 'include-book, the second defun is executed, so that foo no longer has the same definition it did when we proved foo-is-1. Thus, an invalid formula is assumed when we process the defthm while skipping proofs. Thus, the first form above is not a legal embedded event form.

Defpkg is not allowed because it affects how things are read after it is executed. But all the forms embedded in an event are read before any are executed. That is,

(encapsulate nil
             (defpkg "MY-PKG" nil)
             (defun foo () 'my-pkg::bar))
makes no sense since my-pkg::bar must have been read before the defpkg for "MY-PKG" was executed.

Finally, let us elaborate on the restriction mentioned earlier related to the acl2-defaults-table. Consider the following form.

 (local (program))
 (defun foo (x)
   (if (equal 0 x)
     (1+ (foo (- x))))))
See local-incompatibility for a discussion of how encapsulate processes event forms. Briefly, on the first pass through the events the definition of foo will be accepted in defun mode :program, and hence accepted. But on the second pass the form (local (program)) is skipped because it is marked as local, and hence foo is accepted in defun mode :logic. Yet, no proof has been performed in order to admit foo, and in fact, it is not hard to prove a contradiction from this definition!