• « Previous
• Up
• Contents
• Index
• Search
• Next »

Construction of a Rewrite Monoid

RWSMonoid(Q: parameters) : MonFP -> MonRWS

The Knuth--Bendix completion procedure for monoids is run, with the relations of Q taken as the initial reduction rules for the procedure. Regardless of whether or not the completion procedure succeeds, the result will be a rewrite monoid, M, containing a reduction machine and a sequence of reduction relations. If the procedure succeeds M will be marked as confluent, and the word problem for M is therefore decidable. If, as is very likely, the procedure fails then M will be marked as non-confluent. In this case M will contain both the reduction relations and the reduction machine computed up to the point of failure.

As the Knuth--Bendix procedure will more often than not run forever, some conditions must be specified under which it will stop. These take the form of limits that are placed on certain variables, such as the number of reduction relations. If any of these limits are exceeded during a run of the completion procedure it will fail, returning a non-confluent rewrite monoid. The optimal values for these limits varies from example to example.

     MaxRelations: RngIntElt             Default: 32767

Limit the maximum number of reduction equations to MaxRelations.

     GeneratorOrder: SeqEnum             Default:

Give an ordering for the generators. This ordering affects the ordering of words in the alphabet. If not specified the ordering defaults to the order induced by Q's generators, that is [g₁, ..., g_n] where g₁, ..., g_n are the generators of Q.

     Ordering: MonStgElt                 Default: "ShortLex"

     Levels: SeqEnum                     Default:

     Weights: SeqEnum                    Default:

Ordering := "ShortLex": Use the short-lex ordering on strings. Shorter words come before longer, and for words of equal length lexicographical ordering is used, using the given ordering of the generators.

Ordering := "Recursive" | "RTRecursive": Use a recursive ordering on strings. There are various ways to define this. Perhaps the quickest is as follows. Let u and v be strings in the generators. If one of u and v, say v, is empty, then u ≥v. Otherwise, let u=u' a and v=v' b, where a and b are generators. Then u > v if and only if one of the following holds:

(i)

a = b and u' > v';

(ii)

a > b and u > v';

(iii)

b > a and u' > v.

The RTRecursive ordering is similar to the Recursive ordering, but with u=au' and v=bv'. Occasionally one or the other runs significantly quicker, but usually they perform similarly.

Ordering := "WTShortLex": Use a weighted-lex ordering. Weights should be a sequence of non-negative integers, with the i-th element of Weights giving the weight of the i-the generator. The length of Weights must equal the number of generators. The length of words in the generators is then computed by adding up the weights of the generators in the words. Otherwise, ordering is as for short-lex.

Ordering := "Wreath": Use a wreath-product ordering. Levels should be a sequence of non-negative integers, with the i-th element of Levels giving the level of the i-the generator. The length of Levels must equal the number of generators. In this ordering, two strings involving generators of the same level are ordered using short-lex, but all strings in generators of a higher level are larger than those involving generators of a lower level. That is not a complete definition; one can be found in [Sim94, pp. 46--50]. Note that the recursive ordering is the special case in which the level of generator number i is i.

     TidyInt: RngIntElt                  Default: 100

After finding TidyInt new reduction equations, the completion procedure interrupts the main process of looking for overlaps, to tidy up the existing set of equations. This will eliminate any redundant equations performing some reductions on their left and right hand sides to make the set as compact as possible. (The point is that equations discovered later often make older equations redundant or too long.)

     RabinKarp: Tup                      Default:

Use the Rabin-Karp algorithm for word-reduction on words having length at least l, provided that there are at least n equations, where RabinKarp := <l, n>. This uses less space than the default reduction automaton, but it is distinctly slower, so it should only be used when seriously short of memory. Indeed this option is only really useful for examples in which collapse occurs - i.e. at some intermediate stage of the calculation there is a very large set of equations, which later reduces to a much smaller confluent set. Collapse is not uncommon when analysing pathological presentations of finite groups, and this is one situation where the performance of the Knuth--Bendix algorithm can be superior to that of Todd-Coxeter coset enumeration. The best setting for RabinKarp varies from example to example - generally speaking, the smaller l is, the slower things will be, so set it as high as possible subject to not running out of memory. The number of equations n should be set higher than the expected final number of equations.

     MaxStates: RngIntElt                Default:

Limit the maximum number of states of the finite state automaton used for word reduction to MaxStates. By default there is no limit, and the space allocated is increased dynamically as required. The space needed for the reduction automaton can also be restricted by using the RabinKarp parameter. This limit is not usually needed.

     MaxReduceLen: RngIntElt             Default: 32767

Limit the maximum allowed length that a word can reach during reduction to MaxReduceLen. It is only likely to be exceeded when using the recursive ordering on words. This limit is usually not needed.

     ConfNum: RngIntElt                  Default: 500

If ConfNum overlaps are processed and no new equations are discovered, then the overlap searching process is interrupted, and a fast check for confluence performed on the existing set of equations. Doing this too often wastes time, but doing it at the right moment can also save a lot of time. If ConfNum = 0, then the fast confluence check is performed only when the search for overlaps is complete.

Warning: Changing the default setting for any of the following parameters may either cause the procedure to terminate without having found a confluent presentation or change the monoid.

     MaxStoredLen: Tup                   Default:

Only equations in which the left and right hand sides have lengths at most l and r, respectively, where MaxStoredLen := <l, r> are kept. Of course this may cause the overlap search to complete on a set of equations that is not confluent. In some examples, particularly those involving collapse (i.e. a large intermediate set of equations, which later simplifies to a small set), it can result in a confluent set being found much more quickly. It is most often useful when using a recursive ordering on words. Another danger with this option is that sometimes discarding equations can result in information being lost, with the effect of changing the monoid defined by the equations.

     MaxOverlapLen: RngIntElt            Default:

Only overlaps of total length at most MaxOverlapLen are processed. Of course this may cause the overlap search to complete on a set of equations that is not confluent.

     Sort: BoolElt                       Default: false

     MaxOpLen: RngIntElt                 Default: 0

If Sort is set to {true} then the equations will be sorted in order of increasing length of their left hand sides, rather than the default, which is to leave them in the order in which they were found. MaxOpLen should be a non-negative integer. If MaxOpLen is positive, then only equations with left hand sides having length at most MaxOpLen are output. If MaxOpLen is zero, then all equations are sorted by length. Of course, if MaxOpLen is positive, there is a danger that the monoid defined by the output equations may be different from the original.

SetVerbose("KBMAG", v) : MonStgElt, RngIntElt ->

Set the verbose printing level for the Knuth-Bendix completion algorithm. Setting this level allows a user to control how much extra information on the progress of the algorithm is printed. Currently the legal values for v are 0 to 3 inclusive. Setting v to 0 corresponds to the `-silent' option of KBMAG in which no extra output is printed. Setting v to 2 corresponds to the `-v' (verbose) option of KBMAG in which a small amount of extra output is printed. Setting v to 3 corresponds to the `-vv' (very verbose) option of KBMAG in which a huge amount of diagnostic information is printed.

> FM<g10,g20,g30> := FreeMonoid(3);
> Q := quo< FM | g10^2=1, g20*g30=1, g30*g20=1,
>         g20*g20=g30, g30*g10*g30=g10*g20*g10>;
> M := RWSMonoid(Q);
> print M;
A confluent rewrite monoid.
Generator Ordering = [ g10, g20, g30 ]
Ordering = ShortLex.
The reduction machine has 12 states.
The rewrite relations are:
    g10^2 = Id(FM)
    g20 * g30 = Id(FM)
    g30 * g20 = Id(FM)
    g20^2 = g30
    g30 * g10 * g30 = g10 * g20 * g10
    g30^2 = g20
    g20 * g10 * g20 = g10 * g30 * g10
    g30 * g10 * g20 * g10 = g20 * g10 * g30
    g10 * g20 * g10 * g30 = g30 * g10 * g20
    g20 * g10 * g30 * g10 = g30 * g10 * g20
    g10 * g30 * g10 * g20 = g20 * g10 * g30

> FM<x,X,y,Y,z,Z> := FreeMonoid(6);
> Q := quo< FM |
>         x*X=1, X*x=1, y*Y=1, Y*y=1, z*Z=1, Z*z=1,
>         y*y*X*Y*x*Y*z*y*Z*Z*X*y*x*Y*Y*z*z*Y*Z*y*z*z*Y*Z*y=1,
>         z*z*Y*Z*y*Z*x*z*X*X*Y*z*y*Z*Z*x*x*Z*X*z*x*x*Z*X*z=1,
>         x*x*Z*X*z*X*y*x*Y*Y*Z*x*z*X*X*y*y*X*Y*x*y*y*X*Y*x=1>;
> M := RWSMonoid(Q : TidyInt := 3000);
> print M;
A confluent rewrite monoid.
Generator Ordering = [ x, X, y, Y, z, Z ]
Ordering = ShortLex.
The reduction machine has 1 state.
The rewrite relations are:
    Z = Id(FM)
    Y = Id(FM)
    z = Id(FM)
    X = Id(FM)
    y = Id(FM)
    x = Id(FM)

> FM<a,b,c> := FreeMonoid(6);
> Q := quo< FM | b*a=a*b*c, c*a=a*c, c*b=b*c >;
> M := RWSMonoid(Q:Ordering:="Recursive", GeneratorOrder:=[c,b,a]);
> M;
A confluent rewrite monoid.
Generator Ordering = [ c, b, a ]
Ordering = Recursive.
The reduction machine has 3 states.
    b * a = a * b * c
    c * a = a * c
    c * b = b * c
> Order(M);
Infinity

> FM<a,b,c,d,e,f,g> := FreeMonoid(7);
> I := [a*b=c, b*c=d, c*d=e, d*e=f, e*f=g, f*g=a, g*a=b];
> Q := quo<FM | I>;
> M := RWSMonoid(Q: Ordering := "Recursive", MaxStoredLen := <15,15>);
Warning: Knuth Bendix only partly succeeded
> Q := quo< FM | Relations(M) cat I>;
> M := RWSMonoid(Q: Ordering := "Recursive");
> print M;
A confluent rewrite monoid.
Generator Ordering = [ a, b, c, d, e, f, g ]
Ordering = Recursive.
The reduction machine has 30 states.
The rewrite relations are:
    c = a^25
    d = a^20
    e = a^16
    f = a^7
    g = a^23
    b = a^24
    a^30 = a
> Order(M);
30

• « Previous
• Up
• Contents
• Index
• Search
• Next »