REDUNDANT-EVENTS

allowing a name to be introduced ``twice'' 
Major Section:  MISCELLANEOUS

Sometimes an event will announce that it is ``redundant''. When this happens, no change to the logical world has occurred. This happens when the logical name being defined is already defined and has exactly the same definition, from the logical point of view. This feature permits two independent books, each of which defines some name, to be included sequentially provided they use exactly the same definition.

When are two logical-name definitions considered exactly the same? It depends upon the kind of name being defined.

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 defun or mutual-recursion (or defuns) 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 :guard, :measure, type declarations, stobjs declarations and body (before macroexpansion), and an appropriate mode (see the discussion of ``appropriate modes'' below). Exceptions: (1) If either definition is declared :non-executable (see xargs), then the two events must be identical. (2) 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). (3) The :measure check is avoided if we are skipping proofs (for example, during include-book), and 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.

A verify-guards event is redundant if the function has already had its guards verified.

A defaxiom or 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.

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 defstobj is redundant if there is already a defstobj event 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.

A defmacro is redundant if there is already a macro defined with the same name and syntactically identical arguments, guard, and body.

A defpkg is redundant if a package of the same name with exactly the same imports has been defined.

A deftheory is never redundant. The ``natural'' notion of equivalent 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.

An in-theory event is never redundant because it doesn't define any name.

A push-untouchable event is redundant if every name supplied is already a member of the corresponding list of untouchable symbols.

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.

Table and defdoc events are never redundant because they don't define any name.

An encapsulate event is redundant if and only if a syntactically identical encapsulate has already been executed under the same default-defun-mode.

An include-book is redundant if the book has already been included.

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 (: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. This is inappropriate. We do not permit the downgrading of a function from :logic mode to :program mode, since that might produce a logical world in which there were theorems about a :program mode function, violating one of ACL2's basic assumptions.

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 does 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))
(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 when the first definition of foo was processed, so the new definition of mac is not seen in foo unless foo is redefined; yet our attempt at redefinition failed! An easy 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.

The phenomenon illustrated above can occur even without macros. Here is a more complex example, 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)
If now we execute (thm (equal (n5) nil)), it still succeeds even though we expect (n5) = (> (n3) (n4)) = (> 2 1) = t. That is because the body of n5 was normalized to nil. (Such normalization can be avoided; see the brief discussion of :normalize in the documentation for defun.) 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. 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. Consider then the following contrived example. 

(encapsulate () (defun foo (x) x))
(set-ld-redefinition-action '(:warn . :overwrite) state)
(defun foo (x) (cons x x))
(encapsulate () (defun foo (x) x)) ; redundant!
The last encapsulate event is redundant because it meets the criterion for redundancy: it is identical to the earlier encapsulate event. 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))

The examples above are suggestive but by no means exhaustive. Consider the following example. 

(defstub f1 () => *)
(set-ld-redefinition-action '(:warn . :overwrite) state)
(defun f1 () 3)
(defstub f1 () => *) ; redundant -- has no effect
The reason that the final defstub is redundant is that defstub is a macro that expands to a call of encapsulate; so this is very similar to the immediately preceding example.