- Knuth-Bendix completion algorithm
The Knuth-Bendix completion algorithm is an
algorithm for transforming a set ofequation s (overterms ) into a confluentterm rewriting system . When the algorithm succeeds, it has effectively solved the word problem for the specifiedalgebra .An important case in
computational group theory are 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 current focus of this article.Motivation in group theory
The
critical pair lemma states that a term rewriting system is weakly confluent if and only if the critical pairs are convergent. Furthermore, we haveNewman'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 = < X | R > 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 define 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 < gives a consistent method for defining minimal representatives, however computing these representatives may still not be possible. In particular, if a rewriting system is used to calculate minimal representatives then the order < should also have the property:: A < B -> XAY < XBY for all words A,B,X,Y
This property is called translation invariance. An order that is both translation-invariant and a well-order is called a reduction order.
From the presentation of the monoid it is possible to define a rewriting system given by the relations R. If A x B is in R then either A < B in which case B -> A is a rule in the rewriting system, otherwise A > B and A -> B. Since < is a reduction order a given word W can be reduced W > 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 e 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 angle , 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 . For each relation P_i = Q_i in R , suppose Q_i < P_i . Thus we begin with the set of reductions P_i ightarrow 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 , where i eq j , overlap. That is, 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, P_j = AB ; in the latter case, P_i = AB, P_j = BC .
Reduce the word ABC using P_i first, then using P_j first. Call the results r_1, r_2 , respectively. If r_1 eq r_2 , then we have an instance where confluence could fail. Hence, add the reduction max r_1, r_2 ightarrow min r_1, r_2 to R .
After adding a rule to R , remove any rules in R that might have reducible left sides.
Repeat the procedure until all overlapping left sides have been checked.
Example
Consider the presentation x, y mid x^3 = y^3 = (xy)^3 = 1 } . We use the
shortlex order . In fact, this is an infinite group. Nevertheless, the Knuth-Bendix algorithm is able to solve the word problem.Our beginning three reductions are therefore (1) x^3 ightarrow 1 , (2) y^3 ightarrow 1 , and (3) xy)^3 ightarrow 1 .
First, we see an overlap of x in (1) and (3). Consider the word x^3yxyxy . Reducing using (1), we get yxyxy . Reducing using (3), we get x^2 . Hence, we get yxyxy = x^2 , giving the reduction rule (4) yxyxy ightarrow x^2 .
Similarly, using the overlap of y in (2) and (3), we get the reduction (5) xyxyx ightarrow y^2 .
Both of these rules obsolete (3), so we remove it.
Next, consider the overlap of x of (1) and (5). Considering x^3yxyx we get yxyx = x^2y^2 , so we add the rule (6) yxyx ightarrow x^2y^2. This obsoletes rules (4) and (5), so we remove them. Considering xyxyx^3 , we get xyxy = y^2x^2 , so we add the rule (7) y^2x^2 ightarrow xyxy .
Now, we are left with the rewriting system
* (1) x^3 ightarrow 1
* (2) y^3 ightarrow 1
* (6) yxyx ightarrow x^2y^2
* (7) y^2 x^2 ightarrow xyxy 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.Generalizations
If Knuth-Bendix does not succeed, it will either run forever, or fail when it encounters an unorientable equation (i.e. an equation that it cannot turn into a rewrite rule). The enhanced
completion without failure will not fail on unorientable equations and provides asemi-decision procedure for the word problem.References
* D. Knuth and P. Bendix. "Simple word problems in universal algebras." "Computational Problems in Abstract Algebra" (Ed. J. Leech) pages 263--297, 1970.
* C. Sims. 'Computations with finitely presented groups.' Cambridge, 1994.External links
*
Wikimedia Foundation. 2010.