Filter
Top Products
76 CHAPTER 9. DERIVED RULES
The HOL Light approach to permutative rewrite rules has long been used in
the Boyer-Moore theorem prover, and more recently in Isabelle thanks to Tobias
Nipkow. They are only applied if, after instantiation, the left-hand side is “larger”
than the right according to some well-founded ordering. The basic building block is
ORDERED_REWR_CONV. This calls REWR_CONV, but will then force failure unless in the
resulting theorem Γ s
= t
one has t
> s
according to the given ordering > on
terms. In this way, one can rewrite freely with a theorem such as x + y = y + x
without fear of infinite looping.
However in conjunction with other rewrites, infinite looping can reappear. For
example, rewriting with the above commutative law and the associative law (x +
y) + z = x + (y + z) one could still have an infinite rewrite:
x + (y + z) −→ (y + z) + x
−→ y + (z + x)
−→ (z + x) + y
−→ z + (x + y)
−→ (x + y) + z
−→ x + (y + z)
This, however, can be prevented by a suitable choice of ordering. In fact, given
the right ordering, the associative and commutative laws together not only always
terminate, but actually reduce AC combinations to their canonical form. Martin
and Nipkow (1990) give a slightly tricky ordering that makes the associative and
commutative laws alone give a normalizer. However a more obvious approach is to
add a third theorem, easily derived from the other two: x +(y + z) = y + (x +z).
Now, suppose that the ordering has the following properties for any terms x, y and
z:
(x + y) + z > x + (y + z)
x + y > y + x iff x > y
x + (y + z) > y + (x + z) iff x > y
Such an ordering, if it is also monotonic (if s > t then u[s] > u[t]) and total and
is wellfounded on ground terms, is said to be AC-compatible. Intuitively it is clear
that ordered rewriting with these theorems will canonicalize AC combinations by
‘bubbling’ terms in iterated additions to their proper place. Theorems in this class
for some associative and commutative operators are built into HOL, e.g.
#ADD_AC;;
it : thm =
|- (m + n = n + m) /\ ((m + n) + p = m + n + p) /\ (m + n + p = n + m + p)
#MULT_AC;;
it : thm =
|- (m * n = n * m) /\ ((m * n) * p = m * n * p) /\ (m * n * p = n * m * p)
#REWRITE_CONV[ADD_AC; MULT_AC] ‘x * y + z * x + w * x + x * w =
x * w + x * z + y * x + x * w‘;;
it : thm =
|- (x * y + z * x + w * x + x * w = x * w + x * z + y * x + x * w) = T
Martin and Nipkow (1990) show that one can also add laws of left and right
distributivity for + and ∗, as well as idempotence laws x+x = x and x+(x+y) =
x+y and get canonicalizers under these laws too. (For example, if + is conjunction
or disjunction.)