Defining functions that recur from within

(defun$ nat-treep (x) (declare (xargs :loop$-recursion t :measure (acl2-count x))) (cond ((atom x) (natp x)) (t (and (true-listp x) (eq (car x) 'NATS) (loop$ for e in (cdr x) always (nat-treep e)))))) (defun$ copy-nat-tree (x) (declare (xargs :loop$-recursion t :measure (acl2-count x))) (cond ((atom x) (if (natp x) (if (equal x 0) 0 (+ 1 (copy-nat-tree (- x 1)))) x)) (t (cons 'nats (loop$ for e in (cdr x) collect (copy-nat-tree e))))))

Notice that `loop$` (also see for-loop$) in which the function
being defined is called recursively. `xargs`

Recursion is not allowed inside a

Some examples of

**Warning:** We advise you to use `defun$` rather than `defun` when introducing a `apply$`) of unwarranted functions. Indeed, it is
even impossible to execute such applications in the top-level ACL2
read-eval-print loop. See guarantees-of-the-top-level-loop. So a
`defwarrant`.

**Warning:** Even though the functions defined above are recursive,
ACL2 does not generate induction schemes for them! If you want to do
inductive proofs about

If a function being defined exhibits recursion from within a `loop$`
body or within the `defun` of *fn*, then the `xargs`
declaration with

- the
xargs declaration must include an explicit:measure , *fn*must not be part of a`mutual-recursion`clique,- every formal of
*fn*must be ``ordinary,'' e.g., not of`ilk`:FN or:EXPR , *fn*must return a single value,*fn*'s measure must be of type`natp`or be a lexicographic combination of natural numbers as defined by thellist function in the Community Books atbooks/ordinals/ ,*fn*must be`tame`, which implies it may not take or return`state`or`stobj`s,- every quoted
`lambda`object in the body of*fn*must be well-formed (see`well-formed-lambda-objectp`), which implies that every suchlambda object is tame and every function symbol, including*fn*, used in each must have a`badge`, - every quoted
lambda object in the body of*fn*that calls*fn*recursively must occur as the first argument of aloop$ scion and*not*in some arbitrary scion, - there is at least one recursive call of
*fn*inside a quotedlambda object which means that theloop$-recursion t declaration was actually necessary, and - the necessary measure conjectures (see below) must be proved.

These restrictions make a little more sense if you reflect on what has to
be done to check and admit a

But before checks can begin, we have to translate the body of *fn*
and since *fn*, we must assign a badge to *fn* even before
we have translated its body. We assign a badge that declares *fn* to
take the appropriate number of ordinary inputs, to return one result, and be
tame. We check those requirements after *fn* has been admitted.

Because the measure guessing heuristics of ACL2 do not look for calls
inside of quoted

To find every recursive call in a quoted

Some of these restrictions could be lifted with more analysis and coding.
For example, we could change the specification for the *fn* before
processing and check it afterwards. Our current thinking is to ask users to
live with these restrictions and let us see whether

Measure conjectures must be generated for the recursive calls inside
*v*, we first generate a new variable symbol,
*v'*. Certain terms, e.g., tests and arguments to recursive calls, will
be extracted from within the body and used in the measure conjecture. We
rename *v* to *v'* in these terms to distinguish occurrences of
*v* outside the *v'* is a member of the target, conjoined with the (renamed) tests
from inside the body ruling the recursive call.

Below is an example. We show only the measure conjectures generated from
inside the

(defun$ fn (v) (declare (xargs :loop$-recursion t :measure (acl2-count x))) (cond ((natp v) ...) ((true-listp v) (loop$ for v in (target v) sum (if (and (integerp v) (< v 0)) (fn (- v)) (fn v)))) (t ...)))

Note that

(implies (and (not (natp v)) (true-listp v) (member-equal nv0 (target v)) (and (integerp nv0) (< nv0 0))) (o< (acl2-count (- nv0)) (acl2-count v))) (implies (and (not (natp v)) (true-listp v) (member-equal nv0 (target v)) (not (and (integerp nv0) (< nv0 0)))) (o< (acl2-count nv0) (acl2-count v)))

Note that these conjectures require that when *a priori* restriction on the size
of

**Note:** Careful readers might note that the way we handle measure
conjectures for `loop$` we explained that `scion`s on quoted `lambda`
objects and that the guard conjectures for the *But we can guarantee that the computation carried out by the
lambda will terminate!* The

Finally, recall that

- Definductor
- Create an induction scheme for a
loop$ -recursive function