                                              Notes prepared by
                                                 Stanley Burris
                                                   July 3, 2001

Equational Term Rewrite Systems (ETRS’s)

In Chapter III of LMCS we looked at the fundamental notion of a term rewrite system, and the Knuth-Bendix procedure based on the critical pairs lemma. The difficulties encountered in trying to automate equational theorem proving has given a major boost to the study of TRS’s as one of the most promising methods to handle equality. Initial work was with group-like equations. However not many equational systems can be fully converted into TRS’s, so some of the more recent work has been directed towards equational term rewrite systems (ETRS’s).

DEFINITION 1 An equational term rewrite system (ETRS) is an ordered pair (E_{0}, R) where E_{0} is a set of equations and a R is a TRS.

When the E_{0} has been specified then one refers to R as an E_{0}-TRS.

DEFINITION 2 Given an ETRS (E_{0}, R), let ≡ be the congruence on the term algebra associated with E_{0}, i.e., s ≡ t iff E_{0} ⊧ s ≈ t. Let ⟶_{R/E_{0}} be the composition ≡ ∘ ⟶_{R} ∘ ≡. Then the ETRS (E_{0}, R) is a normal form ETRS if

(a) the relation ⟶_{R/E_{0}} is terminating (i.e., well-founded), and

(b) for every term s, all terminating sequences s ⟶_{R/E_{0}} ⋯ terminate in the same coset N(s) of ≡, the normal form coset of s.

When working with ETRS’s the objective is, for a given set of equations E, to select a “nice” subset E_{0} of E such that one has a normal form E_{0}-TRS R with the crucial property that

E ⊧ s ≈ t ⟺ N(s) = N(t).

Of course one wants a good algorithm to determine when the latter holds. There is very interesting work with rings, where E_{0} consists of some associative and/or commutative laws.

Now let us look at some simple examples of normal form ETRS’s for groups. Because of the popularity of the associative, resp. commutative, laws they are labelled A, resp. C, when referred to in the literature on ETRS’s.

EXAMPLE 3 A normal form A-TRS for groups:

\begin{matrix}e^{−1} & ⟶ & e \\ x · e & ⟶ & x \\ e · x & ⟶ & x \\ (x^{−1})^{−1} & ⟶ & x \\ x^{−1} · x & ⟶ & e \\ x · x^{−1} & ⟶ & e \\ (x · y)^{−1} & ⟶ & y^{−1} · x^{−1}. \end{matrix}

EXAMPLE 4 A normal form C-TRS for commutative groups:

\begin{matrix}e^{−1} & ⟶ & e \\ x · e & ⟶ & x \\ (x^{−1})^{−1} & ⟶ & x \\ x^{−1} · x & ⟶ & e \\ x^{−1} · (x · y) & ⟶ & y \\ x · (x^{−1} · y) & ⟶ & y \\ (x · y)^{−1} & ⟶ & y^{−1} · x^{−1} \\ (x · y) · z & ⟶ & x · (y · z). \end{matrix}

EXAMPLE 5 A normal form AC-TRS for commutative groups:

\begin{matrix}e^{−1} & ⟶ & e \\ x · e & ⟶ & x \\ (x^{−1})^{−1} & ⟶ & x \\ x^{−1} · x & ⟶ & e \\ (x · y)^{−1} & ⟶ & y^{−1} · x^{−1}. \end{matrix}

DEFINITION 6 An ETRS (E_{0}, R) is reduced if for s ⟶ t ∈ R, no rule in ≡ ∘(R \ {s ⟶ t})∘ ≡ can be applied to either s or t.

Note that the examples above are reduced. Here is some further reading.

• Rolf Socher-Ambrosius proves that Boolean algebras do not have a normal form AC-TRS in Boolean algebra admits no convergent term rewriting system, Springer Lecture Notes in Computer Science 488, RTA ’91.

• Burris and Lawrence investigate the possibility of finding an AC-TRS for finitely many finite fields, or equivalently, for discriminator varieties of rings, in Term rewrite rules for finite fields, International J. of Algebra and Computation 1 (1991), 353–369.

• Freese Jezek, and Nation prove that lattices do not have a normal form AC-TRS in Term rewrite systems for lattice theory, J. Symbolic Computation (1993) 16, 279–288.

Exercises

Since there are two binary operations in rings, we need to specify just which A and C laws for which operations are to go into E_{0}.

Problem 1 Let an AC denote A for + and × ; C for +. Find a reduced normal form AC-TRS for rings.

For the remainder of the problems on rings AC denotes A and C for both + and × . (We are working with commutative rings in each case).

Problem 2 Find a reduced normal form AC-TRS for commutative rings.

Problem 3 Find a reduced normal form AC-TRS for the equational theory of GF(p), p a prime, using the language {+, ×, −, 0, 1} of rings.

Problem 4 Find a reduced normal form AC-TRS for the equational theory of GF(p^{n}).

Problem 5 Find a reduced normal form AC-TRS for the equational theory of GF(p), GF(q) where p, q are distinct primes.

For distributive lattices (D, ∨, ∧) we take AC to refer to the associative and commutative laws for both operations.

Problem 6 Find a reduced normal form AC-TRS for distributive lattices.