Major Section: RULE-CLASSES
See rule-classes for a general discussion of rule classes and how they are
used to build rules from formulas. An example :corollary formula
from which a :forward-chaining rule might be built is:
Example:
(implies (and (p x) (r x)) ; when (p a) appears in a formula to be
(q (f x))) ; simplified, try to establish (r a) and
; if successful, add (q (f a)) to the
; known assumptions
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 the rewriting, e.g., to establish
hypotheses of rewrite rules. For example, if the goal is
(implies (and (p A) (q A)) (r A)), then when (r A) is being
rewritten, the context tells us we may assume (p A) and (q A).
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.
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. Thus forward chaining is pro-active
and backward chaining (rewriting) is reactive.
Syntactic Restrictions
Forward chaining rules are generated from the corollary term as follows.
First, every let expression is expanded away (hence, so is every
let* and lambda expression), as is every call of a so-called
``guard holder,'' mv-list or return-last (the latter resulting
from macroexpansion of calls of prog2$, must-be-equal or
mbe), ec-call, and a few others), or `the'. 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.
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.
