Major Section: EVENTS
Example:
(verify-termination fact)
General Forms:
(verify-termination fn dcl ... dcl)
(verify-termination (fn1 dcl ... dcl)
(fn2 dcl ... dcl)
...)
where fn and the fni are function symbols having :program mode
(see defun-mode) and all of the dcls are either declare
forms or documentation strings. The first form above is an
abbreviation for
(verify-termination (fn dcl ... dcl))so we limit our discussion to the second form. Each of the
fni
must be in the same clique of mutually recursively defined
functions, but not every function in the clique need be among the
fni.Verify-termination attempts to establish the admissibility of the
fni. Verify-termination retrieves their definitions, creates modified
definitions using the dcls supplied above, and resubmits these
definitions. You could avoid using verify-termination by typing the new
definitions yourself. So in that sense, verify-termination adds no new
functionality. But if you have prototyped your system in :program
mode and tested it, you can use verify-termination to resubmit your
definitions and change their defun-modes to :logic, addings
hints without having to retype or recopy the code.
The defun command executed by verify-termination is obtained
by retrieving the defun (or mutual-recursion) command that
introduced the clique in question and then possibly modifying each definition
as follows. Consider a function, fn, in the clique. If fn is not
among the fni above, its definition is left unmodified other than to add
(declare (xargs :mode :logic)). Otherwise, fn is some fni and we
modify its definition by inserting into it the corresponding dcls listed
with fni in the arguments to verify-termination, as well as
(declare (xargs :mode :logic)). In addition, we throw out from the old
declarations in fn the :mode specification and anything that is
specified in the new dcls.
For example, suppose that fact was introduced with:
(defun fact (n)
(declare (type integer n)
(xargs :mode :program))
(if (zp n) 1 (* n (fact (1- n))))).
Suppose later we do (verify-termination fact). Then the
following definition is submitted.
(defun fact (n) (declare (type integer n)) (if (zp n) 1 (* n (fact (1- n))))).Observe that this is the same definition as the original one, except the old specification of the
:mode has been deleted so that the
defun-mode now defaults to :logic. Although the termination
proof succeeds, ACL2 also tries to verify the guard, because we have
(implicitly) provided a guard, namely (integerp n), for this
function. (See guard for a general discussion of guards, and
see type-spec for a discussion of how type declarations are
used in guards.) Unfortunately, the guard verification fails,
because the subterm (zp n) requires that n be nonnegative, as
can be seen by invoking :args zp. (For a discussion of termination
issues relating to recursion on the naturals, see zero-test-idioms.)
So we might be tempted to submit the following:
(verify-termination fact (declare (xargs :guard (and (integerp n) (<= 0 n))))).However, this is considered a changing of the guard (from
(integerp n)),
which is illegal. If we instead change the guard in the earlier defun
after undoing that earlier definition with :ubt fact, then
(verify-termination fact) will succeed.Remark on system functions. There may be times when you want to apply
verify-termination (and also, perhaps, verify-guards) to functions
that are predefined in ACL2. It may be necessary in such cases to modify the
system code first. See Part II of
http://www.cs.utexas.edu/users/moore/acl2/open-architecture/ for a
discussion of the process for contributing updates to the system code and
books with such verify-termination or verify-guards
events, perhaps resulting in more system functions being built-in as
guard-verified. To see which built-in functions have already received
such treatment, see community books directory books/system/; or, evaluate
the constant *system-verify-guards-alist*, each of whose entries
associates the name of a community book with a list of functions whose
guard-verification is proved by including that book. See the above URL for
more details.
Note that if fn1 is already in :logic mode, then the
verify-termination call has no effect. It is generally considered to be
redundant, in the sense that it returns without error; but if the fn1 is
a constrained function (i.e., introduced in the signature of an
encapsulate, or by defchoose), then an error occurs. This error
is intended to highlight unintended uses of verify-termination; but if
you do not want to see an error in this case, you can write and use your own
macro in place of verify-termination. The following explanation of the
implementation of verify-termination may help with such a task.
We conclude with a discussion of the use of make-event to implement
verify-termination. This discussion can be skipped; we include it only
for those who want to create variants of verify-termination, or who are
interested in seeing an application of make-event.
Consider the following proof of nil, which succeeded up through
Version_3.4 of ACL2.
(encapsulate
()
(defun foo (x y)
(declare (xargs :mode :program))
(if (or (zp x) (zp y))
(list x y)
(foo (1+ x) (1- y))))
(local (defun foo (x y)
(declare (xargs :measure (acl2-count y)))
(if (or (zp x) (zp y))
(list x y)
(foo (1+ x) (1- y)))))
(verify-termination foo))
(defthm bad-lemma
(zp x)
:hints (("Goal" :induct (foo x 1)))
:rule-classes nil)
How did this work? In the first pass of the encapsulate, the second
defun of foo promoted foo from :program to :logic mode,
with y as the unique measured variable. The following call to
verify-termination was then redundant. However, on the second pass of
the encapsulate, the second (local) definition of foo was
skipped, and the verify-termination event then used the first definition
of foo to guess the measure, based (as with all guesses of measures) on a
purely syntactic criterion. ACL2 incorrectly chose (acl2-count x) as the
measure, installing x as the unique measured variable, which in turn led
to an unsound induction scheme subsequently used to prove nil (lemma
bad-lemma, above)Now, verify-termination is a macro whose calls expand to make-event
calls. So in the first pass above, the verify-termination call generated
a defun event identical to the local defun of foo, which
was correctly identified as redundant. That expansion was recorded, and on
the second pass of the encapsulate, the expansion was recalled and used
in place of the verify-termination call (that is how make-event
works). So instead of a measure being guessed for the verify-termination
call on the second pass, the same measure was used as was used on the first
pass, and a sound induction scheme was stored. The attempt to prove nil
(lemma bad-lemma) then failed.
