fbpx
Wikipedia

Knuth–Bendix completion algorithm

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.

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 edit

For a set E of equations, its deductive closure (E) 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, (E) is its rewrite closure, and (E) is the equivalence closure of (E). For a set R of rewrite rules, its deductive closure (RR) 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, (R) is its rewrite closure, (R) is its converse, and (RR) is the relation composition of their reflexive transitive closures (R and R).

For example, if E = {1⋅x = x, x−1x = 1, (xy)⋅z = x⋅(yz)} are the group axioms, the derivation chain

a−1⋅(ab)   E   (a−1a)⋅b   E   1⋅b   E   b

demonstrates that a−1⋅(ab) E b is a member of E's deductive closure. If R = { 1⋅xx, x−1x → 1, (xy)⋅zx⋅(yz) } is a "rewrite rule" version of E, the derivation chains

(a−1a)⋅b   R   1⋅b   R   b       and       b   R   b

demonstrate that (a−1a)⋅b RR b is a member of R's deductive closure. However, there is no way to derive a−1⋅(ab) RR b similar to above, since a right-to-left application of the rule (xy)⋅zx⋅(yz) 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 edit

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 (st) ▻ (lr) if

Delete ‹ E∪{s = s} , R › ‹ E , R ›
Compose         ‹ E , R∪{st} ›         ⊢         ‹ E , R∪{su} ›         if t R u
Simplify ‹ E∪{s = t} , R › ‹ E∪{s = u} , R › if t R u
Orient ‹ E∪{s = t} , R › ‹ E , R∪{st}  › if s > t
Collapse ‹ E , R∪{st} › ‹ E∪{u = t} , R › if s R u by lr with (st) ▻ (lr)
Deduce ‹ E , R › ‹ E∪{s = t} , R › if (s,t) is a critical pair of R

Example edit

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.

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 edit

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. This special case is the focus of this section.

Motivation in group theory edit

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 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 {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 edit

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.

  1. 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  .
  2. 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 edit

A terminating example edit

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 edit

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]

Generalizations edit

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.[7]

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 edit

  1. ^ D. Knuth, "The Genesis of Attribute Grammars"
  2. ^ Jacob T. Schwartz; Domenico Cantone; Eugenio G. Omodeo; Martin Davis (2011). Computational Logic and Set Theory: Applying Formalized Logic to Analysis. Springer Science & Business Media. p. 200. ISBN 978-0-85729-808-9.
  3. ^ Hsiang, J.; Rusinowitch, M. (1987). "On word problems in equational theories" (PDF). Automata, Languages and Programming. Lecture Notes in Computer Science. Vol. 267. p. 54. doi:10.1007/3-540-18088-5_6. ISBN 978-3-540-18088-3., p. 55
  4. ^ Bachmair, L.; Dershowitz, N.; Hsiang, J. (Jun 1986). "Orderings for Equational Proofs". Proc. IEEE Symposium on Logic in Computer Science. pp. 346–357.
  5. ^ N. Dershowitz; 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
  6. ^ V. Diekert; A.J. Duncan; A.G. Myasnikov (2011). "Geodesic Rewriting Systems and Pregroups". In Oleg Bogopolski; Inna Bumagin; Olga Kharlampovich; Enric Ventura (eds.). Combinatorial and Geometric Group Theory: Dortmund and Ottawa-Montreal conferences. Springer Science & Business Media. p. 62. ISBN 978-3-7643-9911-5.
  7. ^ Bachmair, Leo; Dershowitz, Nachum; Plaisted, David A. (1989). "Completion Without Failure" (PDF). Rewriting Techniques: 1–30. doi:10.1016/B978-0-12-046371-8.50007-9. 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. doi:10.1016/0022-0000(81)90002-7.
  • 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 edit

knuth, bendix, completion, algorithm, named, after, donald, knuth, peter, bendix, semi, decision, algorithm, transforming, equations, over, terms, into, confluent, term, rewriting, system, when, algorithm, succeeds, effectively, solves, word, problem, specifie. 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 Buchberger s algorithm for computing Grobner 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 Contents 1 Introduction 2 Rules 3 Example 4 String rewriting systems in group theory 4 1 Motivation in group theory 4 2 Description of the algorithm for finitely presented monoids 4 3 Examples 4 3 1 A terminating example 4 3 2 A non terminating example 5 Generalizations 6 References 7 External linksIntroduction editFor a set E of equations its deductive closure E 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 E is its rewrite closure and E is the equivalence closure of E For a set R of rewrite rules its deductive closure R R 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 R is its rewrite closure R is its converse and R R is the relation composition of their reflexive transitive closures R and R 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 E a 1 a b E 1 b E bdemonstrates 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 a 1 a b R 1 b R b and b R bdemonstrate 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 gt 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 editGiven 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 gt 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 s gt e l in the encompassment ordering or s and l are literally similar and t gt r Delete E s s R E R Compose E R s t E R s u if t R uSimplify E s t R E s u R if t R uOrient E s t R E R s t if s gt tCollapse E R s t E u t R if s R u by l r with s t l r Deduce E R E s t R if s t is a critical pair of RExample editThe 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 Nr Lhs Rhs Source1 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 editAn 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 This special case is the focus of this section Motivation in group theory edit 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 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 M X R displaystyle M langle X mid R rangle nbsp 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 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 lt 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 lt should also have the property A lt B XAY lt XBY for all words A B X YThis 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 lt B in which case B A is a rule in the rewriting system otherwise A gt B and A B Since lt is a reduction order a given word W can be reduced W gt W 1 gt gt 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 edit Suppose we are given a presentation X R displaystyle langle X mid R rangle nbsp where X displaystyle X nbsp is a set of generators and R displaystyle R nbsp is a set of relations giving the rewriting system Suppose further that we have a reduction ordering lt displaystyle lt nbsp among the words generated by X displaystyle X nbsp e g shortlex order For each relation P i Q i displaystyle P i Q i nbsp in R displaystyle R nbsp suppose Q i lt P i displaystyle Q i lt P i nbsp Thus we begin with the set of reductions P i Q i displaystyle P i rightarrow Q i nbsp First if any relation P i Q i displaystyle P i Q i nbsp can be reduced replace P i displaystyle P i nbsp and Q i displaystyle Q i nbsp with the reductions Next we add more reductions that is rewriting rules to eliminate possible exceptions of confluence Suppose that P i displaystyle P i nbsp and P j displaystyle P j nbsp overlap Case 1 either the prefix of P i displaystyle P i nbsp equals the suffix of P j displaystyle P j nbsp or vice versa In the former case we can write P i B C displaystyle P i BC nbsp and P j A B displaystyle P j AB nbsp in the latter case P i A B displaystyle P i AB nbsp and P j B C displaystyle P j BC nbsp Case 2 either P i displaystyle P i nbsp is completely contained in surrounded by P j displaystyle P j nbsp or vice versa In the former case we can write P i B displaystyle P i B nbsp and P j A B C displaystyle P j ABC nbsp in the latter case P i A B C displaystyle P i ABC nbsp and P j B displaystyle P j B nbsp Reduce the word A B C displaystyle ABC nbsp using P i displaystyle P i nbsp first then using P j displaystyle P j nbsp first Call the results r 1 r 2 displaystyle r 1 r 2 nbsp respectively If r 1 r 2 displaystyle r 1 neq r 2 nbsp then we have an instance where confluence could fail Hence add the reduction max r 1 r 2 min r 1 r 2 displaystyle max r 1 r 2 rightarrow min r 1 r 2 nbsp to R displaystyle R nbsp After adding a rule to R displaystyle R nbsp remove any rules in R displaystyle R nbsp 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 edit A terminating example edit Consider the monoid x y x 3 y 3 x y 3 1 displaystyle langle x y mid x 3 y 3 xy 3 1 rangle nbsp 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 x 3 1 displaystyle x 3 rightarrow 1 nbsp 1 y 3 1 displaystyle y 3 rightarrow 1 nbsp 2 x y 3 1 displaystyle xy 3 rightarrow 1 nbsp 3 A suffix of x 3 displaystyle x 3 nbsp namely x displaystyle x nbsp is a prefix of x y 3 x y x y x y displaystyle xy 3 xyxyxy nbsp so consider the word x 3 y x y x y displaystyle x 3 yxyxy nbsp Reducing using 1 we get y x y x y displaystyle yxyxy nbsp Reducing using 3 we get x 2 displaystyle x 2 nbsp Hence we get y x y x y x 2 displaystyle yxyxy x 2 nbsp giving the reduction rule y x y x y x 2 displaystyle yxyxy rightarrow x 2 nbsp 4 Similarly using x y x y x y 3 displaystyle xyxyxy 3 nbsp and reducing using 2 and 3 we get x y x y x y 2 displaystyle xyxyx y 2 nbsp Hence the reduction x y x y x y 2 displaystyle xyxyx rightarrow y 2 nbsp 5 Both of these rules obsolete 3 so we remove it Next consider x 3 y x y x displaystyle x 3 yxyx nbsp by overlapping 1 and 5 Reducing we get y x y x x 2 y 2 displaystyle yxyx x 2 y 2 nbsp so we add the rule y x y x x 2 y 2 displaystyle yxyx rightarrow x 2 y 2 nbsp 6 Considering x y x y x 3 displaystyle xyxyx 3 nbsp by overlapping 1 and 5 we get x y x y y 2 x 2 displaystyle xyxy y 2 x 2 nbsp so we add the rule y 2 x 2 x y x y displaystyle y 2 x 2 rightarrow xyxy nbsp 7 These obsolete rules 4 and 5 so we remove them Now we are left with the rewriting system x 3 1 displaystyle x 3 rightarrow 1 nbsp 1 y 3 1 displaystyle y 3 rightarrow 1 nbsp 2 y x y x x 2 y 2 displaystyle yxyx rightarrow x 2 y 2 nbsp 6 y 2 x 2 x y x y displaystyle y 2 x 2 rightarrow xyxy nbsp 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 edit 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 x y x 1 y 1 x y y x x x 1 x 1 x y y 1 y 1 y 1 displaystyle langle x y x 1 y 1 xy yx xx 1 x 1 x yy 1 y 1 y 1 rangle nbsp The Knuth Bendix completion with respect to lexicographic order x lt x 1 lt y lt y 1 displaystyle x lt x 1 lt y lt y 1 nbsp finishes with a convergent system however considering the length lexicographic order x lt y lt x 1 lt y 1 displaystyle x lt y lt x 1 lt y 1 nbsp it does not finish for there are no finite convergent systems compatible with this latter order 6 Generalizations editIf 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 7 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 edit D Knuth The Genesis of Attribute Grammars Jacob T Schwartz Domenico Cantone Eugenio G Omodeo Martin Davis 2011 Computational Logic and Set Theory Applying Formalized Logic to Analysis Springer Science amp Business Media p 200 ISBN 978 0 85729 808 9 Hsiang J Rusinowitch M 1987 On word problems in equational theories PDF Automata Languages and Programming Lecture Notes in Computer Science Vol 267 p 54 doi 10 1007 3 540 18088 5 6 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 N Dershowitz 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 V Diekert A J Duncan A G Myasnikov 2011 Geodesic Rewriting Systems and Pregroups In Oleg Bogopolski Inna Bumagin Olga Kharlampovich Enric Ventura eds Combinatorial and Geometric Group Theory Dortmund and Ottawa Montreal conferences Springer Science amp Business Media p 62 ISBN 978 3 7643 9911 5 Bachmair Leo Dershowitz Nachum Plaisted David A 1989 Completion Without Failure PDF Rewriting Techniques 1 30 doi 10 1016 B978 0 12 046371 8 50007 9 Retrieved 24 December 2021 D Knuth P Bendix 1970 J Leech ed Simple Word Problems in Universal Algebras PDF Pergamon Press pp 263 297 Gerard Huet 1981 A Complete Proof of Correctness of the Knuth Bendix Completion Algorithm PDF J Comput Syst Sci 23 1 11 21 doi 10 1016 0022 0000 81 90002 7 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 editWeisstein Eric W Knuth Bendix Completion Algorithm MathWorld Knuth Bendix Completion Visualizer Retrieved from https en wikipedia org w index php title Knuth Bendix completion algorithm amp oldid 1146883395, wikipedia, wiki, book, books, library,

article

, read, download, free, free download, mp3, video, mp4, 3gp, jpg, jpeg, gif, png, picture, music, song, movie, book, game, games.