Major Section: MISCELLANEOUS
Before ACL2 can apply a rule with hypotheses, it must establish that the
hypotheses are true. (We ignore the relaxing of this requirement afforded by
case-splits and forced hypotheses.) ACL2 typically establishes
each hypothesis by backchaining -- instantiating the hypothesis and then
rewriting it recursively. Here we describe how ACL2 allows the user to limit
backchaining. At the end, below, we describe the function
backchain-limit.
Each hypothesis of a rewrite, meta, linear, or
type-prescription rule is assigned a backchain-limit when the rule is
stored. By default, this limit is nil, denoting infinity (no limit).
However, the value used for the default may be set to a non-negative
integer (or to nil) by the user; see set-default-backchain-limit. The
default is overridden when a :backchain-limit-lst is supplied explicitly
with the rule; see rule-classes. The number of recursive applications of
backchaining starting with the hypothesis of a rule is limited to the
backchain-limit associated with that hypothesis.
Moreover, the user may set global backchain-limits that limit the total
backchaining depth. See set-backchain-limit. One limit is for the use of
rewrite, meta, and linear rules, while the other limit is
for so-called ``type-set reasoning'', which uses rules of class
type-prescription rules. The two limits operate independently. Below,
we discuss the first kind of backchain limits, i.e., for other than
type-prescription rules, except as otherwise indicated; but the
mechanism for those rules is similar.
Below we lay out the precise sense in which a global backchain-limit
interacts with the backchain-limits of individual rules in order to limit
backchaining. But first we note that when further backchaining is
disallowed, ACL2 can still prove a hypothesis in a given context by using
that contextual information. In fact, type-set reasoning may be
used (except that a weaker version of it is used in the second case above,
i.e., where we are already doing type-set reasoning). Thus, the relieving of
hypotheses may be limited to the use of contextual information (without
backchaining, i.e., without recursively rewriting hypotheses) by executing
:set-backchain-limit 0.
Recall that there are two sorts of backchain limits: those applied to
hypotheses of individual rules, as assigned by their :rule-classes
or else taken from the default (see set-default-backchain-limit); and the
global limit, initially nil (no limit) but settable with
:set-backchain-limit. Here is how these two types of limits
interact to limit backchaining, i.e., recursive rewriting of hypotheses.
ACL2 maintains a current backchain limit, which is the limit on the depth of
recursive calls to the rewriter, as well as a current backchain depth, which
is initially 0 and is incremented each time ACL2 backchains (and is
decremented when a backchain completes). When ACL2 begins to rewrite a
literal (crudely, one of the ``top-level'' terms of the goal currently being
worked on), it sets the current backchain-limit to the global value, which is
initially nil but can be set using :set-backchain-limit. When
ACL2 is preparing to relieve a hypothesis by backchaining (hence, after it
has already tried type-set reasoning), it first makes sure that the current
backchain limit is greater than the current backchain depth. If not, then it
refuses to relieve that hypothesis. Otherwise, it increments the current
backchain depth and calculates a new current backchain-limit by taking the
minimum of two values: the existing current backchain-limit, and the sum of
the current backchain depth and the backchain-limit associated with the
hypothesis. Thus, ACL2 only modifies the current backchain-limit if it is
necessary to decrease that limit in order to respect the backchain limit
associated with the hypothesis.
We illustrate with the following examples.
; We stub out some functions so that we can reason about them.
(defstub p0 (x) t)
(defstub p1 (x) t)
(defstub p2 (x) t)
(defstub p3 (x) t)
; Initially, the default-backchain-limit is nil, or infinite.
(defaxiom p2-implies-p1-limitless
(implies (p2 x)
(p1 x)))
; The following rule will have a backchain-limit of 0.
(defaxiom p1-implies-p0-limit-0
(implies (p1 x)
(p0 x))
:rule-classes ((:rewrite :backchain-limit-lst 0)))
; We have (p2 x) ==> (p1 x) ==> (p0 x). We wish to establish that
; (p2 x) ==> (p0 x). Normally, this would be no problem, but here
; we fail because ACL2 cannot establish (p0 x) by type-set reasoning
; alone.
(thm
(implies (p2 x)
(p0 x)))
; We set the default-backchain-limit (for rewriting) to 1.
:set-default-backchain-limit 1
; The following is more powerful than p1-implies-p0-limit-0
; because it can use rewrite rules to establish (p1 x).
(defaxiom p1-implies-p0-limit-1
(implies (p1 x)
(p0 x)))
; This theorem will succeed:
(thm
(implies (p2 x)
(p0 x)))
; We return the default-backchain-limit to its initial value.
:set-default-backchain-limit nil
; Here is our last axiom.
(defaxiom p3-implies-p2-limitless
(implies (p3 x)
(p2 x)))
; We now have (p3 x) ==> (p2 x) ==> (p1 x) ==> (p0 x). However the
; rule p1-implies-p0-limit-1 has a backchain-limit of 1; hence we
; are not allowed to backchain far enough back to use
; p3-implies-p2-limitless. We therefore lose.
(defthm will-fail
(implies (p3 x)
(p0 x)))
Finally, we remark that to see the current global backchain-limits, issue the following commands.
(backchain-limit wrld :ts) ; backchain limit for type-set reasoning (backchain-limit wrld :rewrite) ; backchain limit for rewriting
