Subversive-recursions
Why we restrict encapsulated recursive functions
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. When the constraint
cannot be thus simplified the user is advised, via the ``infected'' warning,
to phrase the encapsulation in the simplest way possible. See infected-constraints.
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.
We conclude by elaborating on the criterion ``involved in the termination
argument'' mentioned at the outset. Suppose that function f is
recursively defined in an encapsulate, where the body of f has no
``ancestor'' among the functions introduced in the signature of that 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 f as though it is defined in front of that encapsulate form;
so f is not constrained by the encapsulate, and its definition is
hence certainly not subversive in the sense discussed above. But suppose to
the contrary that some function introduced in the signature is an ancestor of
the body of f. Then the definition of f is subversive if moreover,
its termination proof obligation has an ancestor among the signature
functions. Now, that proof obligation involves terms from the first argument
of selected calls of IF, as well as recursive calls; for a detailed
discussion, see rulers. The important point here is that for the
recursive calls, only the arguments in ``measured'' positions are relevant to
the termination proof obligation. Consider the following example.
(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 (acl2-count i) for the definition
of f; thus, i is the only ``measured formal'' of f. Since
i is the first formal of f, then for the recursive call of f,
only the first argument contributes to the termination proof obligation: in
this case, (1- i) but not (h n). Thus, even though h is a
signature function, the definition of f is not considered to be
subversive; an induction scheme is thus stored for f. (This restriction
to measured formal positions of recursive calls, for determining subversive
definitions, is new in Version_3.5 of ACL2.)
