Knuth-Bendix completion algorithm
Encyclopedia
The Knuth–Bendix completion algorithm (named after Donald Knuth and Peter Bendix) is an algorithm
for transforming a set of equation
s (over terms
) into a confluent
term rewriting system. When the algorithm succeeds, it has effectively solved the word problem
for the specified algebra
.
An important case in computational group theory
are string rewriting systems which can be used to give canonical labels to elements or coset
s of a finitely presented group as products of the generators. This special case is the current focus of this article.
(or weakly confluent) if and only if the critical pairs are convergent. Furthermore, we have Newman's lemma
which states that if an (abstract) rewriting system is 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
where X is a finite set of generators and R is a set of defining relations on X. Let X* be the set of all words in X (i.e. the free monoid generated by X). Since the relations R define 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. 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:
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 < B in which case B → A is a rule in the rewriting system, otherwise A > B and A → 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 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.
, where 
is a set of generator
s and
is a set of relations
giving the rewriting system. Suppose further that we have a reduction ordering
among the words generated by 
. For each relation 
in 
, suppose 
. Thus we begin with the set of reductions 
.
First, if any relation
can be reduced, replace 
and 
with the reductions.
Next, we add more reductions (that is, rewriting rules) to eliminate possible exceptions of confluence. Suppose that
and 
, where 
, overlap. That is, either the prefix of 
equals the suffix of 
, or vice versa. In the former case, we can write 
; in the latter case, 
.
Reduce the word
using 
first, then using 
first. Call the results 
, respectively. If 
, then we have an instance where confluence could fail. Hence, add the reduction 
to 
.
After adding a rule to
, remove any rules in 
that might have reducible left sides.
Repeat the procedure until all overlapping left sides have been checked.
. We use the shortlex order
. 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
in (1) and (3). Consider the word 
. Reducing using (1), we get 
. Reducing using (3), we get 
. Hence, we get 
, giving the reduction rule (4) 
.
Similarly, using the overlap of
in (2) and (3), we get the reduction (5) 
.
Both of these rules obsolete (3), so we remove it.
Next, consider the overlap of
of (1) and (5). Considering 
we get 
, so we add the rule (6) 
. This obsoletes rules (4) and (5), so we remove them. Considering 
, we get 
, so we add the rule (7) 
.
Now, we are left with the rewriting system
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.
The notion of logged rewriting discussed in the paper by Heyworth and Wensley listed below allows some recording or logging of the rewriting process as it proceeds. This is useful for computing identities among relations for presentations of groups.
Algorithm
In mathematics and computer science, an algorithm is an effective method expressed as a finite list of well-defined instructions for calculating a function. Algorithms are used for calculation, data processing, and automated reasoning...
for transforming a set of equation
Equation
An equation is a mathematical statement that asserts the equality of two expressions. In modern notation, this is written by placing the expressions on either side of an equals sign , for examplex + 3 = 5\,asserts that x+3 is equal to 5...
s (over terms
Term (mathematics)
A term is a mathematical expression which may form a separable part of an equation, a series, or another expression.-Definition:In elementary mathematics, a term is either a single number or variable, or the product of several numbers or variables separated from another term by a + or - sign in an...
) into a confluent
Confluence (term rewriting)
In computer science, confluence is a property of rewriting systems, describing that terms in this system can be rewritten in more than one way, to yield the same result. This article describes the properties in the most abstract setting of an abstract rewriting system.- Motivating example :Consider...
term rewriting system. When the algorithm succeeds, it has effectively solved the word problem
Word problem (mathematics)
In mathematics and computer science, a word problem for a set S with respect to a system of finite encodings of its elements is the algorithmic problem of deciding whether two given representatives represent the same element of the set...
for the specified algebra
Algebra
Algebra is the branch of mathematics concerning the study of the rules of operations and relations, and the constructions and concepts arising from them, including terms, polynomials, equations and algebraic structures...
.
An important case in computational group theory
Computational group theory
In mathematics, computational group theory is the study ofgroups by means of computers. It is concernedwith designing and analysing algorithms anddata structures to compute information about groups...
are string rewriting systems which can be used to give canonical labels to elements or coset
Coset
In mathematics, if G is a group, and H is a subgroup of G, and g is an element of G, thenA coset is a left or right coset of some subgroup in G...
s of a finitely presented group as products of the generators. This special case is the current focus of this article.
Motivation in group theory
The critical pair lemma states that a term rewriting system is locally confluentConfluence (term rewriting)
In computer science, confluence is a property of rewriting systems, describing that terms in this system can be rewritten in more than one way, to yield the same result. This article describes the properties in the most abstract setting of an abstract rewriting system.- Motivating example :Consider...
(or weakly confluent) if and only if the critical pairs are convergent. Furthermore, we have Newman's lemma
Newman's lemma
In the theory of rewriting systems, Newman's lemma states that a terminating abstract rewriting system , that is, one in which there are no infinite reduction sequences, is confluent if it is locally confluent...
which states that if an (abstract) rewriting system is strongly normalizing
Normal form (term rewriting)
In abstract rewriting, a normal form is an element of the system which cannot be rewritten any further. Stated formally, for some reduction relation ⋅ → ⋅ over X a term t in X is a normal form if there does not exist a term t′ in X such that t → t′.Consider...
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
where X is a finite set of generators and R is a set of defining relations on X. Let X* be the set of all words in X (i.e. the free monoid generated by X). Since the relations R define 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. 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 < B in which case B → A is a rule in the rewriting system, otherwise A > B and A → 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 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.
Description of the algorithm for finitely presented monoids
Suppose we are given a presentationPresentation of a group
In mathematics, one method of defining a group is by a presentation. One specifies a set S of generators so that every element of the group can be written as a product of powers of some of these generators, and a set R of relations among those generators...
, where is a set of generatorGenerating set of a group
In abstract algebra, a generating set of a group is a subset that is not contained in any proper subgroup of the group. Equivalently, a generating set of a group is a subset such that every element of the group can be expressed as the combination of finitely many elements of the subset and their...
s and
is a set of relationsRelation (mathematics)
In set theory and logic, a relation is a property that assigns truth values to k-tuples of individuals. Typically, the property describes a possible connection between the components of a k-tuple...
giving the rewriting system. Suppose further that we have a reduction ordering
among the words generated by . For each relation in , suppose . Thus we begin with the set of reductions .First, if any relation
can be reduced, replace and with the reductions.Next, we add more reductions (that is, rewriting rules) to eliminate possible exceptions of confluence. Suppose that
and , where , overlap. That is, either the prefix of equals the suffix of , or vice versa. In the former case, we can write ; in the latter case, .Reduce the word
using first, then using first. Call the results , respectively. If , then we have an instance where confluence could fail. Hence, add the reduction to .After adding a rule to
, remove any rules in that might have reducible left sides.Repeat the procedure until all overlapping left sides have been checked.
Example
Consider the presentation. We use the shortlex orderShortlex order
The shortlex order is an ordering for ordered sets of objects, where the sequences are primarily sorted by cardinality with the shortest sequences first, and sequences of the same length are sorted into lexicographical order....
. 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
in (1) and (3). Consider the word . Reducing using (1), we get . Reducing using (3), we get . Hence, we get , giving the reduction rule (4) .Similarly, using the overlap of
in (2) and (3), we get the reduction (5) .Both of these rules obsolete (3), so we remove it.
Next, consider the overlap of
of (1) and (5). Considering we get , so we add the rule (6) . This obsoletes rules (4) and (5), so we remove them. Considering , we get , so we add 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.
Generalizations
If Knuth–Bendix 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.The notion of logged rewriting discussed in the paper by Heyworth and Wensley listed below allows some recording or logging of the rewriting process as it proceeds. This is useful for computing identities among relations for presentations of groups.