The following table summarises the names of all the output files that might be produced for an input file for a group or monoid named group, what the files are, and the circumstances in which they are produced. In the "When produced" column, the formula "if input file is proved automatic" is used several times. This means that MAF has been able to generate an automatic structure, and has been able to verify that the general multiplier is closed for each multiplier. It can happen that MAF is able to prove that such a structure exists, but that it is beyond its capacity to actually compute it. Similarly, the formula "proved confluent" mean that MAF has succeeded in finding a confluent rewriting system. In theory, MAF might discover that such a system exists, without being able to find it, but this will be, we hope, a very rare occurrence.
For completeness, various suffixes used with automata for coset systems are also shown here. Such files are described more fully in the equivalent of this table that appears in Output files (coset systems). Subgroup and coset automata can be recognised in the table below by the fact that the filename is shown as cosname rather than group.
| File name | File description | When produced |
|---|---|---|
| group.akbprog | This is a rewriting system for group from which the automatic structure can be reconstructed quickly. It contains at least one equation for every transition in the word-difference machine of the general multiplier. This rewriting system is currently not canonical - running automata with a different options might result in a different set of equations appearing in the file. A canonical version of it surely exists, and MAF will hopefully generate it one day. | When automata has proved an input file automatic but it is not confluent. |
| group.diff1 | This FSA is produced by KBMAG. MAF does not produce this FSA, unless a KBMAG emulation program is used. If MAF's autgroup is used and completes successfully then this file is the same FSA as group.diff1c; this will also be the case with MAF's kbprog -wd when a confluent rewriting system is found. If one of these programs is interrupted then the file is still produced but is equivalent to the group.pdiff1 file which automata generates if it is interrupted. | kbprog (with -wd) and autgroup will produce this file, both in KBMAG and MAF. |
| group.diff1c | This is the word-difference machine of the (possibly infinite) minimal confluent rewriting system for the input file. | If input file is proved automatic or confluent by automata (without -nowd and when word-differences can be computed) or automatic by autgroup with -gpminkb and is also output by gpminkb when run against an input file for which the automatic structure has been computed. |
| group.diff2 | This FSA is the word-difference machine that contain all the word-differences needed for the general multiplier, and the reduction recogniser, and all possible transitions between these, not just transitions that actually occur in some equation. In MAF this FSA is guaranteed to be correct if automata completes successfully (i.e. it really does contain all such word-differences and there are no spurious word-differences). In KBMAG it often contains spurious word-differences. See also group.pdiff2. | If input file is proved automatic. |
| group.diff2c | This is the FSA that contains all the word-differences needed for the (possibly infinite) directly reducing confluent rewriting system, and just the transitions that occur in these equations. If the word-ordering is geodesic then it also contains all the transitions needed for the general multiplier. An FSA with this name is also produced by KBMAG's version of gpminkb, but is a different FSA, which is useless for any purpose other than rebuilding the general multiplier (and has the TRIM flag set incorrectly). | See entry for group.diff1c. |
| group.fastkbprog | This is a "fast" confluent rewriting system for group. It contains all the equations in the minimal confluent rewriting system, and as many other equations as MAF has discovered of the form [u*g,v] where u and v are accepted words, g is a generator, u*g=v is a true equation, and u and v have no common cancellable prefix or suffix. If group is automatic this rewriting system will contain at least one equation for every transition in the .diff2c word difference machine (by which is meant that the every transition in this word-difference machine is taken by at least one equation when the equation is used as input to the word-difference machine). This rewriting system is currently not canonical - running automata with a different options might result in a different set of equations appearing in the file. | When automata has proved an input file confluent. |
| group.fastreduce | This is the index automaton for group.fastkbprog. | When automata has proved a rewriting system confluent. |
| group.geodiff | This is the geodesic word-difference machine for group; like the group.geopairs it accepts all equal pairs of geodesics, but it may accepts other equal words as well. | When gpgeowa has proved a group word-hyperbolic. |
| group.geopairs | This is the geodesic pair recogniser for group. It accepts all pairs of words that are equal as group elements and which are shortest words for the corresponding group element. In other words it is the identity multiplier for the geodesic automatic structure | When gpgeowa has proved a group word-hyperbolic. |
| group.geowa | This is the geodesic word acceptor group for group. | When gpgeowa has proved a group word-hyperbolic. |
| group.gm | The general multiplier. This is the FSA that which accepts all those pairs of reduced words (u,v), at an accept state labelled with all those words x (with x either IdWord or a generator), for which u*x = v is a true equation. MAF makes much more use of this FSA than KBMAG. For example, in the absence of a confluent rewriting system, it is the preferred method of performing word reduction. | If input file is proved automatic. If an input file is proved confluent and finite, the group is automatic, but it can happen that the multiplier is too large to compute. In this case MAF does not generate the general multiplier. If a group is proved confluent and infinite, then the group may or may not be automatic. MAF will perform a certain number of iterations to try to prove it automatic, but if the number of word-differences continues to increase it will give up because it probably is not. |
| group.kbprog | This may either be the minimal confluent rewriting system for the or, if you are using kbprog, a provisional rewriting system. | When either automata, or kbprog (without -wd or with -both) have found a confluent rewriting system for the input file. |
| group.maxkb | This is the FSA which reaches its single accept state, for just those word pairs (u,v) in which u is not accepted by group.wa, but every prefix of u is and v is accepted by group.wa, and for which u=v is a true equation, and in which u,v have no common prefix or suffix. The accepted language of this automaton is the set of all equations which ought to be in group.fastkbprog. | When automata has proved an input file automatic. |
| cosname.midiff1 cosname.midiff1c cosname.midiff2 cosname.midiff2c cosname.migm cosname.pmidiff1 cosname.pmidiff2 | These are "MIDFA" automata produced during the construction of an automatic structure for a coset system | All these automata are produced when automata or one of the KBMAG compatibility programs is processing a coset system. See Output files (coset systems) for details. |
| group.minkb | This is the FSA which reaches its single accept state, for just those word pairs (u,v) in which u is accepted by group.minred, and v by group.wa, and for which u = v is a true equation. | See entry for group.diff1c. |
| group.minred | This the FSA that accepts minimally reducible words. Elsewhere in MAF documentation this is called the L1-acceptor automata will compute this to prove that there is no finite confluent rewriting system, or as an additional check that it has been found correctly when there is. | If input file is proved automatic or confluent by automata or automatic by autgroup with -gpminkb and it is also output by gpminkb when run against an input file for which the automatic structure has been computed. |
| group.near_geodiff | This is the word-difference machine for the geodesic general multiplier of group, which means that it accepts all pairs of the form (u,v) where u and v are geodesics and u^-1*v is the identity element or a generator, but it usually accepts some other pairs of words as well. The accept states are labelled by the word-difference as for a multiplier. | When gpgeowa with the -near option has proved a group word-hyperbolic. |
| group.near_geopairs | As constructed by MAF this is the general multiplier for the geodesic automatic structure for group (except that reducible generators are omitted). Its accepts a pair of words (u,v) at a state labelled by g with g a generator or the identity if and only if u and v are geodesics and u*g = v is a true equation in the group. KBMAG's version of gpgeowa constructs the same FSA if the -n option is used, except that the states are not labelled. | When gpgeowa with the -near option has proved a group word-hyperbolic. |
| group.pdiff1 | Provisional primary word-difference machine. This contains all the word-differences and transitions between them, thought to be needed for the equations in the minimal confluent rewriting system at the time MAF exited. There may be equations that the provisional complete word-difference machine can prove that this machine cannot. In fact, this is more often than not the case. This FSA is given the .diff1 suffix by KBMAG, and also by MAF's KBMAG compatibility programs kbprog (with -wd) and autgroup | If automata is interrupted while trying to prove an input file automatic. |
| group.pdiff2 | Provisional complete difference machine. It contains all the word differences and transitions between them that were known at the time MAF exited. KBMAG uses the .diff2 suffix for this FSA, as do MAF's KBMAG compatibility programs autgroup and kbprog. | If automata is interrupted while trying to prove an input file automatic. |
| group.preduce | This is the index automaton for group.pkbprog. | When MAF has generated group.pkbprog and word-differences are not being computed |
| group.reduce | This is the index automaton for group.kbprog. | When MAF has generated the file group.kbprog |
| group.rr | This, "the reduction recogniser" is the FSA which reaches its single accept state, for just those word pairs (u,v) in which u is not accepted by group.wa, but every prefix of u is and v is accepted by group.wa, and for which u=v is a true equation. It is the FSA from which MAF's group.diff2c FSA is computed. | When automata has proved an input file automatic. |
| group.wa | This the word-acceptor for the group. | If input file is proved confluent by automata, or proved automatic by automata or autgroup |
Several of the automata above can be used for reducing words to their unique minimal representative in the group or monoid described in the input file under the word-ordering specified there. See reduce for further information.