MUTUAL-RECURSION

define some mutually recursive functions

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)))
General Form:
(mutual-recursion def1 ... defn)
where each defi is a call of defun , defund , defun-nx ,
or defund-nx.

When mutually recursive functions are introduced it is necessary to do the termination analysis on the entire clique of definitions. Each 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. Similarly, if any one of the defun s specifies the :non-executable xarg to be t, or if any of the definitions uses defun-nx or defund-nx, then every one of the definitions will be treated as though it specifies a :non-executable xarg of t.

Technical Note: Each defi above must be a call of defun , defund , defun-nx , or defund-nx. In particular, it is not permitted for a defi to be an arbitrary form that macroexpands 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 macroexpanded.

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))).