The Knuth–Bendix completion algorithm (named after
Donald Knuth
Donald Ervin Knuth ( ; born January 10, 1938) is an American computer scientist, mathematician, and professor emeritus at Stanford University. He is the 1974 recipient of the ACM Turing Award, informally considered the Nobel Prize of computer sci ...
and Peter Bendix) is a
semi-decision algorithm
In mathematics and computer science, an algorithm () is a finite sequence of rigorous instructions, typically used to solve a class of specific problems or to perform a computation. Algorithms are used as specifications for performing ...
for transforming a set of
equation
In mathematics, an equation is a formula that expresses the equality of two expressions, by connecting them with the equals sign . The word ''equation'' and its cognates in other languages may have subtly different meanings; for example, in ...
s (over
terms) into a
confluent term rewriting system
In mathematics, computer science, and logic, rewriting covers a wide range of methods of replacing subterms of a formula with other terms. Such methods may be achieved by rewriting systems (also known as rewrite systems, rewrite engines, or red ...
. When the algorithm succeeds, it effectively solves the
word problem for the specified
algebra
Algebra () is one of the broad areas of mathematics. Roughly speaking, algebra is the study of mathematical symbols and the rules for manipulating these symbols in formulas; it is a unifying thread of almost all of mathematics.
Elementary a ...
.
Buchberger's algorithm
In the theory of multivariate polynomials, Buchberger's algorithm is a method for transforming a given set of polynomials into a Gröbner basis, which is another set of polynomials that have the same common zeros and are more convenient for extract ...
for computing
Gröbner bases is a very similar algorithm. Although developed independently, it may also be seen as the instantiation of Knuth–Bendix algorithm in the theory of
polynomial ring
In mathematics, especially in the field of algebra, a polynomial ring or polynomial algebra is a ring (which is also a commutative algebra) formed from the set of polynomials in one or more indeterminates (traditionally also called variabl ...
s.
Introduction
For a set ''E'' of equations, its deductive closure () is the set of all equations that can be derived by applying equations from ''E'' in any order.
Formally, ''E'' is considered a
binary relation
In mathematics, a binary relation associates elements of one set, called the ''domain'', with elements of another set, called the ''codomain''. A binary relation over sets and is a new set of ordered pairs consisting of elements in and i ...
, () is its
rewrite closure, and () is the
equivalence closure
In mathematics, a subset of a given set is closed under an operation of the larger set if performing that operation on members of the subset always produces a member of that subset. For example, the natural numbers are closed under addition, but ...
of ().
For a set ''R'' of rewrite rules, its deductive closure ( ∘ ) is the set of all equations that can be confirmed by applying rules from ''R'' left-to-right to both sides until they are literally equal.
Formally, ''R'' is again viewed as a binary relation, () is its rewrite closure, () is its
converse
Converse may refer to:
Mathematics and logic
* Converse (logic), the result of reversing the two parts of a definite or implicational statement
** Converse implication, the converse of a material implication
** Converse nonimplication, a logical ...
, and ( ∘ ) is the
relation composition
In the mathematics of binary relations, the composition of relations is the forming of a new binary relation from two given binary relations ''R'' and ''S''. In the calculus of relations, the composition of relations is called relative multiplica ...
of their
reflexive transitive closure
In mathematics, a subset of a given set is closed under an operation of the larger set if performing that operation on members of the subset always produces a member of that subset. For example, the natural numbers are closed under addition, but ...
s ( and ).
For example, if are the
group
A group is a number of persons or things that are located, gathered, or classed together.
Groups of people
* Cultural group, a group whose members share the same cultural identity
* Ethnic group, a group whose members share the same ethnic ide ...
axioms, the derivation chain
:
demonstrates that ''a''
−1⋅(''a''⋅''b'') ''b'' is a member of ''Es deductive closure.
If is a "rewrite rule" version of ''E'', the derivation chains
:
demonstrate that (''a''
−1⋅''a'')⋅''b'' ∘ ''b'' is a member of ''Rs deductive closure.
However, there is no way to derive ''a''
−1⋅(''a''⋅''b'') ∘ ''b'' similar to above, since a right-to-left application of the rule 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''.
Rules
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):
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 if
* in the
encompassment ordering, or
* and are
literally similar and .
Example
The following example run, obtained from the
E theorem prover, computes a completion of the (additive) group axioms as in Knuth, Bendix (1970).
It starts with the three initial equations for the group (neutral element 0, inverse elements, associativity), using
f(X,Y)
for ''X''+''Y'', and
i(X)
for −''X''.
The 10 starred equations turn out to constitute the resulting convergent rewrite system.
"pm" is short for "
paramodulation", implementing ''deduce''. Critical pair computation is an instance of paramodulation for equational unit clauses.
"rw" is rewriting, implementing ''compose'', ''collapse'', and ''simplify''.
Orienting of equations is done implicitly and not recorded.
See also
Word problem (mathematics)
In computational mathematics, a word problem is the problem of deciding whether two given expressions are equivalent with respect to a set of rewriting identities. A prototypical example is the word problem for groups, but there are many other ...
for another presentation of this example.
String rewriting systems in group theory
An important case in
computational group theory
In mathematics, computational group theory is the study of
groups by means of computers. It is concerned
with designing and analysing algorithms and
data structures to compute information about groups. The subject
has attracted interest because fo ...
are string rewriting systems which can be used to give canonical labels to elements or
coset
In mathematics, specifically group theory, a subgroup of a group may be used to decompose the underlying set of into disjoint, equal-size subsets called cosets. There are ''left cosets'' and ''right cosets''. Cosets (both left and right) ...
s of a
finitely presented group
In mathematics, a presentation is one method of specifying a group. A presentation of a group ''G'' comprises 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 ...
as products of the
generators. This special case is the focus of this section.
Motivation in group theory
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. Furthermore, we have
Newman's lemma which states that if an (abstract) rewriting system is
strongly normalizing
In abstract rewriting, an object is in normal form if it cannot be rewritten any further, i.e. it is irreducible. Depending on the rewriting system, an object may rewrite to several normal forms or none at all. Many properties of rewriting systems ...
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 generate an equivalence relation on X*, one can consider elements of M to be the equivalence classes of X
* under R. For each class ' it is desirable to choose a standard representative ''w
k''. This representative is called the canonical or normal form for each word ''w
k'' in the class. If there is a computable method to determine for each ''w
k'' its normal form ''w
i'' 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
In mathematics, a well-order (or well-ordering or well-order relation) on a set ''S'' is a total order on ''S'' with the property that every non-empty subset of ''S'' has a least element in this ordering. The set ''S'' together with the well-o ...
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 W
i → W
i+1 it is possible to end up with two different irreducible reductions W
n ≠ 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
presentation
A presentation conveys information from a speaker to an audience. Presentations are typically demonstrations, introduction, lecture, or speech meant to inform, persuade, inspire, motivate, build goodwill, or present a new idea/product. Presenta ...
, where
is a set of
generators and
is a set of
relations giving the rewriting system. Suppose further that we have a reduction ordering
among the words generated by
(e.g.,
shortlex order In mathematics, and particularly in the theory of formal languages, shortlex is a total ordering for finite sequences of objects that can themselves be totally ordered. In the shortlex ordering, sequences are primarily sorted by cardinality (length ...
). 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
overlap.
# Case 1: either the prefix of
equals the suffix of
, or vice versa. In the former case, we can write
and
; in the latter case,
and
.
#Case 2: either
is completely contained in (surrounded by)
, or vice versa. In the former case, we can write
and
; in the latter case,
and
.
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 (after checking if such rules have critical pairs with other rules).
Repeat the procedure until all overlapping left sides have been checked.
Examples
A terminating example
Consider the monoid:
:
.
We use the
shortlex order In mathematics, and particularly in the theory of formal languages, shortlex is a total ordering for finite sequences of objects that can themselves be totally ordered. In the shortlex ordering, sequences are primarily sorted by cardinality (length ...
. This is an infinite monoid but nevertheless, the Knuth–Bendix algorithm is able to solve the word problem.
Our beginning three reductions are therefore
A suffix of
(namely
) is a prefix of
, so consider the word
. Reducing using (), we get
. Reducing using (), we get
. Hence, we get
, giving the reduction rule
Similarly, using
and reducing using () and (), we get
. Hence the reduction
Both of these rules obsolete (), so we remove it.
Next, consider
by overlapping () and (). Reducing we get
, so we add the rule
Considering
by overlapping () and (), we get
, so we add the rule
These obsolete rules () and (), so we remove them.
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.
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
In mathematics, a free abelian group is an abelian group with a basis. Being an abelian group means that it is a set with an addition operation that is associative, commutative, and invertible. A basis, also called an integral basis, is a sub ...
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.
Generalizations
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.
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.
References
*
*
* C. Sims. 'Computations with finitely presented groups.' Cambridge, 1994.
* Anne Heyworth and C.D. Wensley.
Logged rewriting and identities among relators" ''Groups St. Andrews 2001 in Oxford. Vol. I,'' 256–276, London Math. Soc. Lecture Note Ser., 304, Cambridge Univ. Press, Cambridge, 2003.
External links
*
Knuth-Bendix Completion Visualizer
{{DEFAULTSORT:Knuth-Bendix completion algorithm
Computational group theory
Donald Knuth
Combinatorics on words
Rewriting systems