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.
