Defexec
Attach a terminating executable function to a definition
Suppose you define a function (fn x) with a guard of
(good-input-p x), and you know that when the guard holds, the measure
decreases on each recursive call. Unfortunately, the definitional principle
(see defun) ignores the guard. For example, if the definition has the
form
(defun fn (x)
(declare (xargs :guard (good-input-p x)))
(if (not-done-yet x)
(... (fn (destr x)) ...)
...))
then in order to admit this definition, ACL2 must prove the appropriate
formula asserting that (destr x) is ``smaller than'' x under the
assumption (not-done-yet x) but without the assumption (good-input-p
x), even if (not-done-yet x) is true. In essence, it may be necessary
to submit instead the following definition.
(defun fn (x)
(declare (xargs :guard (good-input-p x)))
(if (good-input-p x)
(if (not-done-yet x)
(... (fn (destr x)) ...)
...)
nil)
But it is unfortunate that when calls of fn are evaluated, for example
when fn is applied to an explicit constant during a proof, then a call of
good-input-p must now be evaluated on each recursive call.
Fortunately, defexec provides a way to keep the execution efficient.
For the example above we could use the following form.
(defexec fn (x)
(declare (xargs :guard (good-input-p x)))
(mbe :logic (if (good-input-p x)
(if (not-done-yet x)
(... (fn (destr x)) ...)
...)
nil)
:exec (if (not-done-yet x)
(... (fn (destr x)) ...)
...)))
Here ``mbe'' stands for ``must be equal'' and, roughly speaking,
its call above is logically equal to the :logic form but is evaluated
using the :exec form when the guard holds. See mbe. The effect
is thus to define fn as shown in the defun form above, but to
cause execution of fn using the :exec body. The use of defexec
instead of defun in the example above causes a termination proof to be
performed, in order to guarantee that evaluation always theoretically
terminates, even when using the :exec form for evaluation.
Example:
; Some of the keyword arguments in the declarations below are irrelevant or
; unnecessary, but they serve to illustrate their use.
(defexec f (x)
(declare (xargs :measure (+ 15 (acl2-count x))
:ruler-extenders :basic
:hints (("Goal" :in-theory (disable nth)))
:guard-hints (("Goal" :in-theory (disable last)))
:guard (and (integerp x) (<= 0 x) (< x 25)))
(exec-xargs
:test (and (integerp x) (<= 0 x))
:default-value 'undef ; defaults to nil
:measure (nfix x)
:ruler-extenders :basic
:well-founded-relation o<))
(mbe :logic (if (zp x)
1
(* x (f (- x 1))))
:exec (if (= x 0)
1
(* x (f (- x 1))))))
The above example macroexpands to the following.
(ENCAPSULATE ()
(LOCAL
(ENCAPSULATE ()
(SET-IGNORE-OK T)
(SET-IRRELEVANT-FORMALS-OK T)
(LOCAL (DEFUN F (X)
(DECLARE
(XARGS :VERIFY-GUARDS NIL
:HINTS (("Goal" :IN-THEORY (DISABLE NTH)))
:MEASURE (NFIX X)
:RULER-EXTENDERS :BASIC
:WELL-FOUNDED-RELATION O<))
(IF (AND (INTEGERP X) (<= 0 X))
(IF (= X 0) 1 (* X (F (- X 1))))
'UNDEF)))
(LOCAL (DEFTHM F-GUARD-IMPLIES-TEST
(IMPLIES (AND (INTEGERP X) (<= 0 X) (< X 25))
(AND (INTEGERP X) (<= 0 X)))
:RULE-CLASSES NIL))))
(DEFUN F (X)
(DECLARE (XARGS :MEASURE (+ 15 (ACL2-COUNT X))
:RULER-EXTENDERS :BASIC
:HINTS (("Goal" :IN-THEORY (DISABLE NTH)))
:GUARD-HINTS (("Goal" :IN-THEORY (DISABLE LAST)))
:GUARD (AND (INTEGERP X) (<= 0 X) (< X 25))))
(MBE :LOGIC
(IF (ZP X) 1 (* X (F (- X 1))))
:EXEC
(IF (= X 0) 1 (* X (F (- X 1)))))))
Notice that in the example above, the :hints in the local definition of F are inherited from the :hints in the xargs of the defexec form. We discuss such inheritance below.
CAVEAT: Termination is not considered for calls of mbe under the
top-level call. Moreover, the :exec part of an mbe call under
the :logic part of any superior mbe call is completely ignored.
General Form:
(defexec fn (var1 ... varn) doc-string dcl ... dcl
(mbe :LOGIC logic-body
:EXEC exec-body))
where the syntax is identical to the syntax of defun where the body
is a call of mbe, with the exceptions described below. Thus, fn is
the symbol you wish to define and is a new symbolic name and (var1
... varn) is its list of formal parameters (see name). The first
exception is that at least one dcl (i.e., declare form) must
specify a :guard, guard. The second exception is that one of the
dcls is allowed to contain an element of the form (exec-xargs ...).
The exec-xargs form, if present, must specify a non-empty keyword-value-listp each of whose keys is one of :test,
:default-value, or one of the standard xargs keys of
:measure, :ruler-extenders, :well-founded-relation, :hints
:stobjs, or :dfs. Any of these standard xargs keys that is
present in an xargs of some dcl but is not specified in the
(possibly nonexistent) exec-xargs form is considered to be specified in
the exec-xargs form, as illustrated in the example above for :hints.
(So for example, if you want :hints in the final, non-local definition
but not in the local definition, then specify the :hints in the
xargs but specify :hints nil in the exec-xargs.) If :test
is specified and not nil, let test be its value; otherwise let
test default to guard. If :default-value is specified, let
default-value be its value; else default-value is nil.
Default-value should have the same signature as exec-body;
otherwise the defexec form will fail to be admitted.
The above General Form's macroexpansion is of the form (PROGN encap
final-def), where encap and final-def are as follows.
Final-def is simply the result of removing the exec-xargs
declaration (if any) from its declare form, and is the result of
evaluating the given defexec form, since encap is of the following
form.
; encap
(ENCAPSULATE ()
(set-ignore-ok t) ; harmless for proving termination
(set-irrelevant-formals-ok t) ; harmless for proving termination
(local local-def)
(local local-thm))
The purpose of encap is to ensure that the executable version of
name terminates on all arguments. Thus, local-def and
local-thm are as follows, where the xargs of the declare
form are the result of adding :VERIFY-GUARDS NIL to the result of
removing the :test and (optional) :default-value from the
exec-xargs.
; local-def
(DEFUN fn formals
(DECLARE (XARGS :VERIFY-GUARDS NIL ...))
(IF test
exec-body
default-value))
; local-thm
(DEFTHM fn-EXEC-GUARD-HOLDS
(IMPLIES guard test)
:RULE-CLASSES NIL)
We claim that if the above local-def and local-thm are admitted,
then all evaluations of calls of fn terminate. The concern is that the
use of mbe in final-def allows for the use of exec-body for
a call of fn, as well as for subsequent recursive calls, when guard
holds and assuming that the guards have been verified for final-def.
However, by local-thm we can conclude in this case that test holds,
in which case the call of fn may be viewed as a call of the version of
fn defined in local-def. Moreover, since guards have been verified
for final-def, then guards hold for subsequent evaluation of
exec-body, and in particular for recursive calls of fn, which can
thus continue to be viewed as calls using local=def.
