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]