An important case in
computational group theory is string rewriting systems which can be used to give canonical labels to elements or
cosets of a
finitely presented group as products of the
generators. This special case is the focus of this section.
Motivation in group theory The
critical pair lemma states that a term rewriting system is
locally confluent (or weakly confluent) if and only if all its
critical pairs are convergent. Furthermore, we have
Newman's lemma which states that if an (abstract) rewriting system is
strongly normalizing and weakly confluent, then the rewriting system is confluent. So, if we can add rules to the term rewriting system in order to force all critical pairs to be convergent while maintaining the strong normalizing property, then this will force the resultant rewriting system to be confluent. Consider a
finitely presented monoid M = \langle X \mid R \rangle where X is a finite set of generators and R is a set of defining relations on X. Let X* be the set of all words in X (i.e. the free monoid generated by X). Since the relations R generate an equivalence relation on X*, one can consider elements of M to be the equivalence classes of X* under R. For each class
{w1, w2, ... } it is desirable to choose a standard representative
wk. This representative is called the
canonical or
normal form for each word
wk in the class. If there is a computable method to determine for each
wk its normal form
wi then the word problem is easily solved. A confluent rewriting system allows one to do precisely this. Although the choice of a canonical form can theoretically be made in an arbitrary fashion this approach is generally not computable. (Consider that an equivalence relation on a language can produce an infinite number of infinite classes.) If the language is
well-ordered then the order B and A → B. Since W_1 > ... > W_n where W_n is irreducible under the rewriting system. However, depending on the rules that are applied at each Wi → Wi+1 it is possible to end up with two different irreducible reductions Wn ≠ W'm of W. However, if the rewriting system given by the relations is converted to a confluent rewriting system via the Knuth–Bendix algorithm, then all reductions are guaranteed to produce the same irreducible word, namely the normal form for that word.
Description of the algorithm for finitely presented monoids Suppose we are given a
presentation \langle X \mid R \rangle , where X is a set of
generators and R is a set of
relations giving the rewriting system. Suppose further that we have a reduction ordering among the words generated by X (e.g.,
shortlex order). For each relation P_i = Q_i in R , suppose Q_i . Thus we begin with the set of reductions P_i \rightarrow Q_i . First, if any relation P_i = Q_i can be reduced, replace P_i and Q_i with the reductions. Next, we add more reductions (that is, rewriting rules) to eliminate possible exceptions of confluence. Suppose that P_i and P_j overlap. • Case 1: either the prefix of P_i equals the suffix of P_j , or vice versa. In the former case, we can write P_i = BC and P_j = AB ; in the latter case, P_i = AB and P_j = BC . • Case 2: either P_i is completely contained in (surrounded by) P_j , or vice versa. In the former case, we can write P_i = B and P_j = ABC ; in the latter case, P_i = ABC and P_j = B . Reduce the word ABC using P_i first, then using P_j first. Call the results r_1, r_2 , respectively. If r_1 \neq r_2 , then we have an instance where confluence could fail. Hence, add the reduction \max r_1, r_2 \rightarrow \min r_1, r_2 to R . After adding a rule to R , remove any rules in R that might have reducible left sides (after checking if such rules have critical pairs with other rules). Repeat the procedure until all overlapping left sides have been checked.
Examples A terminating example Consider the monoid: : \langle x, y \mid x^3 = y^3 = (xy)^3 = 1 \rangle . We use the
shortlex order. This is an infinite monoid but nevertheless, the Knuth–Bendix algorithm is able to solve the word problem. Our beginning three reductions are therefore A suffix of x^3 (namely x) is a prefix of (xy)^3=xyxyxy, so consider the word x^3yxyxy . Reducing using (), we get yxyxy . Reducing using (), we get x^2 . Hence, we get yxyxy = x^2 , giving the reduction rule Similarly, using xyxyxy^3 and reducing using () and (), we get xyxyx = y^2 . Hence the reduction Both of these rules obsolete (), so we remove it. Next, consider x^3yxyx by overlapping () and (). Reducing we get yxyx = x^2y^2 , so we add the rule Considering xyxyx^3 by overlapping () and (), we get xyxy = y^2x^2 , so we add the rule These obsolete rules () and (), so we remove them. Now, we are left with the rewriting system Checking the overlaps of these rules, we find no potential failures of confluence. Therefore, we have a confluent rewriting system, and the algorithm terminates successfully.
A non-terminating example The order of the generators may crucially affect whether the Knuth–Bendix completion terminates. As an example, consider the
free Abelian group by the monoid presentation: : \langle x, y, x^{-1}, y^{-1}\, |\, xy=yx, xx^{-1} = x^{-1}x = yy^{-1} = y^{-1}y = 1 \rangle . The Knuth–Bendix completion with respect to lexicographic order x finishes with a convergent system, however considering the length-lexicographic order x it does not finish for there are no finite convergent systems compatible with this latter order. ==Generalizations==