MAF : Background : Rewriting systems
## Rewriting systems

If *G* = ⟨ *X* | *R* ⟩ is a finitely presented monoid or group, *≤* is a partial ordering of *X*^{*}, and (*u,v*) ∈ *R* then *u*→*v* is a rewriting rule with respect to *≤* if *v* *<* *u*. If *r* is a rewriting rule, *u* is the left hand side or LHS of *r*, and *v* is the right hand side or RHS.

If *≤* is a total ordering then any element of *R* can be expressed as a rewriting rule, by interchanging *u* and *v* if necessary. A presentation of a group or monoid given in a form where all the relations take the form of rewriting rules (relative to an ordering *≤*) is called a rewriting system (for *G* over *≤*). Some authors regard the set *R* of rewriting rules on its own as constituting the rewriting system, because then one can consider the rewriting system independently of *G* and *≤*. However in MAF, the writing system is best viewed as the triple (*X*,*R*,≤).

If *u,v,a,b* ∈ *X*^{*},*u→v* ∈ *R* and *w = aub* then *w =*_{G} avb. Clearly *w* is a reducible word. Replacing *w* by *avb* is called rewriting *w*. It is possible that after doing so the rewritten *w* will still contain an LHS. If a word *q* can be obtained by rewriting another word *p* in one step we extend the notation *u*→*v* and write *p→q* to indicate this. If *q* can be obtained by a sequence of rewriting steps then we write *p→*q*. We can use the rewrite procedure, defined informally as "while *w* contains an LHS as a subword replace this LHS with the corresponding RHS", or "while *w = aub* with *u*→*v* ∈ *R* then rewrite *w* as *avb*" to try to find an irreducible word representing the same element as *w*. However, if *≤* is an arbitrary total ordering this procedure might not terminate. Termination is only guaranteed if *≤* is a reduction ordering. A word *w* is reducible or irreducible with respect to the rewriting system (*X*,*R*,≤) according to whether or not the rewrite procedure alters it. It is clear that a word that is reducible in this sense is also reducible in terms of our original non-constructive definition, but in general, a word that is irreducible with respect to a rewriting system might be still be reducible in the first sense.

In the "rewrite" procedure just given, we did not specify how to choose the rule to apply in the case where *w* contains more than one LHS. It is perfectly possible that the word we finish up with will be different according to the choice we make in such cases. If a rewriting system has the property that the final word is independent of any such choices then it said to be confluent. If a rewriting system is not confluent there must be some words *w,u,v* such that both *w→*u* and *w→*v* but there is no word *q* such that *u→*q* and *v→*q*. If this undesirable state of affairs arises then we can attempt to remedy it by adding either (*u*,*v*) or (*v*,*u*) to *R* as a new rewriting rule. It is clear that this does not change the congruence generated by *R*. Knuth-Bendix completion is the procedure which results when one attempts to systematically identify all such rules which might need to be added.

If (*u,v*) is a rule then it does not necessarily follow that *v* is a reduced word. A rewriting system is said to be reduced if for every rule *u* is minimally reducible (with respect to the current set of rules), and *v* is irreducible (with respect to the current rules). Any rewriting system can be modified so that all its rules are reduced.

The reduced confluent rewriting system for a group or monoid contains precisely the primary equations for that ordering of words in the group or monoid. It can correctly reduce all words, so that the words that are reducible by the rewriting system are precisely the reducible words in the original non-constructive definition, but words that are not minimally reducible may need to be reduced more than once.