Loop$-recursion
Defining functions that recur from within FOR loop$ expressions
Examples
(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 nat-treep and copy-nat-tree each contain a simple
FOR loop$ (also see for-loop$) in which the function
being defined is called recursively. Copy-nat-tree is a little more
complicated than nat-treep because copy-nat-tree also contains a
recursive call outside of any loop$. Notice also that both events
specify the xargs :loop$-recursion t and explicitly provide a
:measure. The usual other xargs are optional but
:loop$-recursion t is required if recursion is used inside a FOR
loop$ and the measure must be made explicit.
Recursion is not allowed inside a DO loop$ expression. In fact,
ACL2 disallows the use of :loop$-recursion in the xargs of any
definition whose body contains a DO loop$. So this topic is only
about FOR loop$s.
Some examples of loop$-recursive definitions may be found in the book
projects/apply/loop-recursion-examples.lisp.
Warning: We advise you to use defun$ rather than defun when introducing a :logic mode loop$-recursive function.
When a loop$-recursive function is introduced it is assigned a badge.
This is required because we cannot translate the body of a
loop$-recursive function without a badge. However, no warrant is
assigned by defun. But it is impossible to reason about
applications (with 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
:logic mode loop$-recursive function — which is guaranteed to
involve applications of itself with apply$ — can't be reasoned
about or executed (except on data not exercising the recursive calls inside
loop$s). These inconveniences can be avoided by using defun$ when
introducing :logic mode loop$-recursive functions because
defun$ expands to a defun followed by 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 loop$-recursive functions you must provide a
suitable :induction hint. In addition, to be provable by induction,
theorems about loop$-recursive functions must be suitably general. This
topic is discussed further in loop$-recursion-induction.
Restrictions
If a function being defined exhibits recursion from within a loop$
body or within the WHEN or UNTIL clauses of a loop$ in a
defun of fn, then the defun must include an xargs
declaration with :loop$-recursion t. In addition,
- 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 the llist function in the
Community Books at books/ordinals/,
- fn must be tame, which implies it may not take or
return state or stobjs,
- every quoted lambda object in the body of fn must be
well-formed (see well-formed-lambda-objectp), which implies that
every such lambda 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 a loop$ scion
and not in some arbitrary scion,
- there is at least one recursive call of fn inside a quoted
lambda object which means that the loop$-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 loop$-recursive function. First, we assume
that most ACL2 functions are not loop$-recursive. So to keep
defun-processing as fast as possible, we require you to declare when you
are using loop$ recursion. That declaration triggers additional
checks.
But before checks can begin, we have to translate the body of fn
and since loop$s translate into calls of loop$ scions on quoted
lambdas and those must be tame, and since some of those lambdas
involve calls of 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 lambdas, the measure must be explicitly declared even
if it acl2-count.
To find every recursive call in a quoted lambda object those objects
must all be well-formed. If such an object occurs as the first argument of a
loop$ scion then we know it is only applied to elements of the
loop$ scion's target. Given that, we can investigate whether the
recursive calls in the lambda object are on smaller things. But if a
recursive call were to occur in a quoted lambda object that was passed
to some other kind of scion, we have no way to know (without extensive
analysis) to what it might be applied.
Some of these restrictions could be lifted with more analysis and coding.
For example, we could change the specification for the :loop$-recursion
xargs keyword so that instead of taking on a Boolean value it takes on a
badge. Then we could tentatively assign that badge to fn before
processing and check it afterwards. Our current thinking is to ask users to
live with these restrictions and let us see whether loop$-recursion is
useful (almost certainly it will be), whether the community can develop proof
techniques and tools to reason about them as effectively as we reason about
conventional recursive functions (we're optimistic), and whether investing
time in lifting some of these restrictions is worth it given all the other
ways we could improve ACL2.
Measure Conjectures
Measure conjectures must be generated for the recursive calls inside
loop$ bodies. (We also generate conjectures for the recursive calls the
other loop$-expression components, e.g., the WHEN clause, exactly
analogously, but we speak of the loop$ body only below. We also focus
on simple loop$s here but the conjectures described generalize to fancy
loop$s.) Given a recursive call inside the body of a loop$ with
iteration variable 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 loop$ from those inside. The measure conjecture
requires us to prove that the given measure decreases, as usual. But the
ruling tests are those ruling the loop$, conjoined with the hypothesis
that 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 loop$ because there are two recursive calls in the loop$
body.
(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 v used both as the formal of fn and as the iterative
variable of the loop$. In the measure conjectures below, the iterative
variable has been renamed to nv0. Two measure conjectures are generated
from within the loop$:
(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 fn is called from
within the loop$ the argument is smaller than the initial value of the
formal. Notice also that there is no a priori restriction on the size
of (target v). However, because of the way fn is used inside this
particular example loop$, there are restrictions on the size of the
elements of (target v). These conjectures, along with those generated
from calls outside the loop$ are sufficient to guarantee that fn
always terminates.
Note: Careful readers might note that the way we handle measure
conjectures for loop$s differs from the way we handle guard conjectures
for loop$s. In loop$ we explained that loop$s are
translated into calls of loop$ scions on quoted lambda
objects and that the guard conjectures for the lambda are insensitive to
the context in which the object appeared. But the measure conjectures are
sensitive to the context: tests from outside the loop$ are present in
the measure conjectures. This is deliberate. Guard conjectures are context
insensitive because the implementation caches compiled lambda objects
without remembering the contexts in which they first occurred. Thus, a
lambda object generated by a loop$ may be called on anything and we
cannot guarantee that the input guard to the lambda object will be
satisfied. But we can guarantee that the computation carried out by the
lambda will terminate! The lambda object generated for fn
above terminates no matter what it is called on -- even if called on elements
not in (target v) -- because fn terminates.
Finally, recall that loop$-recursive functions do not automatically
suggest induction schemes and that special care must be taken when
formulating inductively provable conjectures about them. See loop$-recursion-induction.
Subtopics
- Definductor
- Create an induction scheme for a loop$-recursive function
