The Knuth–Bendix completion algorithm (named after Donald Knuth and Peter Bendix[1]) is a semi-decision[2][3] algorithm for transforming a set of equations (over terms) into a confluent term rewriting system.
When the algorithm succeeds, it effectively solves the word problem for the specified algebra.
Although developed independently, it may also be seen as the instantiation of Knuth–Bendix algorithm in the theory of polynomial rings.
For example, if E = {1⋅x = x, x−1⋅x = 1, (x⋅y)⋅z = x⋅(y⋅z)} are the group axioms, the derivation chain demonstrates that a−1⋅(a⋅b) ⁎⟷E b is a member of E's deductive closure.
If R = { 1⋅x → x, x−1⋅x → 1, (x⋅y)⋅z → x⋅(y⋅z) } is a "rewrite rule" version of E, the derivation chains demonstrate that (a−1⋅a)⋅b ⁎⟶R∘⁎⟵R b is a member of R's deductive closure.
However, there is no way to derive a−1⋅(a⋅b) ⁎⟶R∘⁎⟵R b similar to above, since a right-to-left application of the rule (x⋅y)⋅z → x⋅(y⋅z) is not allowed.
The Knuth–Bendix algorithm takes a set E of equations between terms, and a reduction ordering (>) on the set of all terms, and attempts to construct a confluent and terminating term rewriting system R that has the same deductive closure as E. While proving consequences from E often requires human intuition, proving consequences from R does not.
For more details, see Confluence (abstract rewriting)#Motivating examples, which gives an example proof from group theory, performed both using E and using R. Given a set E of equations between terms, the following inference rules can be used to transform it into an equivalent convergent term rewrite system (if possible):[4][5] They are based on a user-given reduction ordering (>) on the set of all terms; it is lifted to a well-founded ordering (▻) on the set of rewrite rules by defining (s → t) ▻ (l → r) if The following example run, obtained from the E theorem prover, computes a completion of the (additive) group axioms as in Knuth, Bendix (1970).
The 10 starred equations turn out to constitute the resulting convergent rewrite system.
Critical pair computation is an instance of paramodulation for equational unit clauses.
"rw" is rewriting, implementing compose, collapse, and simplify.
An important case in computational group theory are string rewriting systems which can be used to give canonical labels to elements or cosets of a finitely presented group as products of the generators.
The critical pair lemma states that a term rewriting system is locally confluent (or weakly confluent) if and only if all its critical pairs are convergent.
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.
Since the relations R generate an equivalence relation on X*, one can consider elements of M to be the equivalence classes of X* under R. For each class {w1, w2, ... } it is desirable to choose a standard representative wk.
This representative is called the canonical or normal form for each word wk in the class.
If there is a computable method to determine for each wk its normal form wi then the word problem is easily solved.
Although the choice of a canonical form can theoretically be made in an arbitrary fashion this approach is generally not computable.
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 Wi → Wi+1 it is possible to end up with two different irreducible reductions Wn ≠ W'm 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.
Next, we add more reductions (that is, rewriting rules) to eliminate possible exceptions of confluence.
Repeat the procedure until all overlapping left sides have been checked.
This is an infinite monoid but nevertheless, the Knuth–Bendix algorithm is able to solve the word problem.
Now, we are left with the rewriting system Checking the overlaps of these rules, we find no potential failures of confluence.
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: The Knuth–Bendix completion with respect to lexicographic order
finishes with a convergent system, however considering the length-lexicographic order
it does not finish for there are no finite convergent systems compatible with this latter order.
[6] If Knuth–Bendix does not succeed, it will either run forever and produce successive approximations to an infinite complete system, or fail when it encounters an unorientable equation (i.e. an equation that it cannot turn into a rewrite rule).
An enhanced version will not fail on unorientable equations and produces a ground confluent system, providing a semi-algorithm for the word problem.