[GAP Forum] "Knuth-Bendix Rewriting Confluent" hangs

[Alexander Hulpke]

Dear GAP-Forum,

Robert Eckert wrote:

> Forcing Knuth-Bendix to run asks if this is in "the swamp", when, alas,
> the swamp is bottomless.  Holt's KBMag package says, effectively, "let's
> just map the top ten meters of the swamp".  Pardon me if I am asking a
> "duh, of course!" or "duh, of course not!" question, but is there a way of
> force-feeding a set of rules?  "Forget what Knuth-Bendix says looks
> good, you will use THESE rules and like it"?  The problem may be that K-B

While I'm not 100% certain on this interpretation, I understand yoiur
question as asking whether you can prescribe your own rewriting rules.

This is possible (see the manual chapter on rewriting systems). However in
this case:
- you will have to ensure confluence on your own. (which can be
  nontrivial).
- Unless you substitute your rewriting system (for this you would have to
  change the library code), you will have to call `ReducedForm' with monoid
  elements and cannot simply do group arithmetic.

> wants to find the shortening possibilities, where actually a rewriting
> that makes most things longer is what some purposes need.
> If I rewrite in an ugly set of generators, I can deploy a filtration,
> pure-F4 = top-F4 semidirect product by pure-C3, which is top-C3 by
> pure-C2, which is top-C2 by pure-A1, which is free on letter-1-squared.
> For each high-grade generator G and lower-grade g there is exactly one
> relation like
> G g = g G' G" G G"- G'-
> moving g left and replacing G with its conjugate by a varying number (zero

What you are doing effectively is to work in some quotient group. GAP can
get you some of these (see e.g. `SolvableQuotient'). 

In principle you could try to generalize existing code to work even in a
profinite quotient. The problem then becomes to know when to stop evaluating
to prove (non)-equality of elements.

Best wishes,

   Alexander Hulpke