Internally a monoid presentation P of the group Q is constructed. By default the generators of P are taken to be g_1, (g_1)^(-1), ..., g_n, (g_n)^(-1) where g_1, ..., g_n are the generators of Q. The relations of P are taken to be the relations of Q. The trivial relations between the generators and their inverses are also added. The word ordering is the short-lex ordering. The Knuth--Bendix completion procedure for monoids is now run on P to calculate the word difference arising from the generated equations thereby calculating the finite state automata associated with a short-lex automatic group.Regardless of whether or not the completion procedure succeeds the result will be an automatic group, G, containing four automata. These are the first and second word-difference machines, the word acceptor, and the word multiplier. If the procedure succeeds G will be marked as confluent, and the word problem for G is therefore decidable. If, as is very likely, the procedure fails then G will be marked as non-confluent. In this case G the four automata contained in G will be those computed from the known equations at the point at which the completion procedure failed.
For simple examples, the algorithms work quickly, and do not require much space. For more difficult examples, the algorithms are often capable of completing successfully, but they can sometimes be expensive in terms of time and space requirements. Another point to be borne in mind is that the algorithms sometimes produce temporary disk files which the user does not normally see (because they are automatically removed after use), but can occasionally be very large. These files are stored in the /tmp directory. If you interrupt a running automatic group calculation you must remove these temporary files yourself.
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 automatic group. The best values to set for these limits varies from example to example.
TidyInt: RngIntElt Default: 20After finding n 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.) The word-differences arising from the equations are calculated after each such tidying and the number reported if verbose printing is on. The best strategy in general is to try a small value of TidyInt first and, if that is not successful, try increasing it. Large values such as 1000 work best in really difficult examples.
MaxRelations: RngIntElt Default: 200Limit the maximum number of reduction equations to MaxRelations.
MaxStates: RngIntElt Default: 1000Limit the maximum number of states of the finite state automaton used for word reduction to MaxStates.
MaxReduceLen: RngIntElt Default: 32767Limit the maximum allowed length that a word can reach during reduction to MaxReduceLen. This limit is usually not needed.
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, and the group defined by the equations changes.
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: 0If 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 group defined by the output equations may be different from the original.
GeneratorOrder: SeqEnum Default:Give an ordering for the generators of P. This ordering affects the ordering of words in the alphabet. If not specified the ordering defaults to [g_1, (g_1)^(-1), ..., g_n, (g_n)^(-1)] where g_1, ..., g_n are the generators of Q.
ConfNum: RngIntElt Default: 500If 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 is 0, then the fast confluence check is performed only when the search for overlaps is complete.
MaxWordDiffs: RngIntElt Default:Limit the maximum number of word differences to MaxWordDiffs. The default behaviour is to increase the number of allowed word differences dynamically as required, and so usually one does not need to set this option.
HaltingFactor: RngIntElt Default: 100
MinTime: RngIntElt Default: 5These options are experimental halting options. HaltingFactor is a positive integer representing a percentage. After each tidying it is checked whether both the number of equations and the number of states have increased by more than HaltingFactor percent since the number of word-differences was last less than what it is now. If so the program halts. A sensible value seems to be 100, but occasionally a larger value is necessary. If the MinTime option is also set then halting only occurs if at least MinTime seconds of cpu-time have elapsed altogether. This is sometimes necessary to prevent very early premature halting. It is not very satisfactory, because of course the cpu-time depends heavily on the particular computer being used, but no reasonable alternative has been found yet.
Large: BoolElt Default: falseIf Large is set to true large hash tables are used internally. Also the Knuth--Bendix algorithm is run with larger parameters, specifically TidyInt is set to 500, MaxRelns is set to 262144, MaxStates is set to unlimited, HaltingFactor is set to 100, MinTime is set to 20 and ConfNum is set to 0. It is advisable to use this option only after having first tried without it, since it will cause easy examples to take much longer to run.
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.
> F<a,b,c,d> := FreeGroup(4); > Q := quo< F | a^-1*b^-1*a*b=d^-1*c^-1*d*c>; > G := AutomaticGroup(Q); Running Knuth-Bendix with the following parameter values MaxRelations = 200 MaxStates = 0 TidyInt = 20 MaxWdiffs = 512 HaltingFactor = 100 MinTime = 5 #Halting with 78 equations. #First word-difference machine with 33 states computed. #Second word-difference machine with 33 states computed. #System is confluent, or halting factor condition holds. #Word-acceptor with 36 states computed. #General multiplier with 104 states computed. #Validity test on general multiplier succeeded. #General length-2 multiplier with 220 states computed. #Checking inverse and short relations. #Checking relation: _8*_6*_7*_5 = _2*_4*_1*_3 #Axiom checking succeeded. > print G; An automatic group. Generator Ordering = [ a, a^-1, b, b^-1, c, c^-1, d, d^-1 ] The second word difference machine has 33 states. The word acceptor has 36 states.
> F<a,b> := FreeGroup(2); > Q := quo< F | a*a=1, b*b=b^-1, b^-1*a*b^-1*a*b^-1*a*b^-1=a*b*a*b*a*b*a>; > G := AutomaticGroup(Q : TidyInt := 20); Running Knuth-Bendix with the following parameter values MaxRelations = 200 MaxStates = 0 TidyInt = 20 MaxWdiffs = 512 HaltingFactor = 100 MinTime = 5 #Halting with 67 equations. #First word-difference machine with 30 states computed. #Second word-difference machine with 30 states computed. #System is confluent, or halting factor condition holds. #Word-acceptor with 52 states computed. #General multiplier with 135 states computed. #Validity test on general multiplier succeeded. #General length-2 multiplier with 161 states computed. #Checking inverse and short relations. #Checking relation: _4*_1*_4*_1*_4*_1*_4 = _1*_3*_1*_3*_1*_3*_1 #Axiom checking succeeded. > print G; An automatic group. Generator Ordering = [ a, a^-1, b, b^-1 ] The second word difference machine has 30 states. The word acceptor has 52 states.
> F<a,b> := FreeGroup(2); > Q := quo< F | b*a^-1*b=a^-1*b*a^-1>; > G := AutomaticGroup(Q: GeneratorOrder := [a,a^-1,b,b^-1]); Running Knuth-Bendix with the following parameter values MaxRelations = 200 MaxStates = 0 TidyInt = 20 MaxWdiffs = 512 HaltingFactor = 100 MinTime = 5 #Halting with 83 equations. #First word-difference machine with 15 states computed. #Second word-difference machine with 17 states computed. #System is confluent, or halting factor condition holds. #Word-acceptor with 15 states computed. #General multiplier with 67 states computed. #Multiplier incorrect with generator number 4. #General multiplier with 71 states computed. #Validity test on general multiplier succeeded. #General length-2 multiplier with 361 states computed. #Checking inverse and short relations. #Checking relation: _3*_2*_3 = _2*_3*_2 #Axiom checking succeeded. > print G; An automatic group. Generator Ordering = [ a, a^-1, b, b^-1 ] The second word difference machine has 21 states. The word acceptor has 15 states.
> F<d, f> := FreeGroup(2); > Q := quo< F | f*d*f^-1*d*f*d^-1*f^-1*d*f^-1*d^-1=1>;
> G := AutomaticGroup(Q); Running Knuth-Bendix with the following parameter values MaxRelations = 200 MaxStates = 0 TidyInt = 20 MaxWdiffs = 512 HaltingFactor = 100 MinTime = 5 #Maximum number of equations exceeded. #Halting with 195 equations. #First word-difference machine with 45 states computed. #Second word-difference machine with 53 states computed. >> G := AutomaticGroup(Q); ^ Runtime error in 'AutomaticGroup': Knuth Bendix failed: > G := AutomaticGroup(Q : Large := true); Running Knuth-Bendix with the following parameter values MaxRelations = 262144 MaxStates = 0 TidyInt = 500 MaxWdiffs = 512 HaltingFactor = 100 MinTime = 5 #Halting with 3055 equations. #First word-difference machine with 49 states computed. #Second word-difference machine with 61 states computed. #System is confluent, or halting factor condition holds. #Word-acceptor with 101 states computed. #General multiplier with 497 states computed. #Multiplier incorrect with generator number 3. #General multiplier with 509 states computed. #Multiplier incorrect with generator number 3. #General multiplier with 521 states computed. #Multiplier incorrect with generator number 3. #General multiplier with 525 states computed. #Validity test on general multiplier succeeded. #General length-2 multiplier with 835 states computed. #Checking inverse and short relations. #Checking relation: _3*_1*_4*_1*_3 = _1*_3*_2*_3*_1 #Axiom checking succeeded. > print G; An automatic group. Generator Ordering = [ d, d^-1, f, f^-1 ] The second word difference machine has 89 states. The word acceptor has 101 states.
Construct the identity word in G.
Given an automatic group G defined on r generators and a sequence [i_1, ..., i_s] of integers lying in the range [ - r, r], excluding 0, construct the word G.|i_1|^(epsilon_1) * G.|i_2|^(epsilon_2) * ... * G.|i_s|^(epsilon_s) where epsilon_j is +1 if i_j is positive, and -1 if i_j is negative.
> FG<a,b> := FreeGroup(2); > Q := quo< FG | b^-1*a*b=a>; > G := AutomaticGroup(Q); Running Knuth-Bendix with the following parameter values MaxRelations = 200 MaxStates = 0 TidyInt = 20 MaxWdiffs = 512 HaltingFactor = 100 MinTime = 5 #System is confluent. #Halting with 8 equations. #First word-difference machine with 9 states computed. #Second word-difference machine with 9 states computed. #System is confluent, or halting factor condition holds. #Word-acceptor with 5 states computed. #General multiplier with 17 states computed. #Validity test on general multiplier succeeded. #Checking inverse and short relations. #Axiom checking succeeded. > print Id(G); Id(G) > print G!1; Id(G)
Having constructed an automatic group G one can perform arithmetic with words in G. Assuming we have u, v in G then the product u * v will be computed as follows:
Product of the words w and v.
Product of the word u by the inverse of the word v, i.e. the word u * v^(-1).
The n-th power of the word w.
Conjugate of the word u by the word v, i.e. the word v^(-1) * u * v.
The inverse of the word w.
Commutator of the words u and v, i.e., the word u^(-1)v^(-1)uv. Here u and v must belong to the same group.
Given r words u_1, ..., u_r belonging to a common group, return their commutator. Commutators are left-normed, so they are evaluated from left to right.
Given words w and v belonging to the same group, return true if w and v reduce to the same normal form, false otherwise. If G is confluent this tests for equality. If G is non-confluent then two words which are the same may not reduce to the same normal form.
Given words w and v belonging to the same group, return false if w and v reduce to the same normal form, true otherwise. If G is confluent this tests for non-equality. If G is non-confluent then two words which are the same may reduce to different normal forms.
Returns true if the word w is the identity word.
The length of the word w.
The sequence Q obtained by decomposing the element u of an automatic group into its constituent generators and generator inverses. Suppose u is a word in the automatic group G. Then, if u = G.i_1^(e_1) ... G.i_m^(e_m), with each e_i equaling plus or minus 1, then Q[j] = i_j if e_j = + 1 and Q[j] = - i_j if e_j = (-1), for j = 1, ..., m.
> FG<a,b,c,d,e> := FreeGroup(5); > Q := quo< FG | a*d*d=1, b*d*d*d=1, c*d*d*d*d*d*e*e*e=1>; > G<a,b,c,d,e> := AutomaticGroup(Q); Running Knuth-Bendix with the following parameter values MaxRelations = 200 MaxStates = 0 TidyInt = 20 MaxWdiffs = 512 HaltingFactor = 100 MinTime = 5 #System is confluent. #Halting with 177 equations. #First word-difference machine with 34 states computed. #Second word-difference machine with 37 states computed. #System is confluent, or halting factor condition holds. #Word-acceptor with 42 states computed. #General multiplier with 164 states computed. #Multiplier incorrect with generator number 3. #General multiplier with 168 states computed. #Validity test on general multiplier succeeded. #General length-2 multiplier with 462 states computed. #Checking inverse and short relations. #Checking relation: _5*_7^4 = _10^3*_8 #Axiom checking succeeded. > print a*d; d^-1 > print a/(d^-1); d^-1 > print c*d^5*e^2; e^-1 > print a^b, b^-1*a*b; a a > print (a*d)^-2, Inverse(a*d)^2; a^-1 a^-1 > print c^-1*d^-1*c*d eq (c,d); true > print IsIdentity(b*d^3); true > print #(c*d*d*d*d*d*e*e); 1