an explanation of why we restrict redefinitions
Major Section:  PROGRAMMING

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 further.

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 does.

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 cases.

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 . :overwrite).

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! It is therefore now prohibited. We illustrate such an unsoundness below. Let foo-thm1.lisp be a book with the following contents.

(in-package "ACL2")
(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 is true.

Now let foo-thm2.lisp be a book with the following contents.

(in-package "ACL2")
(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:

(include-book "foo-thm1")
(include-book "foo-thm2")
(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.