automata has a very large number of command line options. These are discussed in detail in the following sections with related options grouped together. The distinction between the various groups of options is not always clear-cut, and so you may also wish to refer to the Table of options for automata.
These options are also all accepted by the KBMAG compatibility programs: kbprog, kbprogcos, autgroup, autcos, and gpmakefsa, (even though not all the options may be relevant to all of those programs). automata also accepts almost all the KBMAG compatibility options itself, though in one or two cases options are specific to a particular utility.
When MAF starts its implementation of the Knuth-Bendix procedure it chooses values for options that have not been specified explicitly, and for its internal limits, to try to maximise its chances of success. This is done using fairly simple-minded heuristics, based on the minimum and maximum size of the axioms, the number of generators, the word-ordering method, and the values of any options that have been specified explicitly.
Many options have a fixed default setting, and so will need to be set explicitly if you want to change them. In general you will only want to change these options if you find automata behaves badly with its default settings. The -strategy string option allow the user to try various predefined combinations of these options that have proved helpful for some input files.
This option is used to tell automata to read a substructure file as well as a regular input file, and to create a coset system input file and use that as input for the program.
The -resume option tells MAF to read any output file produced by a previous run of automata, or some other program and to use the equations contained in it as additional axioms for the current run. MAF will first look for a file with a .pkbprog suffix, and then if it cannot find that, one with a .kbprog suffix. No warning is given if neither file exists.
If automata is started without any of the the options to be described in this section, then depending on the nature of the input files, MAF will follow one of two plans:
Plan A: MAF will initially assume that an automatic structure is required and will compute the word-differences of the equations it finds, and guess when it is safe to try to perform the computation of an automatic structure. Initially MAF will allow long equations that contain new word-differences into its main list of equations (rather than "pooling" them). If there are very many word differences then MAF will eventually stop doing this, and will also become reluctant to try to build an automatic structure, and will instead behave more as though it were looking for a confluent rewriting system. However, MAF still will eventually attempt to build an automatic structure if it appears that there are no more word differences to be found, either because the rewriting system becomes confluent, or because after a while the word-difference machine can recognise all new equations.
This plan is the default if a geodesic ordering is used, unless the underlying object has generators for which inverses have not been specified.
Plan C: MAF will assume that a confluent rewriting system is required, and continue the Knuth-Bendix procedure until it finds one. After doing so it will also compute an automatic structure if it is possible to do so. This plan is the default if a non-geodesic word-ordering is used, or word-differences cannot be computed.
Unfortunately, while there may be many times when MAF's computations succeed quickly in either case, there are input files for which it is either necessary or highly advisable to use command line options to give MAF more information about what it should do.
The -confluent and -no_wd (or -nowd) command line options both inform MAF that you require a confluent rewriting system (so select plan C). Both options cause MAF to suppress computation of word-differences. The options only differ in what happens when confluence is achieved:
The -confluent option is on by default for all non-geodesic orderings. It is off by default for geodesic orderings.
For large finite groups, and for pathological presentations, these options can make MAF run much more quickly. You should probably always use -no_wd if what you are trying to do is to prove the non-existence of a non-trivial group, because in this case you hope your presentation will be trivial. For example with the -no_wd option MAF proves the difficult examples/trivial/degen4c example trivial in well under thirty seconds on most machines, but run with no special options, it is likely to take two minutes or longer. If you are mainly interested in finite groups, and are not interested in their automatic structure, and don't want any of the other extra automata that automata creates, then you may prefer to use kbprog rather than automata since that has the -nowd option on by default.
This option will force MAF to follow plan A, even for word-orderings where its usual strategy would be to follow plan C. The -force_differences option will have the same effect, but also modifies how plan A is carried out.
There are several command line options that will influence how MAF tries to find a balance between building the an index automaton in a systematic way, which is usually the best strategy for finding a confluent rewriting system, and looking ahead for long equations that contain new word-differences, which is often the strategy that will make for early success in building an automatic structure. We first document the most important, -no_kb, which stands alone, (you can use it with other options, but they will usually then make no difference). Note that all the other options can be used in any combination, even if the names of the options might suggest otherwise. For example -slow -fast is a valid combination of options. Note that none of these options, other than -force_differences, will actually force MAF to follow its plan A. If MAF is following its plan C then these options will have no effect.
This option tells MAF to suppress the Knuth-Bendix phase altogether and to immediately build an automatic structure, using just the word-differences it has been able to deduce from a very cursory examination of the axioms. This option should be used with caution, and never with a presentation you know is for a finite group, nor for a pathological presentation, but for many infinite groups it will give results in a few seconds rather than several minutes. This is in effect a Plan B for building an automatic structure.
With this option the automata built will almost certainly be incorrect for several iterations. However if the group is genuinely automatic, success is eventually inevitable, and for examples of only moderate difficulty, such as examples/automatic/picard and examples/coxeter/cox33334c this may very well give the fastest results. This option is to be recommended for Triangle and Von Dyck type groups, but not for most Coxeter groups. Even for more difficult examples it is usually beneficial, though for a few examples it may be catastrophic. Another possible reason for using this option is where you have already tried, and failed, to build an automatic structure using automata without the -nokb option. If MAF had created a very large number of equations, then it may not have had enough memory available to be able to work efficiently. When you use the -nokb option the number of equations will be kept to a minimum. So there might be cases where the resulting saving in memory would allow an automatic structure to be found. Generally, in this case you would also use the -resume option at the same time, so that more word-differences would be known initially.
This option is like a milder form of -no_kb and causes MAF to take a less cautious view than usual about whether or not to try to build an automatic structure. When it works it will save you a few seconds, or perhaps tens of seconds, but in most cases the -no_kb option would also work well, and would be even faster.
-fast works quite well, or at any rate is not horribly counter-productive, with most of the example presentations (even the confluent ones), but it should not really be used for groups you know in advance are finite, since these definitely do have a minimal confluent rewriting system, and MAF will insist on finding it. If you specify the -fast option for such a group then MAF is more likely to try to build the automatic structure before confluence is achieved, and the consequence may be that MAF will spend a long time building a word-acceptor from a word-difference machine, and may have great difficulty doing so. Then, if the word-acceptor is correct, MAF will see that the group is finite and resume Knuth-Bendix processing anyway. In this case time, possibly a long time, has been wasted. And, if the word-acceptor is wrong and MAF still does not know the group is finite, even more time will be wasted, because in such cases it will probably spend a very long time building and then correcting a multiplier.
If a presentation is difficult then the -fast option usually does not make much difference, because MAF will not want to leave the Knuth-Bendix phase anyway.
When MAF is following plan A, then unless the -tight option is used, it will be allowing some long equations into the index-automaton early, because it appears they contain new word-differences. Therefore, at the end of each expansion cycle, MAF will normally remove all of these long equations from the index-automaton and put them in the pool. Then, when it checks the pool, any of the equations that do still contain new word-differences will be reinserted, but others, for which the word-differences turned out to be spurious, or can be found in a shorter equation, will remain in the pool. The intention behind this is two-fold:
Usually pruning is beneficial, but in some cases it can be very costly and achieves little (because it turns out almost all the long equations come back), so the -no_prune option is provided to disable pruning completely.
When following its plan A, MAF usually reduces the thoroughness of its search of overlaps if it believes it is soon going to move to building an automatic structure. That helps to speed up processing when the number of equations has become large. However, this can sometimes have the effect of making it much more difficult to actually build an automatic structure because the size of the trial word-acceptor becomes very large. The -slow option forces MAF to search overlaps in a more uniform manner, which may sometimes alleviate this problem.
It is probably worth using this option for difficult automatic structures: run with the -slow option until you think word-differences are becoming stable, then interrupt automata with Ctrl+C, and then restart it with the -nokb and -resume options.
This option tells MAF not to favour equations with word-differences at all even though word-differences will still be computed. While this will usually result in it taking longer for MAF to decide it has found all the word-differences it can sometimes have the opposite effect. Sometimes spurious word-differences in long equations can cause MAF to believe the word-differences are still changing, when in reality all the word-differences have been found and when this option is used this is less likely to occur. Because this option prevents long equations from getting into the index automaton early it can have the effect of making the number of equations that gets created much greater, because MAF is forced to increase its internal limits more quickly.
It is also possibly worth using this option if you think a group might have a confluent rewriting system, but that it possibly does not and it looks as though it may also be automatic.
This option tells MAF to continue to favour equations with word-differences even when there are very many of them. The main reason to use this option is so that you can judge whether it is at all likely a group which has a lot of word-differences might eventually turn out to be automatic. Generally speaking if the number of word-differences continues to grow rapidly when this option is used, then unless you can find a different generating set with better behaviour, there is no hope of finding an automatic structure. In such cases it is better to look for a confluent rewriting system, because it is often the case that input files which give rise to very many word-differences eventually collapse and that the group turns out to be finite.
The -max_equations n option limits the number of primary equations that MAF will create. By default there is no limit. This option works differently depending on whether plan A or plan C is being followed.
Plan A: automata will stop performing Knuth-Bendix expansion as soon as possible after the number of primary equations reaches the maximum, and will try to build an automatic structure.
Plan C: automata will abort and output a provisional rewriting system and index-automaton when the limit is reached
This option, and the next are potentially useful. There are some groups for which a careful choice of this option or the next will give faster results than either relying on automata's plan A, or using the -no_kb option to force plan B. However, there does not seem to be any sensible way of discovering a suitable value: for difficult input files it can be counter-productive to run Knuth-Bendix expansion for more than a very short period of time, because the trial automata can become more difficult to correct because they are much larger when more, but not enough, word-differences are known.
The -max_time n option limits the period for which Knuth-Bendix expansion is performed. n is a number of seconds. By default there is no limit, and this is also the case if you put -max_time 0, so the minimum value is 1. This option works differently depending on whether plan A or plan C is being followed.
Plan A: automata will stop performing Knuth-Bendix expansion as soon as possible after the time limit is exceeded and will try to build an automatic structure.
Plan C: automata will abort and output a provisional rewriting system and index-automaton when the time limit is reached.
See also the comment on -max_equations n above.
The -min_time n option sets a lower limit (in seconds) on the the period during which Knuth-Bendix expansion is performed. By default there is no lower limit. This option is only applicable when plan A is being followed, and will be ignored if a confluent rewriting system is found before the minimum time limit has elapsed.
This option is provided for KBMAG compatibility purposes, and there should be no reason to use it in automata.
When MAF has built a candidate word-acceptor for an automatic structure it will normally use heuristics to determine whether it is a good idea to try to build the general multiplier for the acceptor. If the word-acceptor has too many states, MAF will assume that it is probably wrong, and that, rather than building the multiplier, it should try some other technique to discover missing word-differences. MAF has quite a wide repertoire of such techniques; it will often try several of them in turn, usually building a new candidate word-acceptor after each technique is tried, until eventually it either manages to build a word-acceptor with substantially fewer states (at which point the word-acceptor is usually correct, or very nearly so), or it runs out of ideas, and tries to build the multiplier anyway.
For some groups it might happen that the word-acceptor really is large, or that MAF's other techniques for finding more word-differences don't achieve much. In such cases you can try the -force_multiplier option which will change the heuristics so that an attempt to build the multiplier is made much sooner than it otherwise would be. MAF may still try some its alternative techniques, but will be much more inclined to try to build the multiplier early. You should note, that at least in the author's experience, using this option usually has a bad effect, and it will turn out that it takes longer to build the automatic structure when it is used, even if it appeared that MAF's alternative techniques for finding word-differences were not working well or were being used for too long.
When MAF is computing word-difference machines it is necessary for it to compute large numbers of reductions of words of the form x*w*y where x and y are generators and w is a word-difference. Now, it turns out that if w is a word-difference then w^-1 is also a word difference. Therefore, a computation of this type can be performed by computing (w^-1*x^-1)^-1*y, or alternatively,((w*y)^-1*x^-1)^-1. Note that neither of these computation involves any left multiplication, which means that in many cases MAF can compute a putative element for such words very cheaply, provided it has precomputed the inverses of the relevant words. When w is a word-difference and x is a generator MAF calls a term of the form w^-1*x a left half-difference, and a term of the form (w*x)^-1 a right half-difference. MAF will usually compute word-difference machine using these half-differences. When a rewriting system is not confluent it may happen that these two computations give different results from each other, and that a direct computation of x*w*y gives a third word. When MAF first creates a word-difference it performs all three computations and creates any equations that result. Later on, if x*w*y needs to be computed again, MAF will only will only compute the word directly if it cannot compute it quickly from left or right half-difference states in its index automaton.
If a geodesic word-ordering is being used, the inverse of any group element must be represented by a word of the same length. However, for non-geodesic orderings the inverse of a word may be some much longer word. This means using half-differences can be very awkward when non-geodesic orderings are used. The -no_hd option can be used to suppress computations of half-differences. This will prevent some deductions being made that might otherwise be possible. This option is always turned on if a wreath product type word-ordering is being used, except in the case where word-differences are computed only after confluence has been achieved. You can specify the option explicitly to prevent half-differences being used even in that case (though usually they are then beneficial), or to prevent them being used for an ordering such as "wtlex" in the case where very different weights are attached to a generator and its inverse. You can use this option even for geodesic word-orderings if desired, but it will usually have little effect.
These options can be used to explicitly enable or disable validation of an automatic structure that has been computed by the axiom checking process. MAF's default behaviour is to check axioms for coset systems but not for groups, (unless you use autgroup). For a coset system, you might want to use -no_validate if you are confident that MAF will not have any problems computing the automatic structure correctly in the first place (the author has only ever seen computations fail when the subgroup has finite index, and in fact is not even sure if these failures do still ever happen), or if you plan to run gpaxioms as a separate process later on. For groups you might want to use -validate if you don't trust the author's conjecture that the axiom check for a group will never fail, and would rather do the check from within automata than run gpaxioms as a separate process.
Note that when a completely confluent rewriting system is found, (but not a partially confluent coset system), the -validate option will have no effect. An automatic structure built from a confluent rewriting system cannot possibly fail the axiom check. You can always run gpaxioms if you have any doubts about this.
This instructs MAF never to try to use a weak word-difference machine to build a word acceptor. If MAF finds that constructing a trial word-acceptor using the strong word-difference machine is slow, it will at some point try to use the weak word-difference machine instead, because for some groups this results in much faster construction of the word-acceptor. Subsequently it will revert to using the strong word difference machine unless this proves to be the case. Unfortunately, it can happen that construction of such a word-acceptor will cause MAF to crash. The reason for this is that the maximum number of states in a word-acceptor is an exponential function of the number of word-differences, and this is much more likely to arise when a weak word difference machine is used. So, this command line option is provided to allow you to restart MAF if it behaves in this unfortunate manner.
This option sets a time-out value which MAF uses to age various statistics about word-differences. The default value of the option is 20, which means that these statistics will be aged at most every 10 seconds, and that if more than 20 seconds goes by, MAF will switch to a mode in which fewer overlaps are considered, because it is hoping to move from performing Knuth-Bendix expansion to building an automatic structure.
In fact this option sets a maximum time-out. The time-out will initially start at a very low value, and will be increased towards the "official" time-out as MAF's heuristics determine that the group is more difficult. So setting this value to a very low value might help force MAF to move to building an automatic structure. The lowest value that will have much effect is 4.
These two options, which are only relevant when a coset system is being processed, both tell MAF to check if the subgroup being processed has finite index. MAF will perform this check at the end of an expansion pass if no new coset equations have been created for some time. If MAF finds that a subgroup does have finite index then one one more pass of the Knuth-Bendix procedure is performed, this time only considering overlaps which might reduce the number of cosets further (although it usually happens that as soon as MAF can detect a subgroup has finite index it can determine the index correctly this is by no means always the case, so a further pass is needed). The -detect_finite_index option does not affect MAF's strategy much and can safely be used even for subgroups which you are not sure do have finite index, but the -prove_finite_index modifies processing considerably and should only be used when you don't care if MAF runs out of memory before it can do so.
Both -detect_finite_index and -prove_finite_index modify the behaviour of plan C (as selected by the -confluent and -no_wd options). In this modified form of plan C, MAF will create output files for the coset system as soon as the coset structure is known completely (so that "partial" confluence has been achieved in that the number of cosets and the coset representative for each coset is known). MAF does not now wait until the G-equations are completely confluent. There is one exception to this - if MAF can determine that the entire group is finite at the time it checks for a finite index subgroup, it will wait for the entire system to become confluent.
When you use either of these options, and you are using a subgroup structure file with subgroup generator names you will often also need to use the -ignore_h_length option, and quite possibly the -no_h option as well.
This option tells MAF to use the Knuth-Bendix procedure to try to eliminate some of the axioms in a generated subgroup presentation. This option was added to automata before the simplify utility was provided as part of MAF. Now that simplify is available, it will usually be best to use that instead and simplify the presentation afterwards. That will allow you to try its various different strategies for improving the presentation.
This option is usually only relevant when a coset system with named subgroup generators is being processed. As mentioned elsewhere the H-words that appear on the RHS of coset equations can be extremely long. When this option is used, MAF does not count the H-word part of the RHS in the size of the equation, so that coset equations will be more likely to be inserted into the tree rather than being pooled.
In fact, MAF no longer counts the the coset symbol on the right either, so this option also might make a marginal difference even when subgroup generators are not named.
Using this option will often give much faster results for coset systems with named subgroup generators. On, the other hand, if the option is not used, then MAF will tend to run for longer, and therefore discover more G-equations. So when the -ignore_h_length option is not used, the presentation of the subgroup may be better, because MAF may have been able to determine that some subgroup members, which were initially different Schreier generators, actually represent the same group element.
This option is only relevant when a coset system with named subgroup generators is being processed. When this option is used MAF will not ever perform Knuth-Bendix expansion on equations in the H-words alone. This means it can afford to allow all H-equations that are created into the tree immediately, even though they may be very long. Surprisingly, this often seems to improve the stability of MAF with this type of coset system.
For a coset system using named subgroup generators, this option tells MAF that when it computes the subgroup presentation that it should use the Schreier generators that are the initial states of the multiplier. These are the same generators that would be have been used in any case had a simple coset system been used for the subgroup computation. Why might one want to do this? It is for the same reason that is sometimes best not to use the -ignore_h_length option: MAF will usually run for longer when a coset system with named subgroup generators than a corresponding simple coset system. So, in this case more G-equations will be discovered, which may mean the presentation of the subgroup is more tractable.
automata accepts MAF's standard [loglevel] command line options with the usual meaning: -silent, -quiet and -verbose.
The following options can be used to follow MAF's chain of reasoning in its analysis of a rewriting system. None of these options, is to be recommended for other than the smallest examples, because the volume of output produced will be very high, and especially so when you use -v -ve combination.
-veThe verbose-equations option. Each new equation is printed as it is found. If the -verbose option is explicitly enabled, for example by -v -ve or -verbose -ve, then not only is each new equation printed out, but so is an outline proof that it is true.
-vwdThe verbose word-differences option. In addition to MAF's normal output, each new word-difference found is printed to stdout, together with the equation from which it was computed.
The -strategy string option allows the user to select one of a range of predefined strategies. If it is not used then MAF will pick a strategy based on the properties of the input file and any goal setting options that have been specified (and perhaps some other command line options also). Most predefined strategies have been found to work well with a number of input files, but some are only provided for comparison purposes. The string consists of two parts: first comes a strategy name (which may be blank). This may optionally be followed by a / and a number of single letter options which modify some part of the strategy. The modifiers must be used with caution, because it is possible to create strategies that will cause MAF to create an endless stream of ever longer equations, when other strategies would succeed. Setting a non-empty strategy name is also usually equivalent to setting a number of the other options discussed in later sections. For this reason the -strategy option should usually come early on the command line. It is perfectly legitimate to specify specific new values for options that have already been set by the particular strategy.
The predefined strategies are shown in the table below. On the right is an equivalent set of command-line options that does not specify a named strategy and which would have an identical effect. (In most cases one would not usually need to specify all these options, but all are shown to show the effect of the particular strategy. The meanings of the various strategy modifiers is explained in the next section.
| Name | Purpose | Equivalent command line |
|---|---|---|
| balanced | This option selects a fairly similar combination of options to -strategy short, and usually performs similarly. The only two differences are that:
|
-strategy /ab -partial_reductions 1 -special_overlaps 1 -conjugation 1 -secondary 1 -probe_style 3 |
| easy | Selects options which work well with "easy" input files. Many of MAF's special features are turned off in the hope of speeding up processing. This option may increase execution time substantially if the input file is not in fact "easy". | -strategy /au -partial_reductions 0 -special_overlaps 0 -conjugation 0 -secondary 0 -no_hd -probe_style 0 -work_order 1 |
| era | Selects options which may offer the best hope of success for some input files containing long equations. It is fairly similar to -strategy long, and is worth trying for the same kinds of input file. The "era" strategy makes less use than "long" of new equations that are discovered. This means it tends to complete each pass more quickly, and to make some use at least of the equations that existed at the start of a pass sooner than with other strategies. If a hidden short relation can only be deduced from an overlap between equations that are themselves deduced from overlaps of long equations, this strategy might have the best chance of success. On the other hand, because less use of new equations is made more passes may be needed to discover the equation. | -strategy /ecl -conjugation 0 -expand_all -partial_reductions 1 -probe_style 3 -special_overlaps 0 -work_order 4 |
| long | This is the other strategy that is sometimes useful with input files containing very long equations. | -strategy /lc -partial_reductions 1 -special_overlaps 0 -conjugation 0 -secondary 1 -probe_style 0 -work_order 4 |
| naive | Makes MAF simulate a very naive implementation of the Knuth-Bendix procedure, which does not balance equations and cannot tell which overlaps between equations are minimal (do not contain a reducible subword not including either the first or last letter of the word). This option generally increases execution time substantially and may well cause trouble, especially if the input file uses a non-geodesic word-ordering. | -strategy /du -filters 0 -partial_reductions 0 -special_overlaps 0 -conjugation 0 -secondary 0 -balancing 0 -left_balancing 0 -no_hd -probe_style 0 -work_order 4 |
| quick | Selects options which work well with many input files. Some of MAF's special features are turned off in the hope of speeding up processing, but those features which are most likely to be beneficial are turned on. This strategy may well give the best performance, even for very "easy" input files, but it is not suitable for the most difficult input files. | -strategy /a -partial_reductions 1 -special_overlaps 0 -conjugation 1 -secondary 1 -probe_style 0 -work_order 1 |
| short | Selects the same option combinations that MAF would usually use if started with the -confluent if an input file uses a geodesic-word ordering. This option does not function as a goal-setting option. Its purpose is to allow you to investigate possible modifications to the strategy that might be beneficial for a particular input file. For example some input files might benefit from using -strategy short/ec | -strategy /a -partial_reductions 1 -special_overlaps 1 -conjugation 1 -secondary 1 -probe_style 3 -work_order 1 |
| sparse | Selects the same option combinations that MAF would usually use when looking for an automatic structure for an input file using a geodesic word-ordering. It selects a mode of operation in which MAF is allowed to discard equations, or even fail to consider certain overlaps that might be created with other strategies. (Any such equations will eventually be created, but possibly not until much later than they could have been.) This option does not function as a goal-setting option. Its purpose is to allow you to investigate possible modifications to the strategy that might be beneficial for a particular input file. For example some input files might benefit from using -strategy sparse/ec. This type of strategy is usually only useful when MAF is computing word-differences, and indeed will work quite differently depending on whether they are or not. | -strategy /as -partial_reductions 1 -special_overlaps 1 -conjugation 1 -secondary 2 -probe_style 2 -work_order 1 |
| vanilla | Makes MAF simulate a basic implementation of the Knuth-Bendix procedure, which knows which overlaps are minimal, and which performs balancing. This option generally increases execution time, and may not work well if the input file uses a non-geodesic word-ordering. This option is usually very bad if the input file contains long equations. | -strategy /ue -filters 0 -partial_reductions 0 -special_overlaps 0 -conjugation 0 -secondary 0 -no_hd -probe_style 0 -work_order 2 |
| wreath | Selects the same option combinations that MAF would usually use if started with the -confluent if an input file uses a wreath-product word-ordering. This option does not function as a goal-setting option. Its purpose is to allow you to investigate possible modifications to the strategy that might be beneficial for a particular input file. For example some input files might benefit from using -strategy wreath/fc | -partial_reductions 1 -special_overlaps 1 -conjugation 1 -secondary 3 -probe_style 3 -work_order 2 |
The "vanilla" and "naive" strategies are not recommended for general use. They may be of interest to users who are interested in learning how important MAF's extra means of discovering new equations are to its successful operation. KBMAG's version of kbprog is intermediate between these two strategies: it performs balancing, but only if "shortlex" word-ordering is used. It cannot tell which overlaps are minimal, but if the system appears to becoming confluent, can perform a test which checks the current set of minimal overlaps. It is also the case that MAF will perform much worse with these strategies than KBMAG's kbprog or other Knuth-Bendix implementations might, especially when the input file uses a wreath product word-ordering. That is because MAF always operates with a "reduced" set of rules. This tends to reduce the speed with which new equations can be discovered, and to increase the size and perversity of the equations when a wreath-product ordering is used. MAF also discovers overlaps in a completely different way to KBMAG. When KBMAG is expanding an equation it looks for all the overlaps in which it is the right equation, as well as all the overlaps in which it is the left, but in either case the other equation must not have been created after the equation being expanded. MAF could not implement this strategy efficiently. However it can always determine all the minimal overlaps in which any particular equation is the left equation very quickly, and it is some subset of this overlaps that MAF considers when it is "expanding nodes". When MAF out-performs KBMAG substantially it is usually because its strategies can and do consider the overlaps of recently discovered equations sooner than KBMAG would. When KBMAG out-performs MAF substantially it is usually because of the extra overheads inherent in MAF's design: in particular MAF sometimes gets into a state where a rewriting system is clearly trying to collapse to a much smaller one, but takes a very long time to do so.
The strategy modifiers allow you to modify the predefined strategies or to create entirely new strategies for MAF to use. Each modifier corresponds to either a bit in MAF's internal strategy flags option, or to one of the boolean options set by one of the other command line options for automata. It would be difficult some of these options available using regular command line options without adversely affecting MAF's ability to choose default values for options that have not been specified based on the properties of the input file and the other options chosen.
| Letter | Effect |
|---|---|
| A | This option selects "aggressive discard". MAF normally uses this option unless the word-ordering is non-geodesic and can increase the length of words by an unlimited amount. When this option is in effect many equations which might otherwise have been pooled may instead be discarded. (This does not cause trouble, because either the equation is an "extra" equation that has been discovered other than through the Knuth-Bendix procedure, or it is an equation that MAF's "contract" does not oblige it to keep yet, so that the overlap that gave rise to it will certainly be considered again). This option usually improves performance for input files using geodesic word-orderings. It is not used for input files using wreath product word-orderings, but it is possible that it might sometimes be beneficial. |
| B | This option selects "balanced expand". MAF normally uses only a rather small subset of the available equations as the left equation in overlaps. This option increases the size of this set somewhat, though the amount by which it does so varies a lot depending on the nature of the input file. Using this option might sometimes improve performance, but usually has little effect. |
| C | Makes MAF follow a "closed" strategy. If the strategy is "closed" MAF will not add any new equations to the set of equations which will be expanded on this pass. Note that if the right hand side of an equation in this set becomes reducible then the equation which results from repairing the equation by giving it a new right hand side is new and the equation is removed from the set of equations to be expanded, except when the work order option is 1. The "era" and "long" strategies are closed. All other predefined strategies are open. Closed strategies might work better if many new small equations arise from overlaps between small equations, but eventually a new equation that arises from an overlap between two larger equations causes a collapse, since this overlap may be considered sooner in a "closed" strategy. |
| D | Makes MAF follow a "deep" or possibly "dumb" strategy. If this option is set MAF considers non-minimal overlaps. This option is set for the "naive" strategy, but no others. However, it might occasionally be beneficial when a "closed" strategy is used. |
| E | Makes MAF use "era" based expansion. This means that only overlaps in which the right hand equation existed at the start of the pass are considered. If the strategy is also closed (as the "era" predefined strategy is), then the overlap existed at the start of the pass. This option tends to reduce the time each pass requires to run, but increase the number of passes. It is not usually beneficial, but it is more likely to be so when there are hidden equations. |
| F | Makes MAF "forgetful". MAF knows whether overlaps have been considered before, and will exclude overlaps that have been from being considered again if the size of the equation from the overlap is sufficiently small. If this option is used then MAF will not exclude overlaps like this. It is plausible that when a wreath-product word-ordering is used that using this option might sometimes be beneficial, because it can happen that the equation which arises from the overlap now is desirable, whereas the old equation was modified by a perverse reduction that has since been eliminated but will remain in the pool for several passes. |
| I | Allows MAF to be "intelligent" and to make deductions or inferences from information available to it, that would not be available to a basic Knuth-Bendix program. This option is on by default unless you use the "naive", "vanilla" or "easy" predefined strategies. So an option such as -strategy easy/i might make the "easy" strategy work better with input files that were not in fact very easy. For input files using a non-geodesic word-ordering it is unsafe to use this modifier with the "vanilla" or "naive" strategies unless you also use the P modifier. |
| J | This option has no effect unless word-differences are being computed. If they are then it changes the time at which word-differences are computed. MAF's usual policy is to compute the word-differences of an equation as soon as its current set of equations are all correctly reduced, and before computing conjugates and considering special overlaps. If the J option is specified then word-differences are only computed after conjugation and after special overlaps have been considered. Using the J option will increase the number of equations that are inserted because they appear to contain new word-differences (unless the -tight option is used), because the difference tracker MAF uses to compute word-differences may not yet have had an opportunity to compute the word-differences of some other equation that would give rise to the same word-difference. But, on the other hand, the word-difference machine will contain fewer mistakes. |
| L | This option stops MAF from favouring short equations over long ones. In fact the only thing this option does is to cause the "visible limit" to be set to a higher value than it normally would be (to either the length of longest equation or 8/5 of the "expand limit" is this is greater), and you can achieve the same effect by using the -pool_above n option instead, but this value often seems to work well. When this option is used you may find that there are many more "special overlaps", so it may be necessary to disable special overlap processing completely when you use it. If there are long equations in the input file (with a total length above 20) then MAF might normally set the "visible limit" below the length of some of these equations, which means that overlaps involving these equations may be pooled: MAF tries to keep the initial visible limit to 20 or below, though it will never be less than 8 more than the shortest equation in the input file with a length greater than 4 (only G-equations are relevant if the input file is a coset system). So with some input files, the L option causes the "visible limit" to be set to a much higher value, so that almost all equations will be inserted into the index automaton immediately. In general, it is much better to allow some equations to be pooled rather than disable the pool altogether, because when the index automaton contains many very long equations performance of MAF is adversely affected, because the amount of house-keeping required to insert new equations increases, and because such equations tend to be eliminated when later equations make either the LHS or RHS reducible. In fact, it is not having a pool that is often the main reason why the "vanilla" and "naive" strategies perform poorly. |
| N | This options undoes the effect of the L option. So -strategy long/N would allow you to experiment with using a strategy almost the same as the long strategy, but with a different "visible limit", using the combination of options -strategy long/N -pool_above n where n would probably be some smaller number. The "era" strategy also sets the L strategy option flag, so this option letter might also be useful with that strategy. |
| O | This option undoes the effect of the C modifier, and allows a "closed" strategy to be converted into an open one. So -strategy era/o and -strategy long/o would create "open" versions of these two closed strategies. In an "open" strategy, equations discovered during a pass of the new Knuth-Bendix phase may be added to the set of equations to be expanded if they meet certain criteria. Most input files benefit from "open" strategies, in some cases enormously, but a few are adversely affected. |
| P | This options allows the "vanilla" and "naive" strategies to use the pool, which is essential if you want to modify them with the 'I' option, and it may well make them work much better in any case. |
| S | This is option that is set by the "sparse" strategy. If this option is set more equations can be discarded. This will make the pool smaller, so might sometimes speed up processing if confluence is achieved quickly, but usually it will slow processing down a little because more overlaps need to be considered in more than one pass. You could experiment with using this option with the "wreath" strategy, for which the pool can sometimes get very big so that checking the pool becomes a major part of the processing. |
| T | This option undoes the effect of the 'E' that is set by the "era" and "vanilla" strategies. For each equation that is expanded a list of all the overlaps in which it is the left equation will be constructed, whereas when the 'E' option is used the list will only include overlaps with equations that existed at the start of the pass. |
| U | This option makes a strategy "unintelligent": in such strategies MAF is not allowed to make deductions from information that does not come from considering overlaps. For instance, when word-differences are being computed, using this option will prevent the difference tracker from creating equations that arise from processing coincidences in the word-difference machine. If you use this option then the -no_hd option will be set, because otherwise MAF can go wrong when it tries to compute word-differences, because MAF cannot compute inverses without using deductions. For the same reason this option is incompatible with the -check_inverses option. |
MAF has very many options which will modify its implementation of the Knuth-Bendix procedure, and which can therefore dramatically effect the amount of time and memory needed to find a confluent rewriting system.
When MAF first creates an equation it is fed into a pipeline which attempts to maintain the index automaton in good condition. The first thing that happens to any equation is that its right conjugate is created, if it exists. The last thing to happen before the equation is considered to be fully incorporated into the index automaton, is that undergoes a further process of "conjugation". What happens in this process depends on the value of the -conjugation n option.
| Value | Action performed by conjugation procedure |
|---|---|
| 0 | None |
| 1 | The equation obtained by left balancing (multiplying both sides of the equation by the inverse of the first symbol on the LHS) is considered, if left balancing is possible for this equation. This is the default value for the option unless the "era", "long", or "easy" strategy is specified. |
| 2 | All overlaps with equations with an LHS of length 2 are considered (either to the left or right) |
| 3 | All overlaps of length |LHS|+1 containing the LHS are considered (which of course includes all the overlaps with equations of length 2) |
| 4 | Same as 1, unless a coset system is being processed and this is a G equation. In that case a coset equation is formed by multiplying on the left by the coset symbol. |
-conjugation 0 is quite often beneficial for input files for largish finite groups, at least when the presentation is otherwise straight-forward and a geodesic word-ordering is being used.
This option is only relevant if there are more than 8 group generators, or MAF is processing a coset system and there are more than 8 named subgroup generators. In this case MAF will usually use a sparse format for the transitions in the index automaton it maintains for doing its work. The -dense_rm will force dense format to be used.
Word reduction is somewhat slower when sparse format is used, so MAF may work a little more slowly than normal, but this is usually more than offset by the fact that MAF has less work to do when inserting new equations into the automaton (in fact prior to the possibility of using a sparse transition table it was extremely difficult for MAF to handle input files with large generating sets). One reason you might want to force a dense format index automaton to be used is that without it MAF does not detect many partial reductions: often, when the number of generators is large the generating set is much larger than need be, and in such cases doing the partial reduction checks can be very helpful.
Usually MAF follows a strategy of performing multiple passes of Knuth-Bendix completion, in any one pass considering only overlaps in which the first left hand side satisfies certain criteria which causes MAF to "approve" of the equation. This strategy is often very successful and allows MAF to process some input files many times faster than KBMAG would. However, with some other input files it works very badly. -expand_all orders MAF to consider overlaps of all the equations it knows about in each pass. This will normally degrade performance slightly those will not always be the case. A less drastic option with a somewhat similar effect use the "balanced" strategy, or to specify some other strategy explicitly and apply the B strategy modifier.
This option tells MAF to consider each overlap more fully than it normally would. Instead of just considering the basic overlap that arises from the two originally overlapping LHS, MAF will look for other overlaps which arise in the partially reduced words in these overlaps. It might be the case that such overlaps had not yet been considered, and that doing so will help to discover better reductions for one or other side of the equation arising from the first overlap. This option does not often seem to be useful: it tends to degrade performance slightly (but severely with wreath type word-orderings), but it is also only likely ever to be beneficial with such orderings, since it is for them that is most difficult to arrange matters so that overlaps are considered in a sensible order.
This is one of two options which controls which overlaps MAF will consider for an equation being expanded (the other is -probe_style n). The set of overlaps available for an equation is usually filtered so that only overlaps which are less than a certain length, or which appear to give rise to equations of less than a certain size are considered (the limits being gradually increased at the start of each new pass). The -filters n option is a bit mask which should take a value between 0 and 7 and which defaults to 7. The only value about from 7 which you should currently experiment with is 0, which will stop MAF performing any filtering at all. Changing this option is unlikely to have a good effect.
This option tells MAF not to prevent long equations from being added to the index automaton. This is a very risky option to use, and probably should never be used with non-geodesic word-orderings as it will frequently result in a "feedback loop" that causes MAF to generate an almost endless stream of longer and longer equations. In almost all cases the -pool_above n option will be a better choice than this option. It is sometimes useful for input files which have very long equations, especially in the case where there are also some equations of moderate length. This option does not in fact disable the pool altogether, but if it is used equations will only get into the pool if it is currently impossible to reduce either the LHS or the RHS of the equation (because the maximum word length would be exceeded, or because the reduction cannot be completed in a timely manner)
MAF usually imposes a limit on the number of partial reduction checks and special overlaps which may be pending consideration. It does this because otherwise these aspects of processing can come to unduly dominate MAF's activity. You can use the -no_throttle option to remove the limit. This might be worth doing if you have disabled special overlaps completely, because performing more partial reduction checks will make MAF behave more as though it were performing a Todd-Coxeter coset enumeration, and so might be beneficial when the structure whose automata are being computed is finite.
The -partial_reductions n option, which takes a value between 0 and 7, controls what, if any, checks are made when a transition which will cause part (but not the whole) of the input word to be rewritten, is added to the index automaton. The default value is 1 which enables some checking. -partial_reductions 0 often speeds up processing slightly, and equally often slows it down, sometimes quite severely. The other values introduce some extra, experimental checks, but are rarely, if ever, beneficial.
This option sets the initial "visible limit". Equations up to this size are inserted into the index automaton, longer equations are liable to be placed in the pool, or even discarded altogether (if this happens the overlap that gives rise to the equation will be considered again later). MAF will gradually increase the "visible limit", and the first few passes of the Knuth-Bendix procedure can be very quick, so if you want to set this option you may need to experiment a little to achieve the intended result. Setting this option is sometimes necessary when there is a mix of short and long axioms; unless this option is used MAF can sometimes give too much weight to the overlaps of the shorter axioms (though if you think that might be the case you should try using the "long" or "era" strategies).
This is one of two options which determines which overlaps MAF will be visible for an LHS. The value for -probe_style n is a number between 0 and 3. Value 0 makes the fewest overlaps visible, value 3 the most. MAF divides all the left hand sides into two sets, an "approved" set of short left hand sides, and all the rest. At the start of an expansion phase it computes various limits such as the maximum length of an overlap between two approved or two unapproved equations. It then uses these to select which overlaps are visible. Using a low value of probe_style reduces the number of equations that are created which will subsequently need to be eliminated, and when word-differences are being computed, reduces the number of spurious word-differences that are found. On the other hand it might delay the discovery of a possibly important equation to a later phase.
The -repeat n option which takes a value between 0 and 2, controls how many times MAF will look at the overlaps for those equations that are selected to be considered as the first left hand side in an overlap. It is perfectly possible that after considering all the overlaps for a particular equation new overlaps of that equation will have arisen, or that some of the RHS in the previously considered overlaps have changed, or that the equation arising from an already overlap will be different, or will now satisfy the heuristics that control which equations get inserted into the index-automaton when previously it would not have.
This option defaults to 0, which means that the overlaps for any particular equation will be considered just once per pass. If the option is set to 1, the overlaps of each equation are considered twice, and if it is set to 2, the overlaps are considered repeatedly until considering the overlaps has no effect.
This option will usually degrade performance slightly.
A "special overlap" is an overlap that is discovered as a by-product of inserting an equation into MAF's index automaton, rather than one that is discovered through looking for the overlaps of an equation that is being expanded. MAF inevitably discovers such overlaps from time to time. The -special_overlaps n option determines how these overlaps are treated, and takes a value between 0 and 5. The default value of the option is 1, which means that "special overlaps" will only be considered if they appear to correspond to an equation that is fairly short. You can disable special overlap processing altogether with -special_overlaps 0. This often speeds up computations for straight-forward input files, but it can have a very bad effect for difficult ones: for these special overlap processing is often very important, particularly when a wreath type word-ordering is used. The amount of special overlap processing tends to increase as the number of generators increases, so for input files with large generating sets it is often best to use the -special_overlaps 0 option.
If -special_overlaps is given a value of 2, the length up to which equations are considered to be special is increased slightly: in fact the behaviour will then be similar to version 1 of MAF. The limit has been reduced in version 2 of MAF to try to decrease the proportion of input files for which special overlaps processing is unhelpful. However, some input files work better with the old behaviour.
If -special_overlaps is given a value of 3 or above, many more special overlaps will be processed, (though the length up to which overlaps is special is reduced) and each equation will take longer to create. Values greater than 2 currently are almost always bad.
In each phase of its Knuth-Bendix implementation MAF will select a subset of the available primary equations. For each equation in this subset it will then choose a subset of the overlaps in which the LHS of that equation is the prefix. MAF only constructs this list of overlaps at the time it decides to process that particular equation (MAF refers the process of constructing and processing this list as "Expanding Nodes"). This means that the order in which the subset of equations is processed may have a substantial impact on execution time, especially in the case of a difficult presentation.
The -work_order n option where n is a value from 1 to 6, selects the order in which equations will be processed as shown in the table below.
| n | Ordering |
|---|---|
| 1 | Equations that have not been expanded before are processed first, in shortlex order of LHS. Then any equations that have been expanded before and are to be expanded again are processed, also in shortlex order of LHS. Any equations that are added to the list of equations to be expanded while the expansion phase is proceeding are added to the list of equations that have not been expanded before (so are processed before the equations that have been expanded before) on a first in first out basis. This option is the default unless either a wreath type word-ordering method is used, or the "era" or "long" strategies are used. |
| 2 | Equations are processed in order of RHS length, from shortest first. Equations of equal RHS length, are processed in order of LHS length, from shortest first. Equations of equal LHS and RHS length are ordered according to the ordering of the LHS implied by the word-ordering method. Equations that are added to the list of equations to be expanded while the expansion phase is proceeding are inserted into the list at the correct point, and an equation whose RHS changes will be removed and reinserted at the correct point. This option is the default when a wreath type ordering is used unless the "era" or "long" strategies are used. |
| 3 | Equations that have not been expanded before are processed first, using the same ordering as for -work_order 2. Then equations that have been expanded before are expanded again, with those least recently processed expanded first. This means that on phase 3 say, all the equations that were first expanded in phase 2 will usually be processed before all the equations that were first expanded in phase 1. This explanation ignores a technicality which is explained in connection with -work_order 4 |
| 4 | Equations that have not been expanded before are processed first, in order of the time they were inserted into the index automaton. Then equations that have been expanded before are expanded again, with those least recently processed expanded first. This means that on phase 3 say, all the equations that were first expanded in phase 2 will usually be processed before all the equations that were first expanded in phase 1. There is a technicality, which is that the time of expansion is measured not using actual time, but by a timestamp which represents the most recently created equation against which the equation has been expanded. When the "era" strategy is used, all equations are expanded in a way that ignores all equations created after the expansion phase began, so in the next phase all the equations that were expanded have the same timestamp, so will be sorted by the time they were inserted into the automaton. Equations will also appear to have been expanded at the same time if no new equations were added to the index automaton in between the two expansions. -work_order 4 is the default if the "era" or "long" strategies are used. |
| 5 | Equations are processed in order of LHS length, from shortest first. Equations of equal LHS length are ordered according to the ordering of the LHS implied by the word-ordering method. Equations that are added to the list of equations to be expanded while the expansion phase is proceeding are inserted into the list at the correct point. |
| 6 | Equations are processed in order of LHS length, from longest first. Equations of equal LHS length are ordered according to the ordering of the LHS implied by the word-ordering method. Equations that are added to the list of equations to be expanded while the expansion phase is proceeding are inserted into the list at the correct point. |
For a difficult presentations it may well be worth trying -work_order 4 if the default strategy does not work well. In cases where MAF is out-performed by KBMAG using this option will often work well. Option 6 often sometimes well also.
Every equation in a minimal confluent rewriting system has the property that both the RHS and every subword of the LHS are irreducible. This kind of equation is called a primary equation. An equation which instead has the property that both the RHS and every prefix of the LHS are irreducible is called a secondary equation. Secondary equations play an important role in MAF. This is true even if you choose the options which prevent them from being deliberately created.
Secondary equations can be created in two ways:
When a secondary equation is created by the first process, it is quite possible that balancing the new equation will show that the original LHS did not in fact have an irreducible prefix.
When an equation becomes secondary by the second process, it is necessary to consider the overlap between the two left hand sides in order to determine which equation leads to the better reduction of the LHS. MAF assumes that the original equation is better until it has time to consider the overlap.
If a non-geodesic word-ordering is in use it is quite possible that the original secondary equation is much smaller than the equation that arises from considering the overlap between the secondary equation and the primary, and that the resulting new primary equation will be rejected by MAF's heuristics which decide whether or not to allow an equation into the index automaton.
This option only applies when MAF is following plan C: if word-differences are being computed then it is set automatically.
The -secondary n option sets MAF's policy towards secondary equations. It takes a value from 0 to 4. In the value is 0 or 1 secondary equations can only be created through demotion (except that MAF allows RHS correction for -secondary 1). With -secondary 0 secondary equations are always removed as soon as the overlap has been considered, but with -secondary 1 the equation is retained if it had the better RHS.
With -secondary 2 and above secondary equations may be created deliberately, though the extent to which this will happen depends on whether word differences are being computed or not. If word differences are not being computed, the only secondary equations that are created are the right conjugates of primary equations: in other words for each primary equation u*g=v the conjugate equation v*g^-1=u will be created. Such equations may or may not be primary themselves.
The difference between -secondary 2 and -secondary 3 is somewhat technical: in the former case the equation is only partially inserted into the index automaton which performs word reduction, whereas with -secondary 3 the equation is fully inserted (a partially inserted equation will be seen if it occurs as a prefix of the word being reduced, but may be missed otherwise - if an equation is secondary this does not affect whether a word is reducible, though it may effect the final reduction while the system is not confluent). MAF spends a very high proportion of its time performing such updates, so using -secondary 2 option instead of -secondary 3 speeds up the construction of equations but reduces the potential benefit in terms of faster reduction that having secondary equations can bring. If a rewriting system uses a wreath type ordering it will usually be much better to use -secondary 3 than -secondary 2.
-secondary 4 results in the creation of a great many more secondary equations, which are again fully inserted into the tree. Sometimes when a wreath-product type ordering is in effect this is the only way of making reduction feasible: the author knows of an input file where a single incompletely reduced right hand side in an otherwise confluent rewriting system has taken more than 24 hours to reduce - despite the fact that MAF's code for performing word-reduction is very highly optimised.
The default value for -secondary n depends both on the word-ordering, and on whether word differences are being computed. If a wreath type ordering is being used then the default value is 3, otherwise the default value is 2 if word differences are being computed and 1 if not.
If you are using a non-geodesic word-ordering this option can be very important: there are many input files which work very well with -secondary 3 but not -secondary 1, but almost as many for which the opposite is the case. Using -secondary 0 is very risky if you use a wreath type word-ordering. MAF can easily get into a state where word reduction becomes extremely slow. If you feel that MAF is spending too long processing secondary equations then you can try the -weed_secondary option instead
It should only ever be necessary to use this option when a non-geodesic word-ordering is used. It changes how MAF treats an overlap in which the second equation is secondary. MAF's default behaviour is to ignore such overlaps (except perhaps when they arise as special overlaps). If this option is enabled, then MAF will consider such overlaps when it is known that the secondary equation gives a better reduction of its LHS than the corresponding primary does (or at least it did when the overlap between the secondary and its primary was considered). For a secondary equation to be in this state it must be the case that MAF was unable to insert the primary equation arising from the overlap at the time it was last considered. There is no point using this option when you are using a geodesic word-ordering, because it is more or less impossible for there to be any secondary equations in the required state.
This option is not enabled by default. Experiments seem to indicate that it is helpful and unhelpful about equally often, but that the penalty when it is unhelpful is usually bigger than the the benefit when it is helpful. It is possibly more likely to be useful for input files with long relators.
This option alters how MAF deals with secondary equations at the time it considers the overlap with the primary equation. MAF's normal policy is to retain the secondary if it was originally better than the primary, or if both equations lead to the same reduction and the secondary did not need to be repaired. If the -weed_secondary option is set MAF will only retain secondary equations if either the RHS is empty or the secondary equation is better and the necessary primary cannot yet be inserted. So if a geodesic word-ordering is used -weed_secondary will have much the same effect as -secondary 0. This option sometimes improves performance quite a lot when a non-geodesic word-ordering is used, because it can substantially reduce the number of secondary equations that get created. However, like -secondary 0 it can cause word-reduction to become hopelessly slow when wreath type orderings are used.
This option is incompatible with the -secondary 4 option. If that option is in effect secondary equations are always retained, and the RHS is improved if removing the equation would otherwise improve the reduction of the LHS.
Recall that the word-ordering method associated with a rewriting system is said to be geodesic if the normal form for any element is a shortest word. The options described in this section are those which are only ever likely to be useful when the input rewriting system uses a non-geodesic word-ordering, and in may cases the options pertain to code which can in fact only be executed for such orderings. However, in a few cases, the options described apply generally.
Implementing Knuth-Bendix is much more difficult for non-geodesic word-orderings than for geodesic orderings, because the effect of inserting a new equation into the tree is much harder to predict. For, example an equation like a*b=b*a*a may look fairly harmless, but it will result in rewriting a*b^6 as b^5*a^64, so that unless a is known to have finite and small order, it may drastically impact the size of the irreducible words that represent group elements.
When a new equation is discovered, it may happen that it is possible to show that some subword of its left hand side (LHS) is reducible, by multiplying both sides of the equation - either on the left by the inverse of some prefix of the LHS, or on the right by some suffix of the LHS - and then cancelling on the left hand side and reducing, if need be, on the right hand side. This process is known as balancing and will tend to reduce the length of the LHS and increase the length of the RHS. In principle, the balancing of equations is unnecessary, because an equation that is found through balancing would also eventually be found by following the Knuth-Bendix procedure. Nevertheless, for geodesic orderings, it is almost always a good idea to balance equations as much as possible, as this this tends to reduce the number of changes that will need to be made to the rewriting system later on. However, when the word-ordering is non-geodesic it may or may not be a good plan to balance an equation, because it can easily happen that an equation that has been balanced as much as possible will tend to increase both memory usage, and the difficulty of performing word-reduction, and it might well be better to delay discovery of the more aggressively balanced equation until later. For example, when recursive word-ordering is used, it is often the case that the inverse of a generator is found to be reducible to some very long word, so that balancing the equation has the effect of severely increasing the length of the RHS. It might well be the case that later on a shorter reduction is known for the eliminated inverse generator, so that it would be best to delay discovery of the more balanced equation. Therefore, there are a number of options which can be used to control how MAF balances equations, and it may sometimes be worth using one or more of these options.
Note that for a coset system, and where the equation involves the coset symbol, it is almost always possible to move all H-generators from the LHS to the RHS, and this is always done when it is possible.
In MAF balancing is performed by moving one symbol at a time, and balancing may stop either when no more balancing is possible, or when some test involving both the unbalanced and the balanced equation indicates that no more balancing should be performed. MAF will also try to avoid balancing very long equations that are either going to be pooled or discarded.
KBMAG does not balance equations at all when a non-geodesic word-ordering is used.
This option, which should be a number between 0 and 7 controls balancing from the right. It is set to 1 by default, except when the word-ordering method is "rt_recursive" or "rt_wreathprod" when it defaults to 3. If the value is 0 no balancing on the right is performed, and in addition the next option, -left_balancing defaults to 0. In all other cases balancing on the right may be performed. The value of balancing is treated as a bit mask, but only 2 and 4 are significant. Therefore values 2 and 3, 4 and 5, and 6 and 7 behave in the same way. If the 2 bit is set, a right balancing step will not be performed if the total length of the balanced equation is longer than the current "visible limit" for equations but the unbalanced equation is not. If bit 4 is set a balancing step will not be performed if the balanced equation is longer than the "visible limit" and the new RHS is longer than the new LHS and (new_rhs_length - new_lhs_length) > (old_rhs_length - old_lhs_length). Therefore 1 is the most aggressive value for this option.
You may like to note that MAF will never perform a right balancing step if the new LHS is greater than the new RHS prior to the RHS's being reduced, because the balanced equation will be the next equation to be considered.
-left_balancing nThis option, which should be a number between 0 and 3 , controls balancing from the left. The default value for the option is 1 unless one of the rt_ word-orderings is used, in which case it is 3, but, if -balancing 0 was specified then -left_balancing also defaults to 0. If left_balancing is 0 no left balancing is performed, 1,2,3 are progressively more aggressive in the amount of balancing performed.
"unbalancing" is an option that is on by default, except for coset systems where it is not available at all, but which can be turned off with -no_unbalance. Suppose MAF has discovered a new equation, and has decided to insert it into the rewriting system (rather than discarding it, or placing it in the pool). If at that point the LHS is shorter than the RHS, and "unbalancing" is enabled, then MAF will move symbols from the RHS to the LHS by multiplying on the right by the inverse of the RHS for as long as it can do so without the LHS becoming reducible. It then inserts this equation into the tree instead. The idea is to mitigate any bad effect that inserting the more balanced equation immediately would have. Eventually either conjugation or normal Knuth-Bendix will find the more balanced equation.
The -swap_bad option enables another tactics for dealing with equations with a longer RHS than LHS which must be inserted into the tree. Instead of moving symbols from the RHS to the LHS, MAF attempts to make the equation over-balance by multiplying on the right by the inverse of the last symbol on the LHS. If by doing so it is possible to make the RHS later in the word-wording than the LHS before the RHS becomes reducible, then MAF inserts this swapped equation instead before inserting the original equation. One might imagine that this would be helpful if MAF is about to insert an equation such as A=a^26], but does not yet know that a^27=IdWord.
However, in practice this option does not often seem to be beneficial, so it is turned off by default.
The -collapse n option, which must be given a value from 0 to 2, and which is 0 by default enables some equations which might otherwise be pooled or discard to be inserted into the rewriting system instead. These equations are certain to eliminate some part of the tree, and so may help to promote a collapse. Using -collapse 1 is quite often helpful, and unlikely to be very harmful. -collapse 2 will allow potentially allow equations with a long RHS to be inserted much sooner than they otherwise would have been. -collapse 2 usually had a bad effect.
When new equations are inserted into a rewriting system it frequently happens that some of the existing equations become invalid because either the right hand side or a subword of the left hand side are now reducible. MAF tries to repair such equations as soon as possible. When a non-geodesic word-ordering is in use this can be difficult, and one of the tactics MAF usually uses in this case is to repair right hand sides which appear to be "better" very early on in this process. MAF regards an RHS as "better" if the new RHS is shorter than the LHS, or the old RHS was longer than the LHS and the new RHS is shorter than the old one.
The -no_early_repair disables this favouritism towards shorter right hand-sides. This is almost always a bad idea.
When non-geodesic word-ordering is used it can easily happen that one side of an equation is much longer than the other. For example, when recursive orderings are used it is common for inverse generators to be eliminated. It sometimes happens that such an equation gets stuck in the pool for a long time. One way to prevent this from happening is to try the -collapse 2 option. Another is to use this option. If either side of an equation is no more than this value, it will be added to the tree. The default value of this option is 0: any equation with an empty RHS is always added to the tree.
Although it can be frustrating to know that an equation with a short LHS is in the pool, if the RHS is long it is generally best to leave it there for a while. Setting this option rarely has a good effect.
If, for whatever reason, you believe that MAF is producing incorrect results for a particular input file for a group, and you have available a word-difference machine that solves the word problem for this input file, then you can tell MAF to check each equation it produces against this FSA by using the -check fsaname option. In the unlikely event that an equation that is not recognised by the FSA is produced, MAF will terminate with an internal error. If you then send both the input file and the validating FSA to the author he will do his best to investigate to discover if MAF really is producing incorrect results, or if in fact the error is in the supposedly correct FSA you have used for validation. The author has not had cause to use this option since MAF was publicly released.
The table below lists all the options that may affect processing significantly. Options that are only accepted for KBMAG compatibility purposes are not listed. Many of the options are only relevant in specific circumstances, or relate to specific areas of processing within MAF: the second column of the table indicates this. Almost any option can have a drastic effect (either good or bad), on the amount of memory and the amount of time MAF uses in its computations. The third column indicates how useful/important the option is and any caveats.
| Option | Importance/Caveats |
|---|---|
| -balancing n | Sometimes useful, unpredictable |
| -check fsaname | Used for debugging purposes only |
| -check_inverses | Rarely useful, tends to degrade performance slightly (but severely with wreath type orderings). Increases memory usage |
| -collapse n | Rarely useful, tends to degrade performance, often has little effect |
| -confluent | Important, Often useful, but must be used with care |
| -conjugation n | Sometimes useful, but default value (1) usually works well |
| -consider_secondary | Occasionally useful. Unpredictable effect |
| -cos | N/A |
| -dense_rm | Rarely relevant - only applies to rewriting systems with large alphabets (more than 8 generators) |
| -detect_finite_index | Important, often useful |
| -eliminate | Rarely useful, it is usually be better to use simplify instead |
| -expand_all | Sometimes necessary, but usually degrades performance |
| -extended_consider | Rarely useful, tends to degrade performance slightly (but severely with wreath type orderings), but also only likely ever to be beneficial with wreath orderings |
| -fast | Sometimes useful, but when it is -no_kb is usually better |
| -filters n | Unlikely to have much effect |
| -force_differences | Useful as part of a preliminary investigation |
| -force_multiplier | Rarely useful, possibly risky |
| -ignore_h_length | Often essential for coset systems with named subgroup generators. Tends to improve running time but increase relator lengths in any subgroup presentation generated |
| -left_balancing n | Occasionally useful. Unpredictable effect |
| -max_equations n | Occasionally useful |
| -max_time n | Occasionally useful |
| -min_time n | Unlikely to be useful |
| -no_early_repair | Rarely useful. Unpredictable effect |
| -no_h | Often useful for coset systems using named generators. Usually used in combination with -ignore_h_length, in which case it tends to mitigate the bad effects of the latter option on the subgroup presentation. |
| -no_hd | Usually enabled automatically when needed |
| -no_kb | Very useful but risky strategy option |
| -no_pool | Sometimes useful but risky strategy option |
| -no_pool_below n | Rarely useful |
| -no_prune | Occasionally useful |
| -no_throttle | Occasionally useful, risky |
| -no_unbalance | Rarely useful, unpredictable but usually bad effect |
| -no_validate | Risky, since may result in an incorrect automatic structure |
| -no_wd | Important, recommended if you do not want an automatic structure |
| -no_weak_acceptor | Occasionally useful if MAF runs into trouble when building an automatic structure |
| -partial_reductions n | Occasionally useful,unpredictable effect |
| -pool_above n | Often useful for input files with long axioms |
| -probe_style n | Occasionally useful |
| -prove_finite_index | Sometimes useful, risky |
| -repeat n | Rarely useful |
| -resume | Can be useful when automatic structure is wanted |
| -schreier | N/A |
| -secondary n | Sometimes useful |
| -slow | Occasionally useful |
| -special_overlaps n | -special_overlaps 0 often beneficial, but has unpredictable effect |
| -strategy n | Important |
| -swap_bad | Rarely useful |
| -tight | Occasionally useful |
| -timeout n | Rarely useful |
| -validate | Important in theory. May be better to invoke gpaxioms separately |
| -ve | N/A |
| -vwd | N/A |
| -wd | Needed to force construction of automatic structures for non-geodesic orderings when system will not be confluent |
| -weed_secondary | Occasionally useful |
| -work_order n | Often useful, unpredictable effect |
In order to maintain compatibility with KBMAG, MAF includes five utilities that would otherwise be superfluous, namely: kbprog, autgroup, gpmakefsa, kbprogcos, autcos. The MAF versions of these utilities are, broadly speaking, all just variants of automata, in which some options have different default values from normal, and an internal "compatibility flag" is set, which makes minor modifications to the output. None of these programs has any facilities not provided in automata. They are provided solely with the aim of improving compatibility between MAF and KBMAG, and for the benefit of users who are familiar with KBMAG. They can all safely be deleted if you do not have any special requirements for compatibility between MAF and KBMAG. A command line that invokes one of these programs should produce equivalent output, whether it is given to the KBMAG or the MAF version of the utility. If such a command line is changed to invoke MAF's automata instead it will still work, but some extra files may be created, and the names used for any "provisional" output files will differ.
automata includes all the functionality of KBMAG's separate autgroup, kbprog, gpmakefsa, gpaxioms, autcos (including gpsubwa and gpsubpres), and kbprogcos, and gpminkb and a little more besides. Unless you require strict compatibility with KBMAG, there will usually be no need to use these compatibility utilities, once you are used to the slightly different way in which automata is used.
This program is identical to automata except that:
This program is identical to autgroup except that the -cos option is automatically on.
This program is identical to autgroup except that the -nokb option is turned on by default, and it will "import" at least one pre-existing difference machine if such a machine exists, whereas automata generally behaves as though it is being run for the first time against any input file it is asked to work on, even if it in fact has already completed successfully previously. gpmakefsa will exit with an error message if no word-difference machine has been computed for the input file. The detailed operation of gpmakefsa is rather different in MAF from KBMAG. MAF expects to have available the equations that prove word-differences, and in their absence is liable to remove genuine word-differences when correcting the difference machines unless the multiplier passes the checks first time. It is not at all a good idea to run this program unless absolutely necessary. It is not used at all by the MAF version of autgroup and autcos, which are executables rather than shell scripts, and it would probably be a bad idea to replace the KBMAG version with the MAF version when using the GAP KBMAG package.
This program is similar to automata except that the -nowd option is the default, and word difference calculations must be turned on explicitly with -wd. It will exit without building any automata other than the confluent rewriting system and its index automaton (if the presentation is confluent) or the provisional difference machines, if the -wd option is specified. This program is described in more detail below.
This program is almost identical to the MAF version of kbprog, except that the -cos command line option is supplied automatically, so that the program always expects to process a coset system and adjusts its output and methods accordingly. (It does not matter if this option is supplied again).
kbprogcos accepts one special option. -f is treated as a synonym for -detect_finite_index. No other MAF components recognise this option with that meaning: most will treat it as the standard KBMAG option to request minimisation using files, and will therefore ignore it.
Other than that the MAF command line options for kbprogcos are identical to those for kbprog.
Fuller descriptions of the KBMAG options accepted in the MAF version of KGBMAG's two key programs gpmakefsa and kbprog are given below.
gpmakefsa [loglevel] [format] [-cos] groupname subgroup_suffix
Construct the word-acceptor and general multiplier finite state automata for the automatic group or automatic coset system, of which the rewriting system defining the group is in the file groupname or the coset system is in groupname.cosname.
-diff1These options are ignored. MAF will make intelligent decisions about how to build the word-acceptor and multiplier.
These options are ignored. In the KBMAG version of gpmakefsa the -m maxeqns option specifies an upper limit on the number of equations that are processed when correcting the difference machines during a failed correctness test, but the documentation incorrectly describes the -me maxeqns option, which is not recognised, as having this effect.
MAF accepts, but effectively ignores, both options. In MAF as many equations as can be found are processed, but the correctness test is aborted once it appears that all the new equations that are being discovered would be recognised by the updated word difference machine.
This option is ignored. In the KBMAG version of gpmakefsa this puts an upper limit on the number of word-differences allowed after the correction. There is no good reason to have such an option.
The information in this section applies equally to the MAF version of kbprogcos.
kbprog [loglevel] [-ve] [-vwd] [-r | -ro] [-both] [-me n] [-mlr l r] [-mo n] [-mt n] rwsname
The KBMAG version of kbprog has zillions of options. Only those that are actually supported in the MAF version are listed above. Remember that kbprog also supports all MAF's options for automataas well. In the detailed description that follows other KBMAG options that are accepted for compatibility purposes, but ignored, are also listed. In MAF kbprog is a version of automata that is modified so that it will only generate the automata that the KBMAG version of kbprog is capable of producing. This means that it will output either a confluent rewriting system, or word difference machines, or possibly both. However there are some differences in the output files:
The input file is shown as rwsname because kbprog accepts coset systems. In fact it also accepts the -cos option and the subsuffix, and in this case behaves identically to the MAF version of kbprogcos apart from the special handling of -f that is in the latter.
In addition to the options listed here the MAF version of kbprog also accepts the options accepted by the automata program.
This option has no effect. In the KBMAG version of kbprog it controls how often the set of equations is tested for confluence. In MAF this option is not relevant because the algorithm which finds overlaps is a test for confluence. A sign that a system is about to become confluent is that MAF is suddenly able to process very large numbers of equations in a very short time.
This option has no effect. Previous versions of the MAF documentation implied MAF tried to implement this option, but this was not in fact the case.
This option is essentially synonymous with the -max_equations n option. However, since kbprog never builds automatic structures it will always behave as it does in automata when plan C is being followed. However, when word differences are being computed kbprog may take quite a while to stop if you use this option, because it might be difficult for MAF to construct word-difference machines that satisfy MAF's minimum consistency requirements.
KBMAG's kbprog sets the very low default limit on the number of equations of 32767. In MAF kbprog's default behaviour is not to limit the number of equations. This option can also be set using the field maxeqns in the input file.
If this is used, then so far as possible only equations in which the left and right hand sides have lengths at most maxlenleft and maxlenright, respectively, are kept. MAF cannot always respect this option because it can cause inconsistencies in its internal data structures that it will not allow. In fact it is clear that even KBMAG does not always respect it, since on several of the examples where it is used several of the equations in the confluent system exceed the limits. With MAF, this option is not recommended. The author does not know of any input files in which using this option improves MAF's behaviour, and knows of several where it is very counter-productive. If you have used the corresponding option in KBMAG and now want to process the same input file in MAF then first try to run without this option. Only try with this option if necessary. In the author's limited experience values that work with KBMAG are always too small in MAF. Values that are each twice what was used in KBMAG, or equal to the correct maximums as given by the confluent rewriting system, if known, whichever is the greater, may work.
This option can also be set as a field in the input file. The syntax for this is:
maxstoredlen := [maxlenleft,maxlenright] is recognised by KBMAG, but ignored (with a warning) by MAF.
maf_maxstoredlen := [maxlenleft,maxlenright] sets the option for MAF, but is ignored by KBMAG.
The Knuth-Bendix procedure works by forming a word which contains two overlapping reducible words, so that if the reductions are not yet consistent with one another two different reductions for the same word will arise, giving rise to a new equation. This option limits the maximum length of this "overlap" word, and once all possible overlaps up to this length have been considered MAF will behave as though the rewriting system was confluent, even though it is not.
The only good reason for using this option in MAF, is when you know that MAF will not be able to find correct automata, and you are willing to accept provisional automata. Even quite a "short" word-acceptor can usually eliminate most reducible words, so that a program that needs to enumerate group elements, and does not mind if occasionally the same element is enumerated twice, but would prefer to enumerate each element as few times as possible, can benefit from having such an acceptor available.
This parameter can also be set as the field maxoverlaplen in the input file.
This option does nothing. In KBMAG it controls the maximum length a word can reach. In MAF the limit is 2^16-3 = 65533 symbols and this cannot be changed, except by rebuilding MAF with a different value for the MAX_WORD constant, and a change in the definition of the Word_Length type. You are recommended not to try to do this, as if a word ever reaches such an extraordinary length MAF will probably become extremely slow and encounter stack overflow errors. This limit is only likely to be exceeded if you are using a wreath-product type word-ordering.
This option does nothing. In KBMAG it controls the maximum number of states in the index automaton.
This option is synonymous with the -min_time n option of automata: when word-differences are being computed,unless confluence is achieved, kbprog will not abort until at least the specified amount of time has elapsed since Knuth-Bendix expansion began.
This option is ignored, but is accepted for KBMAG compatibility. There is no special reason in MAF to limit the number of word differences. However, if a group has more than around 4000-5000 word differences then it is highly unlikely to be automatic unless it turns out to be finite, and even in this case the multiplier may well be too large to compute, and the index automaton will be a better choice for doing word reduction.
In MAF, this option is identical in effect to the -resume option of automata.
This option does nothing. In the KBMAG version of kbprog it enables the "Rabin-Karp" algorithm for word-reduction. In MAF very long equations are are not usually available for performing reductions. However, if word differences are being computed then unusually long words are reduced with the word difference machine.
In MAF the -ro option is identical in effect to the -resume option of automata.
This option does nothing. In the KBMAG version of kbprog it causes equations to be output in order of increasing length of their left hand sides. MAF always outputs equations in BFS order.
This option does nothing. In the KBMAG version of kbprog it controls the frequency at which equations are tidied. This option can be specify in input files as tidyint := n
The following are accepted as options by the KBMAG version of kbprog but are not recognised by the MAF version. This list is not guaranteed to be complete!
-lexIn the KBMAG version of kbprog these options change the word-ordering from the one specified in the input file. In the MAF version using these options will cause MAF to exit immediately with an error message.