Forward-chaining
Make a rule to forward chain when a certain trigger arises
See rule-classes for a general discussion of rule classes,
including how they are used to build rules from formulas and a discussion of
the various keywords in a rule class description.
Examples:
(defthm p-and-r-forward ; When (p a) appears in a formula to be
(implies (and (p x) (r x)) ; simplified, try to establish (p a) and
(q (f x))) ; (r a) and, if successful, add (q (f a))
:rule-classes :forward-chaining) ; to the known assumptions.
(defthm p-and-r-forward ; as above with most defaults filled in
(implies (and (p x) (r x))
(q (f x)))
:rule-classes ((:forward-chaining :trigger-terms ((p x))
:corollary (implies (and (p x) (r x))
(q (f x)))
:match-free :all)))
To specify the triggering terms provide a non-empty list of terms as the
value of the :trigger-terms field of the rule class object.
General Form:
Any theorem, provided an acceptable triggering term exists.
The structure of this documentation is as follows. First we give a brief
overview of forward chaining and contrast it to backchaining (rewriting).
Then we lay out the syntactic restrictions on :forward-chaining rules.
Then we give more details about the process and point to a tool to assist you
in debugging your :forward-chaining rules.
Overview and When to Use Forward Chaining
Forward chaining is performed as part of the simplification process: before
the goal is rewritten a context is established. The context tells the
theorem prover what may be assumed during rewriting, in particular, to
establish hypotheses of rewrite rules. Forward chaining is used to extend the
context before rewriting begins. For example, the :forward-chaining rule
(implies (p x) (p1 x)) would add (p1 A) to the context, where A
is some term, if (p A) is already in the context.
Forward chaining and backchaining are duals. If a rewrite rule requires
that (p1 A) be established and (p A) is known, it could be done
either by making (implies (p x) (p1 x)) a :forward-chaining rule or
a :rewrite rule. Which should you choose?
As a rule of thumb, if a conclusion like (p1 A) is expected to be
widely needed, it is better to derive it via forward chaining because then it
is available ``for free'' during the rewriting after paying the one-time cost
of forward chaining. Alternatively, if (p1 A) is a rather special
hypothesis of key importance to only a few rewrite rules, it is best to derive
it only when needed through backchaining. Thus forward chaining is pro-active
and backward chaining (rewriting) is reactive.
The following example illustrates that forward chaining may be
indispensable in a scenario with free-variables, whose handling is
quite weak with rewrite rules.
(defstub p0 (x) t)
(defstub p1 (x) t)
(defstub p2 (y) t)
(defaxiom p0-implies-p1
(implies (p0 x)
(p1 x))
:rule-classes :forward-chaining)
(defaxiom p1-implies-p2
(implies (p1 x)
(p2 y)))
; ACL2 proves the following, but only because p0-implies-p1 is a
; :forward-chaining rule. If p0-implies-p1 is instead a :rewrite
; rule, then the proof fails for the following event.
(thm (implies (p0 x)
(p2 y)))
Syntactic Restrictions
Forward chaining rules are generated from the corollary term (see rule-classes) as follows. First, every let expression is expanded
away (hence, so is every let* and lambda expression), and
trivial ``guard holders'' are removed; see guard-holders. If the
resulting term has the form (implies hyp concl), then concl is
treated as a conjunction, with one forward chaining rule with hypothesis
hyp created for each conjunct. In the other case, where the corollary
term is not an implies, we process it as we process the conclusion in
the first case.
Note that unlike rewrite rules, a nested implication is not folded into a
single implication. Consider for example the following term.
(implies (p1 x)
(implies (p2 x)
(p3 x)))
Although this term is parsed for a rewrite rule as (implies (and (p1 x)
(p2 x)) (p3 x)), that is not the case when this term is parsed for a
forward-chaining rule, in which case (p1 x) is treated as the hypothesis
and (implies (p2 x) (p3 x)) is treated as the conclusion.
The :trigger-terms field of a :forward-chaining rule class object
should be a non-empty list of terms, if provided, and should have certain
properties described below. If the :trigger-terms field is not provided,
it defaults to the singleton list containing the ``atom'' of the first
hypothesis of the formula. (The atom of (not x) is x; the atom of
any other term is the term itself.) If there are no hypotheses and no
:trigger-terms were provided, an error is caused.
A triggering term is acceptable if it is not a variable, a quoted constant,
a lambda application, a let- (or let*-) expression, or a
not-expression, and every variable symbol in the conclusion of the
theorem either occurs in the hypotheses or occurs in the trigger.
More Details about Forward Chaining
:Forward-chaining rules are used by the simplifier before it
begins to rewrite the literals of the goal. (Forward chaining is thus carried
out from scratch for each goal.) If any term in the goal is an instance of a
trigger of some forward chaining rule, we try to establish the hypotheses of
that forward chaining theorem (from the negation of the goal). To relieve a
hypothesis we only use type
reasoning, evaluation of ground terms, and presence among our known
assumptions. We do not use rewriting. So-called free variables in hypotheses
are treated specially; see free-variables. If all hypotheses are
relieved, and certain heuristics approve of the newly derived conclusion, we
add the instantiated conclusion to our known assumptions. Since this might
introduce new terms into the assumptions, forward chaining is repeated.
Heuristic approval of each new addition is necessary to avoid infinite looping
as would happen with the rule (implies
(p x) (p (f x))), which might otherwise forward chain from (p A) to
(p (f A)) to (p (f (f A))), etc.
Caution. Forward chaining does not actually add terms to the goals
displayed during proof attempts. Instead, it extends an associated
context, called ``assumptions'' in the preceding paragraph, that ACL2
builds from the goal currently being proved. (For insiders: forward chaining
extends the type-alist.) The context starts out with ``obvious''
consequences of the negation of the goal. For example, if the goal is
(implies (and (p A) (q (f A)))
(c A))
then the context notes that (p A) and (q (f A)) are non-nil
and (c A) is nil. Forward chaining is then used to expand the
context. For example, if a forward chaining rule has (f x) as a trigger
term and has body (implies (p x) (r (f x))), then the context is extended
by binding (r (f A)) to non-nil, provided the heuristics approve of
this extension. Note however that since (r (f A)) is put into the
context, not the goal, you will not see it in the goal formula. Furthermore,
the assumption added to the context is just the instantiation of the
conclusion of the rule, with no simplification or rewriting applied. Thus,
for example, if it contains an enabled non-recursive function symbol it is
unlikely ever to match a (rewritten) term arising during subsequent
simplification of the goal.
However, forward-chaining does support the linear arithmetic reasoning
package. For example, suppose that forward-chaining puts (< (f x) (g x))
into the context. Then this inequality also goes into the linear arithmetic
database, together with suitable instances of linear lemmas whose trigger term
is a call of g. See linear.
Debugging :forward-chaining rules can be difficult since their effects
are not directly visible on the goal being simplified. Tools are available to
help you discover what forward chaining has occurred see forward-chaining-reports.
Subtopics
- Forward-chaining-reports
- To see reports about the forward chaining process
- Case-split
- Like force but immediately splits the top-level goal on the hypothesis
