Major Section: MISCELLANEOUS
For a list of notes and reports about ACL2, see
http://www.cs.utexas.edu/users/moore/publications/acl2-papers.html.
Below is a list of notes and reports pertaining to ACL2.
Major Section: MISCELLANEOUS
Example: Broken at PROVE. Type :H for Help. >>:QACL2 !>
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.
Major Section: MISCELLANEOUS
When a hypothesis of a conditional rule has the form (case-split hyp)
it is logically equivalent to hyp but has the pragmatic effect of
splitting the main goal into two cases, one in which (the required instance
of) hyp is true and one in which (the required instance of) hyp
is false.
Unlike force, case-split does not delay the ``false case'' to
a forcing round but tackles it more or less immediately.
When in the proof checker, case-split behaves like force.
Major Section: MISCELLANEOUS
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.
Major Section: MISCELLANEOUS
To each goal-spec, str, there corresponds a clause-identifier
produced by (parse-clause-id str). For example,
(parse-clause-id "[2]Subgoal *4.5.6/7.8.9'''")returns
((2 4 5 6) (7 8 9) . 3).
The function string-for-tilde-@-clause-id-phrase inverts
parse-clause-id in the sense that given a clause identifier it
returns the corresponding goal-spec.
As noted in the documentation for goal-spec, each clause
printed in the theorem prover's proof attempt is identified by a
name. When these names are represented as strings they are called
``goal specs.'' Such strings are used to specify where in the proof
attempt a given hint is to be applied. The function
parse-clause-id converts goal-specs into clause identifiers,
which are cons-trees containing natural numbers.
Examples of goal-specs and their corresponding clause identifiers are shown below.
parse-clause-id
-->
"Goal" ((0) NIL . 0)
"Subgoal 3.2.1'" ((0) (3 2 1) . 1)
"[2]Subgoal *4.5.6/7.8.9'''" ((2 4 5 6) (7 8 9) . 3)
<--
string-for-tilde-@-clause-id-phrase
The caar of a clause id specifies the forcing round, the cdar specifies the goal being proved by induction, the cadr specifies the particular subgoal, and the cddr is the number of primes in that subgoal.
Internally, the system maintains clause ids, not goal-specs. The
system prints clause ids in the form shown by goal-specs. When a
goal-spec is used in a hint, it is parsed (before the proof attempt
begins) into a clause id. During the proof attempt, the system
watches for the clause id and uses the corresponding hint when the
id arises. (Because of the expense of creating and garbage
collecting a lot of strings, this design is more efficient than the
alternative.)
Major Section: MISCELLANEOUS
...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)The first two forms are examples of commands that are in fact primitive events. See events.
defrec, on the other hand, is a
macro that expands into a progn of several primitive events. In
general, a world extending command generates one or more events.
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.
Major Section: MISCELLANEOUS
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.
Major Section: MISCELLANEOUS
General Form of :hints: (hint1 hint2 ... hintk)Each element, hinti, must be either a common hint or a computed hint.
A common hint is of the form
(goal-spec :key1 val1 ... :keyn valn)
where goal-spec is as specified in goal-spec and each
:keyi and vali is as specified in hints.
A computed hint is either a function symbol, fn, of three
arguments or is a term involving, at most, the three free variables
ID, CLAUSE and WORLD. The function symbol case is treated
as an abbreviation of the term (fn ID CLAUSE WORLD). (Note that
this tells you which argument is which.) In the discussion below we
assume all computed hints are of the term form.
The evaluation of the term (in a context in which its variables are
bound as described below) should be either nil, indicating that
the hint is not applicable to the clause in question, or else the
value is an alternating list of :keyi vali ``pairs'' as
specified in hints. The first applicable hint, if any, is used
and deleted from the list of hints available to the descendants of
the clause (see below).
The evaluation of a hint term is done with guard checking turned off
(see set-guard-checking); e.g., the form (car 23) in a
computed hint returns nil as per the axioms.
When a non-nil value is returned it is treated just as though it
had been typed as part of the original input. That is, your job as
the programmer of computed hints is to generate the form you would
have typed had you supplied a common hint at that point. (In
particular, any theory expressions in it are evaluated with respect
to the global current-theory, not whatever theory is active on the
subgoal in question.) If the generated list of keywords and values
is illegal, an error will be signaled and the proof attempt will be
aborted.
It remains only to describe the bindings of the three variables.
Suppose the theorem prover is working on some clause, clause, named
by some goal-spec, e.g., "Subgoal *1/2'''" in some logical
world, world. Corresponding to the printed goal-spec is an
internal data structure called a ``clause identifier'' id.
See clause-identifier.
In the case of a common hint, the hint applies if the goal-spec of the hint is the same as the goal-spec of the clause in question.
In the case of a computed hint, the variable ID is bound to the
clause id, the variable CLAUSE is bound to the (translated form
of the) clause, and the variable WORLD is bound to the current
ACL2 world.
When a computed hint applies, it is removed from the list of hints
available to the children of the clause to which it applied. This
prevents it from being reapplied (often infinitely). The goals
produced by induction and the top-level goals of forcing rounds are
not considered children; all original hints are available to them.
Insert n copies of a computed hint into the :hints to allow the
hint to be used ``repeatedly'' at n different levels.
For some instruction about how to use computed hints,
see using-computed-hints.
encapsulate events
Major Section: MISCELLANEOUS
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))We would like to imagine moving the definition of(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))) )
before1 to just
in front of this encapsulate, as follows.
(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)))
)
Thus, we will only assign the constraint (consp (sig-fn x)), from
the theorem sig-fn-prop, to the function sig-fn, not to the
function before1.
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))We can see that there is really no harm in imagining that we move the definition of(local (defun sig-fn (x) (cons x x)))
(defthm sig-fn-prop (consp (sig-fn x)))
(defun after1 (x) (sig-fn x)) )
after1 out of the encapsulate, to just after
the encapsulate.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))Only the functions(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 and during receive extra
constraints. The functions before1 and before2 are viewed as
moving in front of the encapsulate, as is the theorem
before2-prop. The functions after1 and after2 are viewed
as being moved past the encapsulate. Notice that the formula
(consp (during x)) is a conjunct of the constraint. It comes
from the :type-prescription rule deduced during the definition
of the function during. The implementation reports the following.
(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))Under the simple approach we have in mind,(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))))))))
bar is constrained to
satisfy both its definition and bar-prop because bar mentions
a function declared in the signatures of the encapsulation. In
fact, bar is so-constrained in the ACL2 semantics of
encapsulation and the first two events above (the encapsulate and
the consequence that foo must be the identity function) are
actually admissible. But under the simple approach to assigning
constraints, foo is unconstrained because no theorem about it is
exported. Under that approach, ouch! is proveable because foo
can be instantiated in foo-id to a function other than the
identity function.
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))))))))
Major Section: MISCELLANEOUS
ACL2 Version 2.3 -- A Computational Logic for Applicative Common Lisp Copyright (C) 1998 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: Kaufmann@aus.edsr.eds.com and Moore@cs.utexas.edu Department of Computer Sciences University of Texas at Austin Austin, TX 78712-1188 U.S.A.
Please also see acknowledgements.
Major Section: MISCELLANEOUS
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.
Major Section: MISCELLANEOUS
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.