Mutual-recursion
Define some mutually recursive functions
See defun for relevant background.
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. Note that although one definition is
acceptable, we focus on the case of at least two definitions, since normally
one would not bother with mutual-recursion otherwise.
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.
However, for the following xargs declarations, listed
alphabetically, it is illegal to specify more than one value, though it is
legal to specify the same value more than once.
:GUARD-DEBUG
:GUARD-SIMPLIFY
:LOOP$-RECURSION
:MEASURE-DEBUG
:MODE
:NON-EXECUTABLE
:NORMALIZE
:OTF-FLG
:SPLIT-TYPES
:VERIFY-GUARDS
:WELL-FOUNDED-RELATION
Thus, for example, you may specify :guard-debug t in two different
defun forms in your mutual-recursion call, in which case the guard-debug feature will be active; but you must not specify :guard-debug
t in one defun but :guard-debug nil in another. It suffices to
specify such a value once, as that will apply throughout analysis of the
mutual-recursion 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 defuns specifies the :verify-guards xarg to be nil, then guard verification is
omitted for all of the functions. Similarly, if any one of the defuns
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))).Subtopics
- Defines
- A very fine alternative to mutual-recursion.
- Make-flag
- Create a flag-based ACL2::induction scheme for a mutual-recursion.
- Mutual-recursion-proof-example
- A small proof about mutually recursive functions
- Def-doublevar-induction
- Create an induction scheme that adds a duplicate variable to the substitution.
- Set-bogus-mutual-recursion-ok
- Allow unnecessary ``mutual recursion''
- Defuns
- An alternative to mutual-recursion
