Knuth–Bendix completion algorithm
The Knuth–Bendix completion algorithm (named after
Buchberger's algorithm 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 rings.
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
For example, if E = {1⋅x = x, x−1⋅x = 1, (x⋅y)⋅z = x⋅(y⋅z)} are the group axioms, the derivation chain
- a−1⋅(a⋅b) (a−1⋅a)⋅b 1⋅b b
demonstrates that a−1⋅(a⋅b) 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
- (a−1⋅a)⋅b 1⋅b b and b b
demonstrate that (a−1⋅a)⋅b ∘ b is a member of R's 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 (x⋅y)⋅z → x⋅(y⋅z) is not allowed.
The Knuth–Bendix algorithm takes a set E of equations between
Rules
Given a set E of equations between
They are based on a user-given- s l in the encompassment ordering, or
- s and l are literally similarand t > r.
Delete | ‹ E∪{s = s} | , R › | ⊢ | ‹ E | , R › | |
Compose | ‹ E | , R∪{s → t} › | ⊢ | ‹ E | , R∪{s → u} › | if t u |
Simplify | ‹ E∪{s = t} | , R › | ⊢ | ‹ E∪{s = u} | , R › | if t u |
Orient | ‹ E∪{s = t} | , R › | ⊢ | ‹ E | , R∪{s → t} › | if s > t |
Collapse | ‹ E | , R∪{s → t} › | ⊢ | ‹ E∪{u = t} | , R › | if s u by l → r with (s → t) ▻ (l → r) |
Deduce | ‹ E | , R › | ⊢ | ‹ E∪{s = t} | , R › | if (s,t) is a critical pair of R
|
Example
The following example run, obtained from the
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.
Nr | Lhs | Rhs | Source | ||
1: | * | f(X,0) | = | X | initial("GROUP.lop", at_line_9_column_1) |
2: | * | f(X,i(X)) | = | 0 | initial("GROUP.lop", at_line_12_column_1) |
3: | * | f(f(X,Y),Z) | = | f(X,f(Y,Z)) | initial("GROUP.lop", at_line_15_column_1) |
5: | f(X,Y) | = | f(X,f(0,Y)) | pm(3,1) | |
6: | f(X,f(Y,i(f(X,Y)))) | = | 0 | pm(2,3) | |
7: | f(0,Y) | = | f(X,f(i(X),Y)) | pm(3,2) | |
27: | f(X,0) | = | f(0,i(i(X))) | pm(7,2) | |
36: | X | = | f(0,i(i(X))) | rw(27,1) | |
46: | f(X,Y) | = | f(X,i(i(Y))) | pm(5,36) | |
52: | * | f(0,X) | = | X | rw(36,46) |
60: | * | i(0) | = | 0 | pm(2,52) |
63: | i(i(X)) | = | f(0,X) | pm(46,52) | |
64: | * | f(X,f(i(X),Y)) | = | Y | rw(7,52) |
67: | * | i(i(X)) | = | X | rw(63,52) |
74: | * | f(i(X),X) | = | 0 | pm(2,67) |
79: | f(0,Y) | = | f(i(X),f(X,Y)) | pm(3,74) | |
83: | * | Y | = | f(i(X),f(X,Y)) | rw(79,52) |
134: | f(i(X),0) | = | f(Y,i(f(X,Y))) | pm(83,6) | |
151: | i(X) | = | f(Y,i(f(X,Y))) | rw(134,1) | |
165: | * | f(i(X),i(Y)) | = | i(f(Y,X)) | pm(83,151) |
See also Word problem (mathematics) for another presentation of this example.
String rewriting systems in group theory
An important case in
Motivation in group theory
The
Consider a
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
- 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 presentation , 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). 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. This is an infinite monoid but nevertheless, the Knuth–Bendix algorithm is able to solve the word problem.
Our beginning three reductions are therefore
-
(1)
-
(2)
-
.(3)
A suffix of (namely ) is a prefix of , so consider the word . Reducing using (1), we get . Reducing using (3), we get . Hence, we get , giving the reduction rule
-
.(4)
Similarly, using and reducing using (2) and (3), we get . Hence the reduction
-
.(5)
Both of these rules obsolete (3), so we remove it.
Next, consider by overlapping (1) and (5). Reducing we get , so we add the rule
-
.(6)
Considering by overlapping (1) and (5), we get , so we add the rule
-
.(7)
These obsolete rules (4) and (5), so we remove them.
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.
A non-terminating example
The order of the generators may crucially affect whether the Knuth–Bendix completion terminates. As an example, consider the
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]
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
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
- ^ D. Knuth, "The Genesis of Attribute Grammars"
- ISBN 978-0-85729-808-9.
- ISBN 978-3-540-18088-3., p. 55
- ^ Bachmair, L.; Dershowitz, N.; Hsiang, J. (Jun 1986). "Orderings for Equational Proofs". Proc. IEEE Symposium on Logic in Computer Science. pp. 346–357.
- J.-P. Jouannaud(1990). Jan van Leeuwen (ed.). Rewrite Systems. Handbook of Theoretical Computer Science. Vol. B. Elsevier. pp. 243–320. Here: sect.8.1, p.293
- ISBN 978-3-7643-9911-5.
- . Retrieved 24 December 2021.
- D. Knuth; P. Bendix (1970). J. Leech (ed.). Simple Word Problems in Universal Algebras (PDF). Pergamon Press. pp. 263–297.
- Gérard Huet (1981). "A Complete Proof of Correctness of the Knuth-Bendix Completion Algorithm" (PDF). J. Comput. Syst. Sci. 23 (1): 11–21. .
- 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.