Major Section: EVENTS

Example: (mutual-recursion (defun evenlp (x) (if (consp x) (oddlp (cdr x)) t)) (defun oddlp (x) (if (consp x) (evenlp (cdr x)) nil)))When mutually recursive functions are introduced it is necessary to do the termination analysis on the entire clique of definitions. EachGeneral Form: (mutual-recursion def1 ... defn) where each defi is a

`defun`

form or a`defund`

form.

`defun`

form specifies its own measure, either with the `:measure`

keyword `xarg`

(see xargs) or by default to `acl2-count`

. When a
function in the clique calls a function in the clique, the measure
of the callee's actuals must be smaller than the measure of the
caller's formals -- just as in the case of a simply recursive
function. But with mutual recursion, the callee's actuals are
measured as specified by the callee's `defun`

while the caller's
formals are measured as specified by the caller's `defun`

. These two
measures may be different but must be comparable in the sense that
`o<`

decreases through calls.
If you want to specify `:`

`hints`

or `:guard-hints`

(see xargs), you
can put them in the `xargs`

declaration of any of the `defun`

forms,
as the `:`

`hints`

from each form will be appended together, as will the
`guard-hints`

from each form.

You may find it helpful to use a lexicographic order, the idea being to have a measure that returns a list of two arguments, where the first takes priority over the second. Here is an example.

(include-book "ordinals/lexicographic-ordering" :dir :system)(encapsulate () (set-well-founded-relation l<) ; will be treated as LOCAL

(mutual-recursion (defun foo (x) (declare (xargs :measure (list (acl2-count x) 1))) (bar x)) (defun bar (y) (declare (xargs :measure (list (acl2-count y) 0))) (if (zp y) y (foo (1- y))))))

The `guard`

analysis must also be done for all of the functions at
the same time. If any one of the `defun`

s specifies the
`:`

`verify-guards`

`xarg`

to be `nil`

, then guard verification is
omitted for all of the functions.

Technical Note: Each `defi`

above must be of the form `(defun ...)`

. In
particular, it is not permitted for a `defi`

to be a form that will
macroexpand into a `defun`

form. This is because `mutual-recursion`

is
itself a macro, and since macroexpansion occurs from the outside in,
at the time `(mutual-recursion def1 ... defk)`

is expanded the `defi`

have not yet been. But `mutual-recursion`

must decompose the `defi`

.
We therefore insist that they be explicitly presented as `defun`

s or
`defund`

s (or a mixture of these).

Suppose you have defined your own `defun`

-like macro and wish to use
it in a `mutual-recursion`

expression. Well, you can't. (!) But you
can define your own version of `mutual-recursion`

that allows your
`defun`

-like form. Here is an example. Suppose you define

(defmacro my-defun (&rest args) (my-defun-fn args))where

`my-defun-fn`

takes the arguments of the `my-defun`

form and
produces from them a `defun`

form. As noted above, you are not
allowed to write `(mutual-recursion (my-defun ...) ...)`

. But you can
define the macro `my-mutual-recursion`

so that
(my-mutual-recursion (my-defun ...) ... (my-defun ...))expands into

`(mutual-recursion (defun ...) ... (defun ...))`

by
applying `my-defun-fn`

to each of the arguments of
`my-mutual-recursion`

.
(defun my-mutual-recursion-fn (lst) (declare (xargs :guard (alistp lst))); Each element of lst must be a consp (whose car, we assume, is always ; MY-DEFUN). We apply my-defun-fn to the arguments of each element and ; collect the resulting list of DEFUNs.

(cond ((atom lst) nil) (t (cons (my-defun-fn (cdr (car lst))) (my-mutual-recursion-fn (cdr lst))))))

(defmacro my-mutual-recursion (&rest lst)

; Each element of lst must be a consp (whose car, we assume, is always ; MY-DEFUN). We obtain the DEFUN corresponding to each and list them ; all inside a MUTUAL-RECURSION form.

(declare (xargs :guard (alistp lst))) (cons 'mutual-recursion (my-mutual-recursion-fn lst))).