An explanation of why we restrict redefinitions
ACL2 does not in general allow the redefinition of functions
because logical inconsistency can result: previously stored theorems can be
rendered invalid if the axioms defining the functions involved are changed.
However, to permit prototyping of both :program and :logic mode systems, ACL2 permits redefinition if the user has accepted
logical responsibility for the consequences by setting ld-redefinition-action to an appropriate non-nil value. The refusal of
ACL2 to support the unrestricted redefinition of :program mode
functions may appear somewhat capricious. After all, what are the logical
consequences of changing a definition if no axioms are involved?
Three important points should be made before we discuss redefinition
The first is that ACL2 does support redefinition (of both :program and :logic functions) when ld-redefinition-action is non-nil.
The second is that a ``redefinition'' that does not change the mode,
formals, guards, type declarations, stobjs, or body of a function is
considered redundant and is permitted even when ld-redefinition-action
is nil. We recognize and permit redundant definitions because it is not
uncommon for two distinct books to share identical function
definitions. When determining whether the body of a function is changed by a
proposed redefinition, we actually compare the untranslated versions of the
two bodies. See term. For example, redundancy is not recognized if
the old body is (list a b) and the new body is (cons a (cons b
nil)). We use the untranslated bodies because of the difficulty of
translating the new body in the presence of the old syntactic information,
given the possibility that the redefinition might attempt to change the signature of the function, i.e., the number of formals, the number of
results, or the position of single-threaded objects in either.
The third important point is that a ``redefinition'' that preserves the
formals, guard, types, stobjs, and body but changes the mode from :program to :logic is permitted even when ld-redefinition-action is nil. That is what verify-termination
This note addresses the temptation to allow redefinition of :program functions in situations other than the three described above.
Therefore, suppose ld-redefinition-action is nil and consider the
Case 1. Suppose the new definition attempts to change the formals or more
generally the signature of the function. Accepting such a redefinition
would render ill-formed other :program functions which call the
redefined function. Subsequent attempts to evaluate those callers could
arbitrarily damage the Common Lisp image. Thus, redefinition of :program functions under these circumstances requires the user's active
approval, as would be sought with ld-redefinition-action '(:query
Case 2. Suppose the new definition attempts to change the body (even
though it preserves the signature). At one time we believed this was
acceptable and ACL2 supported the quiet redefinition of :program
mode functions in this circumstance. However, because such functions can be
used in macros and redundancy checking is based on untranslated bodies, this
turns out to be unsound! (Aside: Perhaps this is not an issue if the function
takes state or a user-defined stobj argument; but we do not
further consider this distinction.) Such redefinition is therefore now
prohibited. We illustrate such an unsoundness below. Let foo-thm1.lisp
be a book with the following contents.
(defun p1 (x) (declare (xargs :mode :program)) (list 'if x 't 'nil))
(defmacro p (x) (p1 x))
(defun foo (x) (p x))
(defthm foo-thm1 (iff (foo x) x) :rule-classes nil)
Note that the macro form (p x) translates to (if x t nil). The
:program function p1 is used to generate this translation.
The function foo is defined so that (foo x) is (p x) and a
theorem about foo is proved, namely, that (foo x) is true iff x
Now let foo-thm2.lisp be a book with the following contents.
(defun p1 (x) (declare (xargs :mode :program)) (list 'if x 'nil 't))
(defmacro p (x) (p1 x))
(defun foo (x) (p x))
(defthm foo-thm2 (iff (foo x) (not x)) :rule-classes nil)
In this book, the :program function p1 is defined so that
(p x) means just the negation of what it meant in the first book, namely,
(if x nil t). The function foo is defined identically — more
precisely, the untranslated body of foo is identical in the two
books, but because of the difference between the two versions of the
:program function p1 the axioms defining the two foos
are different. In the second book we prove the theorem that (foo x) is
true iff x is nil.
Now consider what would happen if the signature-preserving
redefinition of :program functions were permitted and these two
books were included. When the second book is included the redefinition
of p1 would be permitted since the signature is preserved and
p1 is just a :program. But then when the redefinition of
foo is processed it would be considered redundant and thus be permitted.
The result would be a logic in which it was possible to prove that (foo
x) is equivalent to both x and (not x). In particular, the
following sequence leads to a proof of nil:
(thm nil :hints (("Goal" :use (foo-thm1 foo-thm2))))
It might be possible to loosen the restrictions on the redefinition of
:program functions by allowing signature-preserving
redefinition of :program functions not involved in macro
definitions. Alternatively, we could implement definition redundancy checking
based on the translated bodies of functions (though that is quite
problematic). Barring those two changes, we believe it is necessary simply to
impose the same restrictions on the redefinition of :program mode
functions as we do on :logic mode functions.