Introduce an arbitrarily recursive function.

Given a recursive program-mode function that only calls logic-mode functions (besides calling itself) and that may not terminate, it is possible (under some conditions) to construct a logic-mode ``version'' of that function by explicitly testing for termination, via a non-executable predicate. The resulting logic-mode function is ``equivalent'' to the program-mode function when the latter terminates.

The resulting logic-mode function can be subjected to
formal verification and transformation. In particular, if it can be proved that
the termination test holds on every argument value,
then the termination test can be transformed away
(e.g. via a simplification transformation),
obtaining a simpler, provably equivalent logic-mode function,
which may be executable
if the initial program-mode function was executable.
If termination can be proved only on some argument values instead,
the domain of the function can be restricted to those values
(e.g. via `apt::restrict`),
and then the termination test can be transformed away
in the restricted domain.

Constructing the logic-mode function with the explicit termination test may be useful in program verification. The starting program-mode function could be the object of verification, or it may represent, in ACL2, a recursive or iterative program (fragment), in some programming language, that is the object of verification. Instead of having to prove termination right away in order to make the function amenable to any formal verification in ACL2, constructing a logic-mode function with an explicit termination test enables the ``deferral'' of the termination proof. The termination of certain programs may depend on fairly deep semantic properties of the programs (to the point of being inter-related with functional correctness): in these cases, it may be natural to prove these properties along with termination, instead of having to prove termination alone first.

The **def**ine **arb**itrary **rec**ursion')
constructs the logic-mode function with the explicit termination test,
from a specified program-mode function.
The program-mode function is specified as
a name, a list of arguments, and a body (as in `defun`):

The current implementation only works with program-mode functions that make one recursive call (so in this sense it does not support truly arbitrary recursion, but the `arbitrary' here refers to avoiding to prove termination), but it should be possible to extend the macro to handle functions that make multiple different recursive calls. The current implementation does not support guards yet, but it should be possible to add suitable support.

The fact that the program-mode function is constructed by

These design notes, which use this notation, provide the mathematical concepts and template proofs upon which this tool is based. These notes should be read alongside this reference documentation, which refers to the them in numerous places.

(defarbrec fn (x1 ... xn) body :update-names ... ; default nil :terminates-name ... ; default nil :measure-name ... ; default nil :nonterminating ... ; default :nonterminating :print ... ; default :result :show-only ... ; default nil )

Name of the function to introduce.

This is as in

defun.In the design notes, the program-mode

fn is denoted byf , while the logic-modefn is denoted by\hat{f} .

Formal arguments of the function to introduce.

These are as in

defun, but in addition they must not include anystobjs.In the design notes,

x1 , ...,xn are denoted byx_1,\ldots,x_n , or\overline{x} as a whole.

Body of the program-mode function; the logic-mode function has a body based on this one.

This is as in

defun, but with the following additional constraints.The program-mode function must contain a single recursive call, only call logic-mode functions (besides itself), return a non-multiple value, and have no input or output stobjs.

In the rest of this documentation page, for expository convenience, it is assumed that the program-mode function has the following form:

(defun fn (x1 ... xn) (if test<x1,...,xn> base<x1,...,xn> combine<x1,...,xn,(fn update-x1<x1,...,xn> ... update-xn<x1,...,xn>)>))In the design notes,

test<x1,...,xn> is denoted bya(\overline{x}) ,base<x1,...,xn> is denoted byb(\overline{x}) ,combine<x1,...,xn,y> is denoted byc(\overline{x},y) , and eachupdate-xi<x1,...,xn> is denoted byd_i(\overline{x}) for1 \leq i \leq n .

Determines the names of the generated iterated argument update functions, i.e. the functions that iterate the updates of the arguments in the recursive call of the program-mode function (see the `Generated Functions' section below).

It must be one of the following:

nil , to use, for each argumentxi :fn , followed by- , followed byxi , followed by* ; the symbols are in the same package asfn .- A
nil -terminated list ofn distinct symbols (that are not in the main Lisp package and that are not keywords), to use as the names of the functions.In the rest of this documentation page, let

update*-x1 , ...,update*-xn be the names of these functions.

Determines the name of the generated predicate that tests whether the program-mode function terminates.

It must be one of the following:

nil , to usefn followed by-terminates ; the symbol is in the same package asfn .- Any other symbol (that is not in the main Lisp package and that is not a keyword), to use as the name of the predicate.
In the rest of this documentation page, let

terminates be the name of this predicate.

Determines the name of the generated measure function of the logic-mode function.

It must be one of the following:

nil , to usefn followed by-measure ; the symbol is in the same package asfn .- Any other symbol (that is not in the main Lisp package and that is not a keyword), to use as the name of the measure function.
In the rest of this documentation page, let

measure be the name of this function.

Specifies the value that the logic-mode function returns when the program-mode function does not terminate.

It must be a term that includes no free variables other than

x1 , ...,xn , that only calls logic-mode functions, that returns a non-multiple value, and that has no output stobjs.In the rest of this documentation page, let

nonterminating be this term.

Customizes the screen output.

It must be one of the following:

nil , to print nothing.:error , to print only error output.:result , to print, besides error output, the functions described in the `Generated Functions' section below, i.e. the result ofdefarbrec .:all , to print, besides error output and the result (see:result above), ACL2's output in response to all the submitted events (the ones that form the result as well as some ancillary ones).If the call to

defarbrec is redundant (see the `Redundancy' section below), a message to that effect is printed on the screen, unlessnil .

Determines whether the event expansion of

defarbrec is submitted to ACL2 or printed on the screen:

nil , to submit it.t , to print it. In this case: the event expansion is printed even ifnil ; the generated functions are not printed separately (other than their appearance in the event expansion), even if:result or:all ; no ACL2 output is printed even if:all (because the event expansion is not submitted). If the call todefarbrec is redundant (see the `Redundancy' section below), the event expansion generated by the existing call is printed.

The iterated argument update functions:

(defun update*-xi (k x1 ... xn) (if (zp k) xi (update*-xi (1- k) update-x1<x1,...,xn> ... update-xn<x1,...,xn>)))In the design notes,

(update*-xi k x1 ... xn) is denoted byd_i^{k}(\overline{x}) for1 \leq i \leq n .

The predicate that tests the termination of the program-mode function:

(defun-sk terminates (x1 ... xn) (exists k test<(update*-x1 k x1 ... xn), ... (update*-xn k x1 ... xn)>))In the design notes,

terminates is denoted byt , andterminates-witness is denoted by\epsilon_t .

The measure function for the logic-mode function:

(defun measure (x1 ... xn k) (declare (xargs :measure (nfix (- (terminates-witness x1 ... xn) (nfix k))))) (let ((k (nfix k))) (if (or test<(update*-x1 k x1 ... xn), ..., (update*-xn k x1 ... xn)> (>= k (nfix (terminates-witness x1 ... xn)))) k (measure x1 ... xn (1+ k)))))In the design notes,

measure is denoted by\nu , andnfix is denoted by\phi .

The logic-mode function:

(defun fn (x1 ... xn) (declare (xargs :measure (measure x1 ... xn 0) :well-founded-relation o<)) (if (terminates x1 ... xn) (if test<x1,...,xn> base<x1,...,xn> combine<x1,...,xn,(fn update-x1<x1,...,xn> ... update-xn<x1,...,xn>)>) nonterminating))In the design notes, this logic-mode function

fn is denoted by\hat{f} .

A call of

A call to

If a call to

`defpun` produces a constrained (not defined) function.
Since APT transformations operate on defined functions,
having `defpun` produces only tail-recursive functions,
while

`defpun` documentation)
is a generalization of `defpun`,
but it still produces
a constrained (not defined) tail-recursive-only function.

`defpun` documentation)
extends `defpun` with executability,
but its use of `defexec` requires
that the domain over which the function terminates be provided right away,
and that the termination be proved right away.
Both things are deferred with

`defpm` produces a measure, termination predicate, and some theorems
that can be used to introduce a tail-recursive logic-mode function
similar to the one produced by `defthm-domain` serves to show that
the termination predicate holds in suitable domains.
However, the termination predicate generated by `defpm`
is constrained, not defined;
in constrast,
the termination predicate generated by `defpm` provides the components for defining it manually.

`defpm` documentation),
which supersedes

- Defarbrec-implementation
- Implementation of
`defarbrec`.