Editing Knuth–Bendix completion algorithm (section)

=== Motivation in group theory ===
The [[critical pair lemma]] states that a term rewriting system is [[confluence (term rewriting)|locally confluent]] (or weakly confluent) if and only if all its [[critical pair (logic)|critical pairs]] are convergent. Furthermore, we have [[Newman's lemma]] which states that if an (abstract) rewriting system is [[normal form (term rewriting)|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]] <math>M = \langle X \mid R \rangle</math> where X is a finite set of generators and R is a set of defining relations on X.  Let X<sup>*</sup> 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<sup>*</sup> under R.  For each class ''{w<sub>1</sub>, w<sub>2</sub>, ... }'' it is desirable to choose a standard representative ''w<sub>k</sub>''.  This representative is called the '''canonical''' or '''normal form''' for each word ''w<sub>k</sub>'' in the class.  If there is a computable method to determine for each ''w<sub>k</sub>'' its normal form ''w<sub>i</sub>'' 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&nbsp;<&nbsp;B in which case B&nbsp;→&nbsp;A is a rule in the rewriting system, otherwise A&nbsp;>&nbsp;B and A&nbsp;→&nbsp;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<sub>i</sub>&nbsp;→&nbsp;W<sub>i+1</sub> it is possible to end up with two different irreducible reductions W<sub>n</sub>&nbsp;≠&nbsp;W'<sub>m</sub> 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.