Determines whether a function definition is a logical act

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

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. One restriction is that
every function called by the newly defined one must be in `apply$`.) But the most challenging restriction is that the system must
prove that the recursion in the new definition terminates.

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 `defun`'s `declare`

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
`xargs` keyword. Below we show `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 `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

However, the ACL2 theorem prover knows no axioms about `program` mode does not
imperil the soundness of the system — despite the fact that the
termination argument for

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 `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 `defun`, for example with `=` replaced by `<=`, will succeed, and an axiom about

Technically, `verify-termination` submits a redefinition of the
`program` mode function. This is permitted, even when `ld-redefinition-action` is

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.

- Program
- To set the default defun-mode to
: `program` - Logic
- To set the default defun-mode to
:logic - Defun-mode-lambdas
- :program mode functions in
`lambda`objects