Limiting the effort expended on relieving hypotheses

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-split`s and `force`d 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

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 reasoning'', which uses rules of class `type-prescription` rules (see type-reasoning). 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 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

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 `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 `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

- Set-default-backchain-limit
- Sets the default backchain-limit used when admitting a rule
- Set-backchain-limit
- Sets the backchain-limit used by the type-set and rewriting mechanisms