Talk:Knuth–Bendix completion algorithm

I added a motivation section so hopefully the article is no longer too technical. I'd like to hear other people's thoughts before I remove the tag, though. TooMuchMath 01:45, 27 April 2006 (UTC)[reply]

Well, I've got a Ph.D. in computer science. My first thesis (roughly B.Sc. equivalent) was on analysing and transforming unfailing completion proofs, my second one (M.Sc.) was on automatic learing of search heuristics for completion-based theorem proving, and my Ph.D. and PostDoc work was on superposition-based proving. I've taught rewriting systems (at a T.A. level) for several years. I barely recognize KB completion from the current article. Maybe it's because I come from the CS side. I consider the language and notation from BDP89 or BN98 to be nice and natural. I don't e.g. see why we need a monoid (what is our associative operation?), and I don't know what "generators" are in this context.

 @InProceedings{BDP89,
   author =       {L. Bachmair and N. Dershowitz and D.A. Plaisted},
   title =        { {Completion Without Failure} },
   key =          {BDP89},
   booktitle =    {Resolution of Equations in Algebraic Structures},
   editor =       {H. Ait-Kaci and M. Nivat},
   year =         {1989},
   volume =       {2},
   publisher =    {Academic Press},
   pages =        {1--30},
 }

 @Book{BN:REWRITING-98,
   author =       {F. Baader and T. Nipkow},
   title =        { {Term Rewriting and All That} },
   publisher =    {Cambridge University Press},
   year =         {1998},
 }

--Stephan Schulz 07:12, 27 April 2006 (UTC)[reply]

Thanks for the comments Stephan. I encountered the subject of rewriting systems in Sims' book "Computation With Finitely Presented Groups" so it does sound like we are coming from different places. In fact my understanding is limited to rewriting systems wrt monoids and groups so I'm probably not the best person to rewrite this from the CS perspective. I would welcome any information from the CS perspective, though, and would really like to see this article develop into something that is useful for everyone.

To clarify the case of the monoid, the language $\Sigma ^{*}$ over the alphabet $\Sigma$ is the same thing as the free monoid $F=\Sigma ^{*}$ over the generators $X=\Sigma$ . The associative binary operation is string concatenation and the identity is the empty string. The finite presentation $M=<X|R>$ is basically a way of assigning a partition to $\Sigma ^{*}$ (by taking the transitive, reflexive, symmetric closure of R) so that elements of M are equivalence classes of $\Sigma ^{*}$ . The goal (in my mind) of KB is to produce a system to find a minimum (wrt a reduction order <) representative of an equivalence class starting from any of its representatives .

TooMuchMath 17:20, 27 April 2006 (UTC)[reply]

Ok, now it makes more sense. It looks like your version is restricted to what we call "string rewrite systems". You can define reduction systems and completion on a more general level, with a reduction system (R, =>) given by an arbitrary set R and a binary relation =>, and transforming => into a convergent relation using completion. The concrete case then uses first-order terms as the carrier set and equations/rules over terms to describe the relation. String rewrite systems are a further specialization for the case that you only have unary function symbols. --Stephan Schulz 20:24, 27 April 2006 (UTC)[reply]

I'd like to be able to tackle the general case but there are still a few things I don't quite grasp. If we start with an arbitrary set R and a relation => then it makes sense to talk about the transitive closure relation =>* given by reduction sequences. However I don't see how the notion of term and subterm fits in here. That is, we need a way to identify elements of R as compositions of other elements of R so that we may apply a rule a => b to terms other than a (IE applying this rule to ab we get the reduction ab => bb). Perhaps this is somehow captured in a grammar for R but we have taken R to be an arbitrary set, not a formal language.

Also, I don't understand what you mean by "transforming => into a convergent relation using completion." Is this simply the transitive closure =>*? I've never taken a course in logic so an example of a rewriting system that isn't a string rewriting system would be very helpful. TooMuchMath 21:47, 27 April 2006 (UTC)[reply]

In the abstract case, you don't use composite elements. You assume an arbitrary binary relation over arbitrary elements. That each equation potentially defines equality for an infite number of instances in an infinite number of contexts is irrelevant in that abstract view. Manipulating equations manipulates all the instances in one go. As for a concrete example, here is a completion of the group axioms as in the KB70 paper (straight out of my prover E):

     1 :  : [++equal(f(X1,0), X1)] : initial("GROUP.lop", at_line_9_column_1)
     2 :  : [++equal(f(X1,i(X1)), 0)] : initial("GROUP.lop", at_line_12_column_1)
     3 :  : [++equal(f(f(X1,X2),X3), f(X1,f(X2,X3)))] : initial("GROUP.lop", at_line_15_column_1)
     5 :  : [++equal(f(X1,X2), f(X1,f(0,X2)))] : pm(3,1)
     6 :  : [++equal(f(X1,f(X2,i(f(X1,X2)))), 0)] : pm(2,3)
     7 :  : [++equal(f(0,X2), f(X1,f(i(X1),X2)))] : pm(3,2)
    27 :  : [++equal(f(X1,0), f(0,i(i(X1))))] : pm(7,2)
    36 :  : [++equal(X1, f(0,i(i(X1))))] : rw(27,1)
    46 :  : [++equal(f(X1,X2), f(X1,i(i(X2))))] : pm(5,36)
    52 :  : [++equal(f(0,X1), X1)] : rw(36,46)
    60 :  : [++equal(i(0), 0)] : pm(2,52)
    63 :  : [++equal(i(i(X1)), f(0,X1))] : pm(46,52)
    64 :  : [++equal(f(X1,f(i(X1),X2)), X2)] : rw(7,52)
    67 :  : [++equal(i(i(X1)), X1)] : rw(63,52)
    74 :  : [++equal(f(i(X1),X1), 0)] : pm(2,67)
    79 :  : [++equal(f(0,X2), f(i(X1),f(X1,X2)))] : pm(3,74)
    83 :  : [++equal(X2, f(i(X1),f(X1,X2)))] : rw(79,52)
   134 :  : [++equal(f(i(X1),0), f(X2,i(f(X1,X2))))] : pm(83,6)
   151 :  : [++equal(i(X1), f(X2,i(f(X1,X2))))] : rw(134,1)
   165 :  : [++equal(f(i(X1),i(X2)), i(f(X2,X1)))] : pm(83,151)
   239 :  : [++equal(f(X1,0), X1)] : 1 : 'final'
   240 :  : [++equal(f(X1,i(X1)), 0)] : 2 : 'final'
   241 :  : [++equal(f(f(X1,X2),X3), f(X1,f(X2,X3)))] : 3 : 'final'
   242 :  : [++equal(f(0,X1), X1)] : 52 : 'final'
   243 :  : [++equal(i(0), 0)] : 60 : 'final'
   244 :  : [++equal(i(i(X1)), X1)] : 67 : 'final'
   245 :  : [++equal(f(i(X1),X1), 0)] : 74 : 'final'
   246 :  : [++equal(f(X1,f(i(X1),X2)), X2)] : 64 : 'final'
   247 :  : [++equal(f(i(X1),f(X1,X2)), X2)] : 83 : 'final'
   248 :  : [++equal(i(f(X1,X2)), f(i(X2),i(X1)))] : 165 : 'final'

I hope the format is more or less self-explaining. Notice non-unary terms like "f(X1,0)" with variables and constants. We start with the three initial equations for the group (neutral element, inverse element, associativity). The 10 equations marked with "final" represent the resulting convergent rewrite system. "pm" is short for "paramodulation", a generalization of critical pairs to non-unit clauses (we only have units in this example, though). "rw" is rewriting. Ordering of equations is done implicitely and not recorded. --Stephan Schulz 22:00, 27 April 2006 (UTC)[reply]