Redundant-events
Allowing a name to be introduced ``twice''
Sometimes an event will announce that it is ``redundant'', meaning
that 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 event that introduces that name. We consider these
below in alphabetical order, followed by ``Note About'' comments. Macros in
the community-books may also support redundancy; see their
documentation for details, since below we only discuss ACL2 events that
are built into ACL2.
A defstobj or defabsstobj is redundant if there is already
an identical such event in the logical world.
A defattach event is never redundant. (Reasons are provided in a
comment in the ACL2 sources definition of defattach in the ACL2 logic.) Note
that defattach events do not define any names.
A defaxiom or defthm event is redundant if there is already
an axiom or theorem of the given name and the two events are
syntactically identical. But there is the following more generous criterion:
both the formula (after macroexpansion) and the rule-classes (after
translation and certain ``truncation'') are syntactically identical. This
``truncation'' involves removing the :HINTS and :INSTRUCTIONS fields
from a rule-class, and also removing the :COROLLARY field when it
specifies the same term as the event. Note that a defaxiom can be
redundant with a defthm and vice-versa. (Remark for system hackers:
defthm/defaxiom redundancy is implemented in ACL2 source function,
redundant-theoremp.)
A defconst is redundant if the name is already defined either with
a syntactically identical defconst event or one that defines it to have
the same value.
A 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 names,
below.
A defmacro event is redundant if there is already a macro defined
with the same name and syntactically identical arguments, guard, and
body.
A defpkg event is redundant if a package of the same name with
exactly the same imports has been defined.
A defthm event is redundant according to the criteria given above
in the discussion of defaxiom.
A deftheory event is redundant if keyword argument
:redundant-okp is not nil and the theory is unchanged from the one
already associated with the name. More precisely, the runic theory computed
from the theory expression must be equal to the runic theory already
associated with the name. (See theories for a discussion of runic
theories. Also see defthy for a variant of deftheory that
supports redundancy by default.) Equality of runic theories is a rather
severe restriction, since most theory expressions are sensitive to the context
in which they occur. Consider the following example.
(deftheory foo (disable append revappend) :redundant-okp t)
(defthm my-car-cons (equal (car (cons x y)) x))
(deftheory foo (disable revappend append) :redundant-okp t)
The second deftheory event above is not redundant, because its
computed runic theory includes the rune (:rewrite my-car-cons),
which is not in the runic theory previously associated with foo. If we
change the example either to eliminate the defthm above or to change
it to call defthmd instead, then the second deftheory event is
redundant, because the runic theories are ordered, and hence the order of
runic designators (here, revappend and append) is irrelevant.
A defun, defuns, or mutual-recursion event is
redundant if for each function to be introduced, there has already been
introduced a function with the same name, formals, and body (before
macroexpansion), and with the same values declared for the :guard, :measure, types, :ruler-extenders,
:non-executable, :type-prescription, :stobjs, and
:split-types, provided that the defun-modes are
appropriate (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 and clarifications:
- If the new and existing function events have no explicit ruler-extenders (which are therefore syntactically equal), the default-ruler-extenders for the new and existing function events must be the
same.
- It is permissible for one definition to have a :guard of
t and the other to have no explicit guard (hence, the guard is implicitly
t).
- The :measure check is avoided if the old definition is non-recursive
(and not defined within a mutual-recursion) or we are skipping proofs
(for example, during include-book). Otherwise, the new definition may
have a :measure of (:? v1 ... vk), where (v1 ... vk) enumerates
the variables occurring in the measure stored for the old definition.
- 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.
- The stobjs declared by the two definitions are allowed to disagree
on state: one can declare state among its declared :stobjs
values while the other does not, regardless of whether or not set-state-ok has been evaluated. That is, they only need to agree on the
user-defined stobjs.
- Redundancy may fail with an error about a name being “already
defined using special raw Lisp code” or “predefined in the
"COMMON-LISP" package”. This applies to certain functions that are
built into ACL2; it may also apply when definitions are overridden in raw Lisp
using trust tags (see defttag), typically in books. The reason for
causing an error is that if the proposed redundant definition is in a book,
then when later including that book after it is certified, the compiled code
for that definition will replace the original code, which is generally
undesirable when the original code has special raw Lisp optimizations. If the
earlier definition is in a book, then the error message will suggest including
that book rather than trying to define the function redundantly.
An encapsulate event is most commonly redundant when a
syntactically identical encapsulate has already been executed under
the same default-defun-mode, default-ruler-extenders, and
default-verify-guards-eagerness. The full criterion for redundancy of
encapsulate events is more complex, for example ignoring contents of
local events; see redundant-encapsulate.
An in-theory event is never redundant by default, though that can
be changed; see set-in-theory-redundant-okp. Note that it doesn't
define any name.
An include-book event is redundant if the book has already been
included.
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.
A mutual-recursion event is redundant according to the criteria in
the discussion above for the case of a defun event.
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.
A push-untouchable event is redundant if every name supplied is
already a member of the corresponding list of untouchable symbols.
A regenerate-tau-database event is never redundant. Note that it
doesn't define any name.
A remove-untouchable event is redundant if no name supplied is a
member of the corresponding list of untouchable symbols.
A reset-prehistory event is redundant if it does not cause any
change.
A set-body event is redundant if the indicated body is already the
current body.
A 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. Setting a non-existent key to nil is not redundant, with the
exception discussed next.
Memoization is carried out using a table,
memoize-table, that may associate a function symbol with nil when it
is not memoized. It is redundant to unmemoize a currently-unmemoized
function symbol, thus associating it with nil in the memoize-table
— even if that function symbol is not already a key of that table (this
is the exception noted in the preceding paragraph). It is redundant to memoize a function when the function is already identically memoized, that
is, when the corresponding table event is redundant.
A 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 local. This restriction is needed for soundness, for technical reasons
omitted here (details may be found in a long comment about redundant-events in
source function chk-acceptable-defuns-redundancy).
Note About Appropriate Modes:
Suppose a function is being redefined and that the formals, guards, types,
user-defined stobjs, and bodies are identical. When are the
modes (:program or :logic) ``appropriate?''
Identical modes are appropriate. But what if the old mode was :program
and the new mode is :logic? This is appropriate, provided the definition
meets the requirements of the logical definitional principle. That is, you
may redefine ``redundantly'' a :program mode function as a :logic
mode function provide the measure conjectures can be proved. This is what
verify-termination does. Now consider the reverse style of
redefinition. Suppose the function was defined in :logic mode and is
being identically redefined in :program mode. ACL2 will treat the
redefinition as redundant, provided the appropriate criteria are met (as
though it were in :logic mode).
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 redundant. When
fn is used as a logical name in a theory expression, it denotes the point
in history at which fn was introduced. Observe that those points
are different in the two sessions. Hence, it is likely that theory
expressions involving fn 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 fn is the very first event in the book and happens to be a
defun event. This expression returns the advertised set if fn is
not already defined when the book is included. But if fn were 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 deflabel.
Note About Unfortunate Redundancies.
Notice that our syntactic criterion for redundancy of defun events 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 happen
The call of macro mac was expanded away before storing the first
definition of foo for the theorem prover. Therefore, the new definition
of mac does not affect the expansion of foo by the theorem prover,
because the new definition of foo is ignored.
One workaround is first to supply a different definition of foo, just
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
applies 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 see 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, sadly
We may expect the final thm call to fail because of the following
reasoning: (n5) = (> (n3) (n4)) = (> 2 1) = t.
Unfortunately, the body of n5 was simplified to nil when n5 was
admitted (see normalize), so the redefinition of n3 is ignored
during the final thm call. (Such normalization can be avoided; see xargs for discussion of the :normalize keyword.) So, given this
unfortunate situation, one might expect at this point simply to redefine
n5 using 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 n5 to be something different, and then redefine n5 again 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. (But a weaker condition applies in general; see
redundant-encapsulate.) 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 encapsulate event is redundant because it meets the criterion
for redundancy: it is identical to the earlier encapsulate event. Even
though redefinition is active, and hence ACL2 ``should'' be able to see that
the new defun of foo is not truly redundant, nevertheless the
criterion for redundancy of encapsulate allows the new
encapsulate form to be redundant.
A workaround can be to add something trivial to the encapsulate, for
example:
(encapsulate ()
(deflabel try2) ; ``Increment'' to try3 next time, and so on.
(defun foo (x) x))
Subtopics
- Set-enforce-redundancy
- Require most events to be redundant
- Set-in-theory-redundant-okp
- Allow in-theory events to be redundant
- Get-guard-checking
- Get the status most recently installed by set-guard-checking
- Get-enforce-redundancy
- Query the world on whether redundancy is being enforced
