Major Section: MISCELLANEOUS
Two ``defun-modes'' are supported, :
program
and :
logic
. Roughly
speaking, :
program
mode allows you to prototype a function for
execution without any proof burdens, while :
logic
mode allows you to
add a new definitional axiom to the logic. The system comes up in
:
logic
mode. Execution of functions whose defun-mode is :
program
may render ACL2 unsound! See defun-mode-caveat.
Note that calls of local
and of many events are skipped in
:program
mode; see program.
When you define a function in the ACL2 logic, that function can be run on concrete data. But it is also possible to reason deductively about the function because each definition extends the underlying logic with a definitional axiom. To ensure that the logic is sound after the addition of this axiom, certain restrictions have to be met, namely that the recursion terminates. This can be quite challenging.
Because ACL2 is a programming language, you often may wish simply to program in ACL2. For example, you may wish to define your system and test it, without any logical burden. Or, you may wish to define ``utility'' functions -- functions that are executed to help manage the task of building your system but functions whose logical properties are of no immediate concern. Such functions might be used to generate test data or help interpret the results of tests. They might create files or explore the ACL2 database. The termination arguments for such functions are an unnecessary burden provided no axioms about the functions are ever used in deductions.
Thus, ACL2 introduces the idea of the ``defun-mode'' of a function.
The :mode
keyword of defun
's declare
xarg
allows you to
specify the defun-mode of a given definition. If no :mode
keyword is supplied, the default defun-mode is used;
see default-defun-mode.
There are two defun-modes, each of which is written as a keyword:
:
program
-- logically undefined but executable outside deductive
contexts.
:
logic
-- axiomatically defined as per the ACL2 definitional
principle.
It is possible to change the defun-mode of a function from :
program
to :
logic
. We discuss this below.
We think of functions having :
program
mode as ``dangerous''
functions, while functions having :
logic
mode are ``safe.'' The
only requirement enforced on :
program
mode functions is the
syntactic one: each definition must be well-formed ACL2. Naively
speaking, if a :
program
mode function fails to terminate then no
harm is done because no axiom is added (so inconsistency is avoided)
and some invocations of the function may simply never return. This
simplistic justification of :
program
mode execution is faulty
because it ignores the damage that might be caused by
``mis-guarded'' functions. See defun-mode-caveat.
We therefore implicitly describe an imagined implementation of defun-modes that is safe and, we think, effective. But please see defun-mode-caveat.
The default defun-mode is :
logic
. This means that when you defun
a
function the system will try to prove termination. If you wish to
introduce a function of a different defun-mode use the :mode
xargs
keyword. Below we show fact
introduced as a function in :
program
mode.
(defun fact (n) (declare (xargs :mode :program)) (if (or (not (integerp n)) (= n 0)) 1 (* n (fact (1- n)))))No axiom is added to the logic as a result of this definition. By introducing
fact
in :
program
mode we avoid the burden of a
termination proof, while still having the option of executing the
function. For example, you can type
ACL2 !>(fact 3)and get the answer
6
. If you type (fact -1)
you will get a hard
lisp error due to ``infinite recursion.''However, the ACL2 theorem prover knows no axioms about fact
. In
particular, if the term (fact 3)
arises in a proof, the theorem
prover is unable to deduce that it is 6
. From the perspective of
the theorem prover it is as though fact
were an undefined
function symbol of arity 1
. Thus, modulo certain important
issues (see defun-mode-caveat), the introduction of this
function in :
program
mode does not imperil the soundness of the
system -- despite the fact that the termination argument for fact
was omitted -- because nothing of interest can be proved about
fact
. Indeed, we do not allow fact
to be used in logical
contexts such as conjectures submitted for proof.
It is possible to convert a function from :
program
mode to
:
logic
mode at the cost of proving that it is admissible. This can
be done by invoking
(verify-termination fact)which is equivalent to submitting the
defun
of fact
, again, but
in :
logic
mode.
(defun fact (n) (declare (xargs :mode :logic)) (if (or (not (integerp n)) (= n 0)) 1 (* n (fact (1- n)))))This particular event will fail because the termination argument requires that
n
be nonnegative. A repaired defun
, for example with =
replaced by <=
, will succeed, and an axiom about fact
will
henceforth be available.Technically, verify-termination
submits a redefinition of the
:
program
mode function. This is permitted, even when
ld-redefinition-action
is nil
, because the new definition is
identical to the old (except for its :mode
and, possibly, other
non-logical properties).
See guard for a discussion of how to restrict the execution of
functions. Guards may be ``verified'' for functions in :
logic
mode; see verify-guards.