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

.