Free-variables
Free variables in rules
As described elsewhere (see rule-classes), ACL2 rules are
treated as implications for which there are zero or more hypotheses hj to
prove. In particular, rules of class :rewrite may look like
this:
(implies (and h1 ... hn)
(fn lhs rhs))
Variables of hi are said to occur free in the above
:rewrite rule if they do not occur in lhs or in any hj with
j<i. (To be precise, here we are only discussing those variables that
are not in the scope of a let/let*/lambda that binds
them.) We also refer to these as the free variables of the rule. ACL2
may issue a warning or error when there are free variables in a rule, as
described below. (Variables of rhs may be considered free if they do not
occur in lhs or in any hj. But we do not consider those in this
discussion.)
In general, the free variables of rules are those variables
occurring in their hypotheses (not let/let*/lambda-bound)
that are not bound when the rule is applied. For rules of class :linear and :forward-chaining, variables are bound by a trigger
term. (See rule-classes for a discussion of the :trigger-terms
field). For rules of class :type-prescription, variables are
bound by the :typed-term field.
See free-variables-examples for more examples of how this all works,
including illustration of how the user can exercise some control over it. In
particular, see free-variables-examples-rewrite for an explanation of
output from the break-rewrite facility in the presence of rewriting
failures involving free variables, as well as an example exploring ``binding
hypotheses'' as described below.
Let us discuss the method for relieving hypotheses of rewrite rules
with free variables. Similar considerations apply to linear and forward-chaining rules, and type-prescription rules. Note that the
:match-free mechanism discussed below does not apply to type-prescription rules. See free-variables-type-prescription for a
discussion of how to control free-variable matching for type-prescription rules.
We begin with an example. Does the proof of the thm below
succeed?
(defstub p2 (x y) t)
(defaxiom p2-trans
(implies (and (p2 x y)
(p2 y z))
(equal (p2 x z) t))
:rule-classes ((:rewrite :match-free :all)))
(thm (implies (and (p2 a c)
(p2 a b)
(p2 c d))
(p2 a d)))
Consider what happens when the proof of the thm is attempted. The
ACL2 rewriter attempts to apply rule p2-trans to the conclusion, (p2 a
d). So, it binds variables x and z from the left-hand side of the
conclusion of p2-trans to terms a and d, respectively, and then
attempts to relieve the hypotheses of p2-trans. The first hypothesis of
p2-trans, (p2 x y), is considered first. Variable y is free in
that hypothesis, i.e., it has not yet been bound. Since x is bound to
a, the rewriter looks through the context for a binding of y such
that (p2 a y) is true, and it so happens that it first finds the term
(p2 a b), thus binding y to b. Now it goes on to the next
hypothesis, (p2 y z). At this point y and z have already been
bound to b and d; but (p2 b d) cannot be proved.
So, in order for the proof of the thm to succeed, the rewriter
needs to backtrack and look for another way to instantiate the first
hypothesis of p2-trans. Because :match-free :all has been
specified, backtracking does take place. This time y is bound to c,
and the subsequent instantiated hypothesis becomes (p2 c d), which is
true. The application of rule (p2-trans) succeeds and the theorem is
proved.
If instead :match-free :all had been replaced by :match-free
:once in rule p2-trans, then backtracking would not occur, and the
proof of the thm would fail.
Next we describe in detail the steps used by the rewriter in dealing with
free variables.
The ACL2 rewriter uses the following sequence of steps to relieve a
hypothesis with free variables, except that steps (1) and (3) are skipped for
:forward-chaining rules and step (3) is skipped for
:type-prescription rules. First, if the hypothesis is of the form
(force hyp0) or (case-split hyp0), then replace it with
hyp0.
(1) Suppose the hypothesis has the form (equiv var term)
where var is free and no variable of term is free, and either
equiv is equal or else equiv is a known equivalence
relation and term is a call of double-rewrite. We call this a
``binding hypothesis.'' Then bind var to the result of rewriting
term in the current context.
(2) Look for a binding of the free variables of the hypothesis so that the
corresponding instance of the hypothesis is known to be true in the current
context.
(3) Search all enabled, hypothesis-free rewrite rules of the form
(equiv lhs rhs), where lhs has no variables (other than those bound
by let, let*, or lambda), rhs is known to be true in
the current context, and equiv is typically equal but can be any
equivalence relation appropriate for the current context (see congruence); then attempt to bind the free variables so that the instantiated
hypothesis is lhs.
For cases (2) and (3), the first instance found may ultimately fail because
the remaining hypotheses are not all relieved under the extended bindings. In
that case, should the attempt to relieve hypotheses fail, or should the search
continue to find other instances for (2) or (3)? The answer depends on which
of two options is in force for the so-called ``match-free'' of the rule.
Below we discuss how to specify these two options as ``:once'' or
``:all'' (the default), respectively.
Suppose that the original hypothesis is a call of force or case-split, where forcing is enabled (see enable-forcing) . Also
suppose that one of the following two cases applies: no instances are found for
(2) and also none for (3), or else the ``match-free'' option for the rule is
:all (as discussed below) and all attempts ultimately fail for (2)
and (3) (because the remaining hypotheses are not all relieved). Then the
current hypothesis is relieved but in the resulting split-off goals, all free
variables are bound to unusual names that call attention to this odd
situation.
Is it better to specify :once or :all? We believe that :all
is generally the better choice because of its greater power, provided the user
does not introduce a large number of rules with free variables, which has been
known to slow down the prover due to combinatorial explosion in the search
(Steps (2) and (3) above).
Either way, it is good practice to put the ``more substantial'' hypotheses
first, so that the most likely bindings of free variables will be found first
(in the case of :all) or found at all (in the case of :once). For
example, a rewrite rule like
(implies (and (p1 x y)
(p2 x y))
(equal (bar x) (bar-prime x)))
may never succeed if p1 is nonrecursive and enabled, since we may well
not find calls of p1 in the current context. If however p2 is
disabled or recursive, then the above rule may apply if the two hypotheses are
switched. For in that case, we can hope for a match of (p2 x y) in the
current context that therefore binds x and y; then the rewriter's
full power may be brought to bear to prove (p1 x y) for that x and
y.
Moreover, the ordering of hypotheses can affect the efficiency of the
rewriter. For example, the rule
(implies (and (rationalp y)
(foo x y))
(equal (bar x) (bar-prime x)))
may well be sub-optimal. Presumably the intention is to rewrite (bar
x) to (bar-prime x) in a context where (foo x y) is explicitly
known to be true for some rational number y. But y will be bound
first to the first term found in the current context that is known to
represent a rational number. If the 100th such y that is found is the
first one for which (foo x y) is known to be true, then wasted work will
have been done on behalf of the first 99 such terms y — unless
:once has been specified, in which case the rule will simply fail after
the first binding of y for which (rationalp y) is known to be true.
Thus, a better form of the above rule is almost certainly the following.
(implies (and (foo x y)
(rationalp y))
(equal (bar x) (bar-prime x)))
Specifying `once' or `all'.
As noted above, the following discussion applies only to rewrite,
linear, and forward-chaining rules. See free-variables-type-prescription for a discussion of analogous considerations
for type-prescription rules.
One method for specifying :once or :all for free-variable
matching is to provide the :match-free field of the :rule-classes of
the rule, for example, (:rewrite :match-free :all). See rule-classes. However, there are global events that can be used to specify
:once or :all; see set-match-free-default and see add-match-free-override. Here are some examples.
(set-match-free-default :once) ; future rules without a :match-free field
; are stored as :match-free :once (but this
; behavior is local to a book)
(add-match-free-override :once t) ; existing rules are treated as
; :match-free :once regardless of their
; original :match-free fields
(add-match-free-override :once (:rewrite foo) (:rewrite bar . 2))
; the two indicated rules are treated as
; :match-free :once regardless of their
; original :match-free fields
Some history. Before Version 2.7 the ACL2 rewriter performed Step
(2) above first. More significantly, it always acted as though :once had
been specified. That is, if Step (2) did not apply, then the rewriter took
the first binding it found using either Steps (1) or (3), in that order, and
proceeded to relieve the remaining hypotheses without trying any other
bindings of the free variables of that hypothesis.
Subtopics
- Add-match-free-override
- Set :match-free value to :once or :all in existing
rules
- Set-match-free-default
- Provide default for :match-free in future rules
- Free-variables-type-prescription
- Matching for free variable in type-prescription rules
- Set-match-free-error
- Control error vs. warning when :match-free is missing
- Free-variables-examples
- Examples pertaining to free variables in rules
