LOOP-STOPPER

Major Section:  MISCELLANEOUS

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))),

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 repect 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, insted 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).