Major Section: MISCELLANEOUS
Subtleties arise when one of the ``constrained'' functions,
introduced in the signature of an
encapsulate event, is
involved in the termination argument for a non-local recursively
g, in that
encapsulate. During the
processing of the encapsulated events,
f is locally defined to
be some witness function,
f'. Properties of
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
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
f. In addition, ACL2 removes from its knowledge
g any suggestions about legal inductions to ``unwind'' its
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''
f in order to admit
g, e.g., constrain it to
reduce some ordinal measure. However, by separating the
f from the admission of
g you will clearly
identify the necessary constraints on
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
fon the bogus grounds that the only use of
fin 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 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
mapplays the role of
mapcalls the constrained function
maptruly does not constrain
f. In particular, the definition of
mapcould be moved ``out'' of the encapsulate so that
mapis introduced afterwards. The difference between
gis 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
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.