Knuth–Bendix completion algorithm

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 ${\displaystyle 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 {w₁, w₂, ... } it is desirable to choose a standard representative w_k. This representative is called the canonical or normal form for each word w_k in the class. If there is a computable method to determine for each w_k its normal form w_i 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 W_i → W_i+1 it is possible to end up with two different irreducible reductions W_n ≠ 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.

Suppose we are given a presentation ${\displaystyle \langle X\mid R\rangle }$, where ${\displaystyle X}$ is a set of generators and ${\displaystyle R}$ is a set of relations giving the rewriting system. Suppose further that we have a reduction ordering ${\displaystyle <}$ among the words generated by ${\displaystyle X}$(e.g., shortlex order). For each relation ${\displaystyle P_{i}=Q_{i}}$ in ${\displaystyle R}$, suppose ${\displaystyle Q_{i}<P_{i}}$. Thus we begin with the set of reductions ${\displaystyle P_{i}\rightarrow Q_{i}}$.

First, if any relation ${\displaystyle P_{i}=Q_{i}}$ can be reduced, replace ${\displaystyle P_{i}}$ and ${\displaystyle Q_{i}}$ with the reductions.

Next, we add more reductions (that is, rewriting rules) to eliminate possible exceptions of confluence. Suppose that ${\displaystyle P_{i}}$ and ${\displaystyle P_{j}}$ overlap.

1. Case 1: either the prefix of ${\displaystyle P_{i}}$ equals the suffix of ${\displaystyle P_{j}}$, or vice versa. In the former case, we can write ${\displaystyle P_{i}=BC}$ and ${\displaystyle P_{j}=AB}$; in the latter case, ${\displaystyle P_{i}=AB}$ and ${\displaystyle P_{j}=BC}$.
2. Case 2: either ${\displaystyle P_{i}}$ is completely contained in (surrounded by) ${\displaystyle P_{j}}$, or vice versa. In the former case, we can write ${\displaystyle P_{i}=B}$ and ${\displaystyle P_{j}=ABC}$; in the latter case, ${\displaystyle P_{i}=ABC}$ and ${\displaystyle P_{j}=B}$.

Reduce the word ${\displaystyle ABC}$ using ${\displaystyle P_{i}}$ first, then using ${\displaystyle P_{j}}$ first. Call the results ${\displaystyle r_{1},r_{2}}$, respectively. If ${\displaystyle r_{1}\neq r_{2}}$, then we have an instance where confluence could fail. Hence, add the reduction ${\displaystyle \max r_{1},r_{2}\rightarrow \min r_{1},r_{2}}$ to ${\displaystyle R}$.

After adding a rule to ${\displaystyle R}$, remove any rules in ${\displaystyle 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.

Consider the monoid:

${\displaystyle \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

${\displaystyle x^{3}\rightarrow 1}$

(1)

${\displaystyle y^{3}\rightarrow 1}$

(2)

${\displaystyle (xy)^{3}\rightarrow 1}$.

(3)

A suffix of ${\displaystyle x^{3}}$ (namely ${\displaystyle x}$) is a prefix of ${\displaystyle (xy)^{3}=xyxyxy}$, so consider the word ${\displaystyle x^{3}yxyxy}$. Reducing using (1), we get ${\displaystyle yxyxy}$. Reducing using (3), we get ${\displaystyle x^{2}}$. Hence, we get ${\displaystyle yxyxy=x^{2}}$, giving the reduction rule

${\displaystyle yxyxy\rightarrow x^{2}}$.

(4)

Similarly, using ${\displaystyle xyxyxy^{3}}$ and reducing using (2) and (3), we get ${\displaystyle xyxyx=y^{2}}$. Hence the reduction

${\displaystyle xyxyx\rightarrow y^{2}}$.

(5)

Both of these rules obsolete (3), so we remove it.

Next, consider ${\displaystyle x^{3}yxyx}$ by overlapping (1) and (5). Reducing we get ${\displaystyle yxyx=x^{2}y^{2}}$, so we add the rule

${\displaystyle yxyx\rightarrow x^{2}y^{2}}$.

(6)

Considering ${\displaystyle xyxyx^{3}}$ by overlapping (1) and (5), we get ${\displaystyle xyxy=y^{2}x^{2}}$, so we add the rule

${\displaystyle y^{2}x^{2}\rightarrow xyxy}$.

(7)

These obsolete rules (4) and (5), so we remove them.

Now, we are left with the rewriting system

${\displaystyle x^{3}\rightarrow 1}$

(1)

${\displaystyle y^{3}\rightarrow 1}$

(2)

${\displaystyle yxyx\rightarrow x^{2}y^{2}}$

(6)

${\displaystyle y^{2}x^{2}\rightarrow xyxy}$.

(7)

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.

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:

${\displaystyle \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 ${\displaystyle x<x^{-1}<y<y^{-1}}$ finishes with a convergent system, however considering the length-lexicographic order ${\displaystyle x<y<x^{-1}<y^{-1}}$ it does not finish for there are no finite convergent systems compatible with this latter order.[6]