Verify-termination
Convert a function from :program mode to :logic mode
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,
adding 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.
It may be necessary to specify an appropriate :ruler-extenders in a
dcl supplied to verify-termination. This determines the rulers used in the termination proofs and also the case analysis in the
induction scheme suggested by the admitted function. See induction-coarse-v-fine-grained.
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 verify-guards-for-system-functions
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*, which specifies 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.
Subtopics
- Verify-guards-for-system-functions
- Arranging that source functions come up as guard-verified
- ACL2-pc::prove-termination
- (macro)
Prove termination efficiently by using a previous termination theorem.
- Verify-termination-on-raw-program-okp
- Permit verify-termination for functions with raw Lisp code.
