16
D.W. LOVELAND
of equational theories permit computation of a complete set of
rewrite rules; that is, a set of rewrite rules sufficient to check the
truth of every equation of the tpeory by demand.ing that equal
terms reduce to the same normal form. The theory of groups is
one such theory while the theory of abelian groups is not. How-
ever, the problems of handling commutativity (and similar prob-
lems with associativity within some equational theories) have been
surmounted in limited cases by researchers such as Lankford and
Ballantyne, Huet and Peterson, Slagle, and Stickel. (For example,
see [Sl2],
[LBl].
[Hu2], [PSl].) A key idea here has been the use of
auxiliary equivalence classes; for example, one equatc;:s terms that
reduce to terms within the same equivalence class. An
unanswered question was (and is): what equational theories have
complete sets of rewrite rules? One faces both the problems of
finite termination of a sequence of .terms under rewrite transfor-
mations and, if termination occurs, whether a normal form is
reached whenever it should be. This problem has been investi-
gated by a number of people (see Huet and Oppen [HOl] for a
technical overview). This approach has been integrated with reso-
lution (see Slagle [Sll],[Sl2]).
A research area very close to rewrite (or reduction) systems is
that of special unification algorithms. As previously mentioned,
unification is the name J.A. Robinson gave to the process for
finding a most general substitution for variables to make atomic
formulas identical. Special unification also seeks to "unify"
atomic formulas, but within special theories, usually equational
theories. The usual unification process is augmented by equations
or rewrite rules in such a manner as to make unnecessary the
explicit listing of the equations as axioms. This idea was first for-
malized in Plotkin [Pl2] to deal with general equational theories.
Equational theories with commutative and/or associative
Previous Page Next Page