Report Number: CS-TR-80-785
Institution: Stanford University, Department of Computer Science
Title: Equations and rewrite rules: a survey
Author: Huet, Gerard
Author: Oppen, Derek C.
Date: January 1980
Abstract: Equations occur frequently in mathematics, logic and computer
science. In this paper, we survey the main results concerning
equations, and the methods available for reasoning about them
and computing with them. The survey is self-contained and
unified, using traditional abstract algebra.
Reasoning about equations may involve deciding if an equation
follows from a given set of equations (axioms), or if an
equation is true in a given theory. When used in this manner,
equations state properties that hold between objects.
Equations may also be used as definitions; this use is well
known in computer science: programs written in applicative
languages, abstract interpreter definitions, and algebraic
data type definitions are clearly of this nature. When these
equations are regarded as oriented "rewrite rules," we may
actually use them to compute.
In addition to covering these topics, we discuss the problem
of "solving" equations (the "unification" problem), the
problem of proving termination of sets of rewrite rules, and
the decidability and complexity of word problems and of
combinations of equational theories. We restrict ourselves to
first-order equations, and do not treat equations which
define non-terminating computations or recent work on rewrite
rules applied to equational congruence classes.