Major Section: MISCELLANEOUS
Sometimes an event will announce that it is ``redundant'', meaning that the the form is not evaluated because ACL2 determines that its effect is already incorporated into the logical world. Thus, when this happens, no change to the logical world takes place. This feature permits two independent books, each of which defines some name, to be included sequentially provided they use exactly the same definition.
Note that by the definition above, a form can have no effect on the logical world yet not be considered to be redundant. Here is an example of such a form.
(value-triple (cw "Hello world.~%"))
When are two logical-name definitions considered ``the same''? It depends upon the kind of name being defined. We consider these below in alphabetical order. See also the Notes below.
defabsstobj is redundant if there is already an identical
defabsstobj event in the logical world.
defattach event is never redundant. Note that it doesn't define any
defthm event is redundant if there is already an axiom
or theorem of the given name and both the formula (after
macroexpansion) and the rule-classes are syntactically identical.
Note that a
defaxiom can make a subsequent
defthm redundant, and a
defthm can make a subsequent
defaxiom redundant as well.
defconst is redundant if the name is already defined either with a
defconst event or one that defines it to have the
defdoc event is never redundant because it doesn't define any name.
deflabel event is never redundant. This means that if you have a
deflabel in a book and that book has been included (without error),
then references to that label denote the point in history at which
the book introduced the label. See the note about shifting logical
defmacro event is redundant if there is already a macro defined with
the same name and syntactically identical arguments, guard, and body.
defpkg event is redundant if a package of the same name with exactly
the same imports has been defined.
defstobj event is redundant if there is already a
with the same name that has exactly the same field
descriptors (see defstobj), in the same order, and with the same
:renaming value if
:renaming is supplied for either event.
defthm event is redundant according to the criterion given above in
the discussion of
deftheory is never redundant. The ``natural'' notion of
deftheory forms is that the names and values of the two
theory expressions are the same. But since most theory expressions are
sensitive to the context in which they occur, it seems unlikely to
us that two
deftheorys coming from two sequentially included books
will ever have the same values. So we prohibit redundant theory
definitions. If you try to define the same theory name twice, you
will get a ``name in use'' error.
mutual-recursion event is redundant if
for each function to be introduced, there has already been introduced a
function with the same name, the same formals, and syntactically identical
:measure, type declarations,
body (before macroexpansion), and an appropriate
mode (see the ``Note About Appropriate Modes'' below). Moreover, the
order of the combined
guard and type declarations must be the same
in both cases. Exceptions:
(1) If either definition is declared
:non-executable (see defun-nx),
then the two events must be identical.
(2) It is permissible for one definition to have a
and the other to have no explicit guard (hence, the guard is implicitly
:measure check is avoided if we are skipping proofs (for example,
include-book), and otherwise, the new definition may have a
(:? v1 ... vk), where
(v1 ... vk) enumerates the
variables occurring in the measure stored for the old definition.
(4) If either the old or new event is a
mutual-recursion event, then
redundancy requires that both are
mutual-recursion events that define
the same set of function symbols.
encapsulate event is most commonly redundant when a syntactically
encapsulate has already been executed under the same
default-verify-guards-eagerness. The full criterion for redundancy of
encapsulate events is more complex, for example ignoring contents of
local events; see encapsulate.
in-theory event is never redundant. Note that it doesn't define any
include-book event is redundant if the book has already been
A call of
make-event is never redundant, as its argument is always
evaluated to obtain the make-event expansion. However, that expansion may of
course be redundant.
mutual-recursion event is redundant according to the criteria in the
discussion above for the case of a
progn event is never redundant: its subsidiary events are always
considered. Of course, its sub-events may themselves be redundant. If all
of its sub-events are redundant -- or more generally, if none of the
sub-events changes the logical world -- then the
progn event also
won't change the world.
push-untouchable event is redundant if every name supplied is
already a member of the corresponding list of untouchable symbols.
regenerate-tau-database event is never redundant. Note that it
doesn't define any name.
remove-untouchable event is redundant if no name supplied is
a member of the corresponding list of untouchable symbols.
reset-prehistory event is redundant if it does not cause any change.
set-body event is redundant if the indicated body is already the
table event not define any name. It is redundant when it sets the
value already associated with a key of the table, or when it sets an entire
table (using keyword
:clear) to its existing value; see table.
verify-guards event is redundant if the function has already had
its guards verified.
Note About Built-in (Predefined) Functions and Macros:
Redundancy is restricted for built-in macros and functions that have special
raw Lisp code. Such redundancy is only legal in the context of
This restriction is needed for soundness, for technical reasons omitted here
(details may be found in a long comment about redundant-events in source
Note About Appropriate Modes:
Suppose a function is being redefined and that the formals, guards, types,
stobjs, and bodies are identical. When are the modes (
logic) ``appropriate?'' Identical modes are appropriate.
But what if the old mode was
:program and the new mode is
This is appropriate, provided the definition meets the requirements of the
logical definitional principle. That is, you may redefine ``redundantly''
:program mode function as a
:logic mode function provide the
measure conjectures can be proved. This is what
does. Now consider the reverse style of redefinition. Suppose the
function was defined in
:logic mode and is being identically redefined
:program mode. ACL2 will treat the redefinition as redundant,
provided the appropriate criteria are met (as though it were in :logic
Note About Shifting Logical Names:
Suppose a book defines a function
fn and later uses
fn as a logical
name in a theory expression. Consider the value of that theory
expression in two different sessions. In session A, the book is
included in a world in which
fn is not already defined, i.e., in a
world in which the book's definition of
fn is not redundant. In
session B, the book is included in a world in which
fn is already
identically defined. In session B, the book's definition of
fn is used as a logical name in a theory
expression, it denotes the point in history at which
introduced. Observe that those points are different in the two
sessions. Hence, it is likely that theory expressions involving
will have different values in session A than in session B.
This may adversely affect the user of your book. For example,
suppose your book creates a theory via
deftheory that is advertised
just to contain the names generated by the book. But suppose you
compute the theory as the very last event in the book using:
(set-difference-theories (universal-theory :here) (universal-theory fn))where
fnis the very first event in the book and happens to be a
defunevent. This expression returns the advertised set if
fnis not already defined when the book is included. But if
fnwere previously (identically) defined, the theory is larger than advertised.
The moral of this is simple: when building books that other people
will use, it is best to describe your theories in terms of logical
names that will not shift around when the books are included. The
best such names are those created by
Note About Unfortunate Redundancies.
Notice that our syntactic criterion for redundancy of
may not allow redefinition to take effect unless there is a syntactic change
in the definition. The following example shows how an attempt to redefine a
function can fail to make any change.
(set-ld-redefinition-action '(:warn . :overwrite) state) (defmacro mac (x) x) (defun foo (x) (mac x)) (defmacro mac (x) (list 'car x)) (set-ld-redefinition-action nil state) (defun foo (x) (mac x)) ; redundant, unfortunately; foo does not change (thm (equal (foo 3) 3)) ; succeeds, showing that redef of foo didn't happenThe call of macro
macwas expanded away before storing the first definition of
foofor the theorem prover. Therefore, the new definition of
macdoes not affect the expansion of
fooby the theorem prover, because the new definition of
One workaround is first to supply a different definition of
before the last definition of
foo above. Then that final definition will
no longer be redundant. However, as a courtesy to users, we strengthen the
redundancy check for function definitions when redefinition is active. If in
the example above we remove the form
(set-ld-redefinition-action nil state), then the problem goes away:
(set-ld-redefinition-action '(:warn . :overwrite) state) (defmacro mac (x) x) (defun foo (x) (mac x)) (defmacro mac (x) (list 'car x)) (defun foo (x) (mac x)) ; no longer redundant (thm (equal (foo 3) 3)) ; fails, as we would like
To summarize: If a
defun form is submitted that meets the usual
redundancy criteria, then it may be considered redundant even if a macro
called in the definition has since been redefined. The analogous problem
applie to constants, i.e., symbols defined by
defconst that occur in
the definition body. However, if redefinition is currently active the
problem goes away: that is, the redundancy check is strengthened to check the
``translated'' body, in which macro calls and constants defined by
defconst are expanded away.
The above discussion for
defun forms applies to
defconst forms as
well. However, for
defmacro forms ACL2 always checks translated
bodies, so such bogus redundancy does not occur.
Here is more complex example illustrating the limits of redefinition, based on one supplied by Grant Passmore.
(defun n3 () 0) (defun n4 () 1) (defun n5 () (> (n3) (n4))) ; body is normalized to nil (thm (equal (n5) nil)) ; succeeds, trivially (set-ld-redefinition-action '(:warn . :overwrite) state) (defun n3 () 2) (thm (equal (n5) nil)) ; still succeeds, sadlyWe may expect the final
thmcall to fail because of the following reasoning:
(> (n3) (n4))=
(> 2 1)=
t. Unfortunatly, the body of
n5was simplified (``normalized'') to
n5was admitted, so the redefinition of
n3is ignored during the final
thmcall. (Such normalization can be avoided; see the brief discussion of
:normalizein the documentation for
defun.) So, given this unfortunate situation, one might expect at this point simply to redefine
n5using the same definition as before, in order to pick up the new definition of
n3. Such ``redefinition'' would, however, be redundant, for the same reason as in the previous example: no syntactic change was made to the definition. Even with redefinition active, there is no change in the body of
n5, even with macros and constants (defined by
defconst) expanded; there are none such! The same workaround applies as before: redefine
n5to be something different, and then redefine
n5again to be as desired.
A related phenomenon can occur for
encapsulate. As explained above, an
encapsulate event is redundant if it is identical to one already in the
database. Consider then the following contrived example.
(defmacro mac (x) x) (encapsulate () (defun foo (x) (mac x))) (set-ld-redefinition-action '(:warn . :overwrite) state) (defmacro mac (x) (list 'car x)) (encapsulate () (defun foo (x) (mac x)))The last
encapsulateevent is redundant because it meets the criterion for redundancy: it is identical to the earlier
encapsulateevent. Even though redefinition is active, and hence ACL2 ``should'' be able to see that the new
foois not truly redundant, nevertheless the criterion for redundancy of
encapsulateallows the new
encapsulateform to be redundant.
A workaround can be to add something trivial to the
(encapsulate () (deflabel try2) ; ``Increment'' to try3 next time, and so on. (defun foo (x) x))