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! (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.
(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.
