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 , where X is a set of generators and R is a set of relations giving the rewriting system. Suppose further that we have a well-ordering < 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 .

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 , 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₁,r₂, respectively. If , then we have an instance where confluence could fail. Hence, add the reduction 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 . 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) , (2) , and (3) .

First, we see an overlap of x in (1) and (3). Consider the word x³yxyxy. Reducing using (1), we get yxyxy. Reducing using (3), we get x². Hence, we get yxyxy = x², giving the reduction rule (4) .

Similarly, using the overlap of y in (2) and (3), we get the reduction (5) .

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

Next, consider the overlap of x of (1) and (5). Considering x³yxyx we get the rule yxyx = x²y², so we get the rule (6) . This obsoletes rule (4) and (5), so we remove them. Considering xyxyx³, we get xyxy = y²x², so we get the rule (7) .

Now, we are left with the rewriting system

• (1)
• (2)
• (6)
• (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.