Editing Knuth–Bendix completion algorithm (section)

===Examples===

==== A terminating example ====
Consider the monoid: 
:<math> \langle x, y \mid x^3 = y^3 = (xy)^3 = 1 \rangle </math>.  
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
{{NumBlk|:|<math> x^3 \rightarrow 1 </math>|{{EquationRef|1}}}} 
{{NumBlk|:|<math> y^3 \rightarrow 1 </math>|{{EquationRef|2}}}}

{{NumBlk|:|<math> (xy)^3 \rightarrow 1 </math>.|{{EquationRef|3}}}}

A suffix of <math>x^3</math> (namely <math>x</math>) is a prefix of <math>(xy)^3=xyxyxy</math>, so consider the word <math> x^3yxyxy </math>.  Reducing using ({{EquationNote|1}}), we get <math> yxyxy </math>.  Reducing using ({{EquationNote|3}}), we get <math> x^2 </math>.  Hence, we get <math> yxyxy = x^2 </math>, giving the reduction rule

{{NumBlk|:|<math> yxyxy \rightarrow x^2 </math>.|{{EquationRef|4}}}}

Similarly, using <math> xyxyxy^3 </math> and reducing using ({{EquationNote|2}}) and ({{EquationNote|3}}), we get <math> xyxyx = y^2 </math>.  Hence the reduction

{{NumBlk|:|<math> xyxyx \rightarrow y^2 </math>.|{{EquationRef|5}}}}

Both of these rules obsolete ({{EquationNote|3}}), so we remove it.

Next, consider <math> x^3yxyx </math> by overlapping ({{EquationNote|1}}) and ({{EquationNote|5}}). Reducing we get <math> yxyx = x^2y^2 </math>, so we add the rule

{{NumBlk|:|<math> yxyx \rightarrow x^2y^2</math>.|{{EquationRef|6}}}}
Considering <math> xyxyx^3 </math> by overlapping ({{EquationNote|1}}) and ({{EquationNote|5}}), we get <math> xyxy = y^2x^2 </math>, so we add the rule

{{NumBlk|:|<math> y^2x^2 \rightarrow xyxy </math>.|{{EquationRef|7}}}}
These obsolete rules ({{EquationNote|4}}) and ({{EquationNote|5}}), so we remove them.

Now, we are left with the rewriting system
{{NumBlk|:|<math> x^3 \rightarrow 1 </math>|({{EquationNote|1}})|RawN=.}}
{{NumBlk|:|<math> y^3 \rightarrow 1 </math>|({{EquationNote|2}})|RawN=.}}

{{NumBlk|:|<math> yxyx \rightarrow x^2y^2 </math>|({{EquationNote|6}})|RawN=.}}
{{NumBlk|:|<math> y^2 x^2 \rightarrow xyxy </math>.|({{EquationNote|7}})|RawN=.}}

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:

: <math>\langle x, y, x^{-1}, y^{-1}\, |\, xy=yx, xx^{-1} = x^{-1}x = yy^{-1} = y^{-1}y = 1 \rangle  .</math>

The Knuth–Bendix completion with respect to lexicographic order <math>x < x^{-1} < y < y^ {-1}</math> finishes with a convergent system, however considering the length-lexicographic order <math>x < y < x^{-1} < y^{-1}</math> it does not finish for there are no finite convergent systems compatible with this latter order.<ref name="BogopolskiBumagin2011">{{cite book |editor=Oleg Bogopolski |editor2=Inna Bumagin |editor3=Olga Kharlampovich |editor4=Enric Ventura|title=Combinatorial and Geometric Group Theory: Dortmund and Ottawa-Montreal conferences|year=2011|publisher=Springer Science & Business Media|isbn=978-3-7643-9911-5|page=62|chapter=Geodesic Rewriting Systems and Pregroups|author=V. Diekert |author2=A.J. Duncan |author3=A.G. Myasnikov}}</ref>