Knuth-Bendix completion algorithm

The Knuth-Bendix completion algorithm is an algorithm for transforming a set of equations (over terms) into a confluent term rewriting system. When the algorithm succeeds, it has effectively solved the word problem for the specified algebra. Hence, it can also be used to solve the coset enumeration problem. The word problem is, in general, undecidable, hence the algorithm cannot always terminate successfully. If it 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 a semi-decision procedure for the word problem.

Description of the algorithm

Suppose we are given a presentation <math> \langle X \mid R \rangle <math>, where <math> X <math> is a set of generators and <math> R <math> is a set of relations giving the rewriting system. Suppose further that we have a well-ordering <math> < <math> among the words generated by <math> X <math>. For each relation <math> P_i = Q_i <math> in <math> R <math>, suppose <math> Q_i < P_i <math>. Thus we begin with the set of reductions <math> P_i \rightarrow Q_i <math>.

First, if any relation <math> P_i = Q_i <math> can be reduced, replace <math> P_i <math> and <math> Q_i <math> with the reductions.

Next, we add more reductions (that is, rewriting rules) to eliminate possible exceptions of confluence. Suppose that <math> P_i <math> and <math> P_j <math>, where <math> i \neq j <math>, overlap. That is, either the prefix of <math> P_i<math> equals the suffix of <math> P_j <math>, or vice versa. In the former case, we can write <math> P_i = BC, P_j = AB <math>; in the latter case, <math> P_i = AB, P_j = BC <math>.

Reduce the word <math> ABC <math> using <math> P_i <math> first, then using <math> P_j <math> first. Call the results <math> r_1, r_2 <math>, respectively. If <math> r_1 \neq r_2 <math>, then we have an instance where confluence could fail. Hence, add the reduction <math> \max r_1, r_2 \rightarrow \min r_1, r_2 <math> to <math> R <math>.

After adding a rule to <math> R <math>, remove any rules in <math> R <math> that might have reducible left sides.

Repeat the procedure until all overlapping left sides have been checked.

Example

Consider the presentation <math> \{ x, y \mid x^3 = y^3 = (xy)^3 = 1 \} <math>. We use the lexicographic ordering. 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) <math> x^3 \rightarrow 1 <math>, (2) <math> y^3 \rightarrow 1 <math>, and (3) <math> (xy)^3 \rightarrow 1 <math>.

First, we see an overlap of <math> x <math> in (1) and (3). Consider the word <math> x^3yxyxy <math>. Reducing using (1), we get <math> yxyxy <math>. Reducing using (3), we get <math> x^2 <math>. Hence, we get <math> yxyxy = x^2 <math>, giving the reduction rule (4) <math> yxyxy \rightarrow x^2 <math>.

Similarly, using the overlap of <math> y <math> in (2) and (3), we get the reduction (5) <math> xyxyx \rightarrow y^2 <math>.

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

Next, consider the overlap of <math> x <math> of (1) and (5). Considering <math> x^3yxyx <math> we get the rule <math> yxyx = x^2y^2 <math>, so we get the rule (6) <math> yxyx \rightarrow x^2y^2<math>. This obsoletes rule (4) and (5), so we remove them. Considering <math> xyxyx^3 <math>, we get <math> xyxy = y^2x^2 <math>, so we get the rule (7) <math> y^2x^2 \rightarrow xyxy <math>.

Now, we are left with the rewriting system

• (1) <math> x^3 \rightarrow 1 <math>
• (2) <math> y^3 \rightarrow 1 <math>
• (6) <math> yxyx \rightarrow x^2y^2 <math>
• (7) <math> y^2 x^2 \rightarrow xyxy <math>

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.