SUBVERSIVE-RECURSIONS

why we restrict encapsulated recursive functions
```Major Section:  MISCELLANEOUS
```

Subtleties arise when one of the ``constrained'' functions, `f`, introduced in the signature of an `encapsulate` event, is involved in the termination argument for a non-local recursively defined function, `g`, in that `encapsulate`. During the processing of the encapsulated events, `f` is locally defined to be some witness function, `f'`. Properties of `f'` are explicitly proved and exported from the encapsulate as the constraints on the undefined function `f`. But if `f` is used in a recursive `g` defined within the encapsulate, then the termination proof for `g` may use properties of `f'` -- the witness -- that are not explicitly set forth in the constraints stated for `f`.

Such recursive `g` are said be ``subversive'' because if naively treated they give rise to unsound induction schemes or (via functional instantiation) recurrence equations that are impossible to satisfy. We illustrate what could go wrong below.

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 `g` becomes one of the constraints on `f`. This is generally a severe restriction on future functional instantiations of `f`. In addition, ACL2 removes from its knowledge of `g` any suggestions about legal inductions to ``unwind'' its recursion.

What should you do? Often, the simplest response is to move the offending recursive definition, e.g., `g`, out of the encapsulate. That is, introduce `f` by constraint and then define `g` as an ``independent'' event. You may need to constrain ``additional'' properties of `f` in order to admit `g`, e.g., constrain it to reduce some ordinal measure. However, by separating the introduction of `f` from the admission of `g` you will clearly identify the necessary constraints on `f`, functional instantiations of `f` will be simpler, and `g` will be a useful function which suggests inductions to the theorem prover.

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 `f` on the bogus grounds that the only use of `f` in the encapsulate is in an admissible function. We discuss the plausibility of this bogus argument in a moment.

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 `(f '(a . b))` were `'(a . b)`, then `(g '(a . b))` would be `(not (g '(a . b)))`, which is impossible.

But then we could functionally instantiate `f-not-identity`, replacing `f` by the identity function, to prove `nil`! This is bad.

```(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 `g` above poses no constraint on `f`? Here is a very similar encapsulate.

```(encapsulate (((f *) => *))
(local (defun f (x) (cdr x)))
(defun map (x)
(if (consp x)
(cons (f x) (map (cdr x)))
nil)))
```
Here `map` plays the role of `g` above. Like `g`, `map` calls the constrained function `f`. But `map` truly does not constrain `f`. In particular, the definition of `map` could be moved ``out'' of the encapsulate so that `map` is introduced afterwards. The difference between `map` and `g` is that the constrained function plays no role in the termination argument for the one but does for the other.

As a ``user-friendly'' gesture, ACL2 implicitly moves `map`-like functions out of encapsulations; logically speaking, they are introduced after the encapsulation. This simplifies the constraint. This is done only for ``top-level'' encapsulations. When an `encapsulate` containing a non-empty signature list is embedded in another `encapsulate` with a non-empty signature list, no attempt is made to move `map`-like functions out. The user is advised, via the ``infected'' warning, to phrase the encapsulation in the simplest way possible.

The lingering bug between Versions 1.5 and 2.3 mentioned above was due to our failure to detect the `g`-like nature of some functions when they were defined in mutually recursively cliques with other functions. The singly recursive case was recognized. The bug arose because our detection ``algorithm'' was based on the ``suggested inductions'' left behind by successful definitions. We failed to recall that mutually-recursive definitions do not, as of this writing, make any suggestions about inductions and so did not leave any traces of their subversive natures.  