Loop-stopper
Limit application of permutative rewrite rules
See rule-classes for a discussion of the syntax of the
:loop-stopper field of :rewrite rule-classes. Here we
describe how that field is used, and also how that field is created when the
user does not explicitly supply it.
For example, the built-in :rewrite rule
commutativity-of-+,
(implies (and (acl2-numberp x)
(acl2-numberp y))
(equal (+ x y) (+ y x))),
creates a rewrite rule with a loop-stopper of ((x y binary-+)). This
means, very roughly, that the term corresponding to y must be ``smaller''
than the term corresponding to x in order for this rule to apply.
However, the presence of binary-+ in the list means that certain
functions that are ``invisible'' with respect to binary-+ (by default,
unary-- is the only such function) are more or less ignored when
making this ``smaller'' test. We are much more precise below.
Our explanation of loop-stopping is in four parts. First we discuss ACL2's
notion of ``term order.'' Next, we bring in the notion of ``invisibility'',
and use it together with term order to define orderings on terms that are used
in the loop-stopping algorithm. Third, we describe that algorithm. These
topics all assume that we have in hand the :loop-stopper field of a given
rewrite rule; the fourth and final topic describes how that field is
calculated when it is not supplied by the user.
ACL2 must sometimes decide which of two terms is syntactically simpler. It
uses a total ordering on terms, called the ``term order.'' Under this
ordering constants such as '(a b c) are simpler than terms containing
variables such as x and (+ 1 x). Terms containing variables are
ordered according to how many occurrences of variables there are. Thus x
and (+ 1 x) are both simpler than (cons x x) and (+ x y). If
variable counts do not decide the order, then the number of function
applications are tried. Thus (cons x x) is simpler than (+ x (+ 1
y)) because the latter has one more function application. Finally, if the
number of function applications do not decide the order, a lexicographic
ordering on Lisp objects is used. See term-order for details.
When the loop-stopping algorithm is controlling the use of permutative
:rewrite rules it allows term1 to be moved leftward over
term2 only if term1 is smaller, in a suitable sense. Note: The
sense used in loop-stopping is not the above explained term order but a
more complicated ordering described below. The use of a total ordering stops
rules like commutativity from looping indefinitely because it allows (+ b
a) to be permuted to (+ a b) but not vice versa, assuming a is
smaller than b in the ordering. Given a set of permutative rules that
allows arbitrary permutations of the tips of a tree of function calls, this
will normalize the tree so that the smallest argument is leftmost and the
arguments ascend in the order toward the right. Thus, for example, if the
same argument appears twice in the tree, as x does in the binary-+ tree denoted by the term (+ a x b x), then when the allowed
permutations are done, all occurrences of the duplicated argument in the tree
will be adjacent, e.g., the tree above will be normalized to (+ a b x
x).
Suppose the loop-stopping algorithm used term order, as noted above, and
consider the binary-+ tree denoted by (+ x y (- x)). The
arguments here are in ascending term order already. Thus, no permutative
rules are applied. But because we are inside a +-expression it is very
convenient if x and (- x) could be given virtually the same position
in the ordering so that y is not allowed to separate them. This would
allow such rules as (+ i (- i) j) = j to be applied. In support of this,
the ordering used in the control of permutative rules allows certain unary
functions, e.g., the unary minus function above, to be ``invisible'' with
respect to certain ``surrounding'' functions, e.g., + function
above.
Briefly, a unary function symbol fn1 is invisible with respect to a
function symbol fn2 if fn2 belongs to the value of fn1 in
invisible-fns-table; also see set-invisible-fns-table, which
explains its format and how it can be set by the user. Roughly speaking,
``invisible'' function symbols are ignored for the purposes of the term-order
test.
Consider the example above, (+ x y (- x)). The translated version of
this term is (binary-+ x (binary-+ y (unary-- x))). The initial invisible-fns-table makes unary-- invisible with respect to binary-+. The commutativity rule for binary-+ will attempt to swap
y and (unary-- x) and the loop-stopping algorithm is called to
approve or disapprove. If term order is used, the swap will be disapproved.
But term order is not used. While the loop-stopping algorithm is permuting
arguments inside a binary-+ expression, unary-- is invisible.
Thus, instead of comparing y with (unary-- x), the loop-stopping
algorithm compares y with x, approving the swap because x comes
before y.
Here is a more precise specification of the total order used for
loop-stopping with respect to a list, fns, of functions that are to be
considered invisible. Let x and y be distinct terms; we specify
when ``x is smaller than y with respect to fns.'' If x is
the application of a unary function symbol that belongs to fns, replace
x by its argument. Repeat this process until the result is not the
application of such a function; let us call the result x-guts. Similarly
obtain y-guts from y. Now if x-guts is the same term as
y-guts, then x is smaller than y in this order iff x is
smaller than y in the standard term order. On the other hand, if
x-guts is different than y-guts, then x is smaller than y
in this order iff x-guts is smaller than y-guts in the standard term
order.
Now we may describe the loop-stopping algorithm. Consider a rewrite rule
with conclusion (equiv lhs rhs) that applies to a term x in a given
context; see rewrite. Suppose that this rewrite rule has a
loop-stopper field (technically, the :heuristic-info field) of ((x1 y1
. fns-1) ... (xn yn . fns-n)). (Note that this field can be observed by
using the command :pr with the name of the rule; see pr.)
We describe when rewriting is permitted. The simplest case is when the
loop-stopper list is nil (i.e., n is 0); in that case,
rewriting is permitted. Otherwise, for each i from 1 to n let
xi' be the actual term corresponding to the variable xi when
lhs is matched against the term to be rewritten, and similarly correspond
yi' with y. If xi' and yi' are the same term for all
i, then rewriting is not permitted. Otherwise, let k be the least
i such that xi' and yi' are distinct. Let fns be the list
of all functions that are invisible with respect to every function in
fns-k, if fns-k is non-empty; otherwise, let fns be nil.
Then rewriting is permitted if and only if yi' is smaller than xi'
with respect to fns, in the sense defined in the preceding paragraph.
It remains only to describe how the loop-stopper field is calculated for a
rewrite rule when this field is not supplied by the user. (On the other hand,
to see how the user may specify the :loop-stopper, see rule-classes.) Suppose the conclusion of the rule is of the form (equiv
lhs rhs). First of all, if rhs is not an instance of the left hand
side by a substitution whose range is a list of distinct variables, then the
loop-stopper field is nil. Otherwise, consider all pairs (u . v)
from this substitution with the property that the first occurrence of v
appears in front of the first occurrence of u in the print representation
of rhs. For each such u and v, form a list fns of all
functions fn in lhs with the property that u or v (or
both) appears as a top-level argument of a subterm of lhs with function
symbol fn. Then the loop-stopper for this rewrite rule is a list of all
lists (u v . fns).
Remark. The paragraph above mentions ``the conclusion of the rule''
as (equiv lhs rhs). The rule's conclusion is actually produced from a
naive version (equiv lhs0 rhs) of the conclusion by expanding away all
lambda applications in lhs0. If lhs0 and lhs are
distinct (i.e., if there is any such lambda expansion) and also the
loop-stopper field is calculated as nil as described above, then a second
attempt to calculate the loop-stopper is made using lhs0 in place of
lhs.
Subtopics
- Invisible-fns-table
- Functions that are invisible to the loop-stopper algorithm
- Set-invisible-fns-table
- Set the invisible functions table
- Add-invisible-fns
- Make some unary functions invisible to the loop-stopper
algorithm
- Remove-invisible-fns
- Make some unary functions no longer invisible
