J. Symbolic Computation (1993) 16, 279–288 c ○ Acadenic Press Limited Term Rewrite Systems for Lattice Theory

It is shown that, even though there is a very well-behaved, natural normal form for lattice theory, there is no finite, convergent AC term rewrite system for the equational theory of all lattices. The study of the equational theory of a class K of algebras and their free algebras FK(X) is greatly facilitated by a normal form for the terms over the language of K. For terms u and v over some set of variables X, u is equivalent to v modulo K if the equation u ≈ v holds identically in K (i.e., for all substitutions of the variables into all algebras in K). We write this u ≈ v (mod K). By a normal form we mean an effective choice function from the equivalence classes of this relation. We will use the notation nf(w) forsucha normal form function. Having a normal form is equivalent to the equational theory being decidable. Moreover, if this normal form can be computed efficiently, it is very helpful for computer implementations of the free algebras in K. A term rewrite system, abbreviated TRS, constitutes a very specific method for transforming terms. A normal form TRS transforms terms into a unique normal form and, as such, is computationally useful. (The definitions will be given below.) Not every decidabl