Why we restrict encapsulated recursive functions

Subtleties arise when one of the ``constrained'' functions, `encapsulate` event, is
involved in the termination argument for a non-local recursively defined
function,

Such recursive

Subversive recursions are not banned outright. Instead, they are treated
as part of the constraint. That is, in the case above, the definitional
equation for

What should you do? Often, the simplest response is to move the offending
recursive definition, e.g.,

Note that the functions introduced in the signature should not even occur ancestrally in the termination proofs for non-local recursive functions in the encapsulate. That is, the constrained functions of an encapsulate should not be reachable in the dependency graph of the functions used in the termination arguments of recursive functions in encapsulate. If they are reachable, their definitions become part of the constraints.

The following event illustrates the problem posed by subversive recursions.

(encapsulate (((f *) => *)) (local (defun f (x) (cdr x))) (defun g (x) (if (consp x) (not (g (f x))) t)))

Suppose, contrary to how ACL2 works, that the encapsulate above were to
introduce no constraints on

Then it would be possible to prove the theorem:

(defthm f-not-identity (not (equal (f '(a . b)) '(a . b))) :rule-classes nil :hints (("Goal" :use (:instance g (x '(a . b))))))

simply by observing that if

But then we could functionally instantiate

(defthm bad nil :rule-classes nil :hints (("Goal" :use (:functional-instance f-not-identity (f identity)))))

This sequence of events was legal in versions of ACL2 prior to Version 1.5. When we realized the problem we took steps to make it illegal. However, our steps were insufficient and it was possible to sneak in a subversive function (via mutual recursion) as late as Version 2.3.

We now turn to the plausibility of the bogus argument above. Why might one
even be tempted to think that the definition of

(encapsulate (((f *) => *)) (local (defun f (x) (cdr x))) (defun map (x) (if (consp x) (cons (f x) (map (cdr x))) nil)))

Here

As a ``user-friendly'' gesture, ACL2 implicitly moves

The lingering bug between Versions 1.5 and 2.3 mentioned above was due to
our failure to detect the

We conclude by elaborating on the criterion ``involved in the termination
argument'' mentioned at the outset. Suppose that function `encapsulate`, where the body of `encapsulate`, i.e.: the body contains no call of a signature function, no call
of a function whose body calls a signature function, and so on. Then ACL2
treats

(encapsulate (((h *) => *)) (local (defun h (n) n)) (defun f (i n) (if (zp i) n (f (1- i) (h n)))))

ACL2 heuristically picks the measure