The table below lists the various types of output file for coset systems, and the circumstances under which they are produced. The details given apply to a coset system called group.cos. This is the coset file that will be analysed if automata is started with any of the following command lines:
automata -cos group [sub]
or
automata -cos group cos
or
automata group.cos
In the first command line sub is shown in square brackets to indicate that it is optional. In fact if the substructure file is called group.sub then there is of course no need to supply this; but if you have multiple substructure files group.sub1, group.sub2,... then it would be required, and as described in Coset system filenames, the name of the coset system would be altered accordingly too.
| File name | File description | When produced |
|---|---|---|
| group.cos.akbprog | This is a rewriting system for the coset system which contains at least one equation for every transition that appears either in the word-difference machine of the MIDFA general multiplier for the coset system, or the .midiff2c word-difference machine. It also contains any axioms which were not eliminated. The automatic structure can be reconstructed quickly from this rewriting system. This rewriting system is not canonical - running automata with different options might result in different equations appearing in this rewriting system. | When automata has proved a coset rewriting system automatic but not confluent. |
| group.cos.cosets | This is the coset table for a finite index subgroup. | When automata has proved a subgroup has finite index. This automaton can also be computed using gptcenum -table |
| group.cos.fastkbprog | This is a "fast" rewriting system for the coset system. 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 (possibly involving the coset symbol), and u and v have no common cancellable prefix or trailing subword. If the coset system is automatic this rewriting system will contain at least one equation for every transition in the .midiff2c word difference machine (by which is meant that the every transition in this word-difference machine is taken for at least one equation when the equation is used as input to the word-difference machine). Currently this rewriting system is not canonical - running automata with different options might result in different equations appearing in this rewriting system. | When automata has proved a coset rewriting system confluent. |
| group.cos.fastreduce | This is the index automaton for group.cos.fastkbprog | When automata has proved a coset system confluent. |
| group.cos.gm | This the determinised version of the coset general multiplier. In the determinised multiplier, a label can include words that are not equal in the group, something that does not happen either with automatic structures for groups, nor in the .migm form of the coset multiplier. This FSA is canonical. | If coset system is proved automatic by automata, autgroup or autcos. See the entry below for group.cos.migm for reasons why this file might not be produced. |
| group.cos.kbprog | This may either be the minimal confluent rewriting system for the coset system, or a partially confluent one, or, if you are using either kbprog or kbprogcos, a provisional rewriting system. | When either automata, or kbprog/kbprogcos (without -wd or with -both) have proved a coset system confluent or partially confluent (with -detect_finite_index or -prove_finite_index options). |
| group.cos.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.cos.wa, but every prefix of u is accepted, and v is accepted by group.cos.wa, and for which u=v is a true equation, and in which u,v have no common prefix. | If coset system is proved automatic by automata. |
| group.cos.midiff1c | This is the FSA that contains all the word differences needed for the (possibly infinite) minimal confluent coset rewriting system, and just the transitions that arise in this system. This FSA is not canonical. For an explanation of this refer to the .migm entry. Note that in the case where subgroup generators are named MAF usually labels the initial states of this and every other word-difference machine with both a G-word and an H-word. KBMAG cannot cope with word-difference machines labelled like this. Therefore, when you use a KBMAG compatibility program the word-difference machines are only labelled with G-words. | If coset system is proved either confluent or automatic by automata, or by autgroup/autcos with -gpminkb option, or you run gpminkb against a coset system for which an automatic structure has been computed. |
| group.cos.midiff2c | This is the FSA that contains all the word differences needed for the coset reduction recogniser, and just the transitions that occur in that word-difference machine. If the input file for the group uses a geodesic word-ordering this is almost the same as the word-difference machine for the general multiplier, but a non-geodesic ordering is used there will be some differences. This FSA is not canonical. For an explanation of this refer to the .migm entry. The states are labelled in the same way as for group.cos.midiff1c. | If coset system is proved automatic by automata, or autgroup/autcos with -gpminkb option, or you run gpminkb against a coset system for which an automatic structure has been computed. |
| group.cos.midiff2 | This is the FSA that contains all the word differences needed for the coset general multiplier, and all possible transitions between them, not just transitions that are actually needed. This FSA may contain word-differences that are not needed for coset reduction but are needed for ordinary reduction, but it does not contain any word differences that do not genuinely arise in one of these two ways, and it will not contain any extra word-differences if -detect_finite_index or -prove_finite_index showed that the subgroup had finite index. In KBMAG this FSA often contains spurious word differences. This FSA is not canonical. For an explanation of this refer to the .migm entry. The states are labelled in the same way as for group.cos.midiff1c. | If coset system is proved automatic. |
| group.cos.migm | The MIDFA coset system general multiplier. This is the FSA that contains an accept state labelled with x equal to the identity element or a generator, reached from an initial state labelled with h, for every coset-reduced u and v, and every x, for which u*x=h*v is a true equation. MAF labels initial states with both the best-known G-word and the best known H-word for the element h, (unless you use a KBMAG compatibility program) whereas KBMAG only uses a best known G-word. This FSA is not canonical because it can easily happen that there is more than one initial state corresponding to the same group element. This can happen if MAF has been able to show that two distinct words, which are in fact equal as group elements, are members of the subgroup, but MAF has not realised that they are equal. When this happens the presentation computed for the subgroup is likely to be "difficult". | If a coset system is proved automatic. If a group is proved finite, then any coset system for the group is certainly automatic, but it can happen that the multiplier would have an extremely large number of states before minimisation, (and possibly afterwards as well). In this one case MAF does not generate the general multiplier that is known to exist. If a coset system is proved confluent but the subgroup does not have finite index, then the coset system might not be automatic. MAF will perform a certain number of iterations to try to prove it automatic, but if number of word differences continues to increase it will give up because it probably is not. |
| group.cos.minkb | This is the FSA which reaches its single accept state, for just those word pairs (u,v) in which u is accepts by group.cos.minred and v by group.cos.wa, and for which u=v is a true equation. | If coset system is proved automatic by automata, or autgroup/autcos with -gpminkb option, or you run gpminkb against a coset system for which an automatic structure has been computed. |
| group.cos.minred | This the FSA that accepts minimally coset reducible words. automata will calculate this to prove that the minimal confluent rewriting system is not finite, or as an additional check that a confluent system has been found correctly. A word is minimally coset reducible if no prefix is coset reducible and no trailing subword is reducible as a group element. | If coset system is proved either confluent or automatic by automata, or autgroup/autcos with -gpminkb option, or you run gpminkb against a coset system for which an automatic structure has been computed. |
| group.cos.pkbprog | This is a provisional rewriting system for the coset system. It contains all the equations that were known and not pooled for words which were thought to be minimally reducible at the time MAF was interrupted. kbprog and kbprogcos will use the .kbprog suffix for this file (and .reduce for the corresponding index automaton). | When automata was interrupted while trying to prove a minimal rewriting system confluent. |
| group.cos.pmidiff1 | Provisional primary difference machine for the coset system. This contains all the word differences and transitions between them that were thought to be needed for the equations in the minimal rewriting system at the time MAF terminated. There may be equations that the provisional complete difference machine can prove that this cannot. In fact this is more often than not the case. If you use kbprog/kbprogcos with -wd option or autcos then this file is given the suffix .midiff1 for compatibility with KBMAG. The states are labelled in the same way as for group.cos.midiff1c. | If automata is interrupted while trying to prove a coset system automatic. |
| group.cos.pmidiff2 | Provisional complete difference machine. It contains all the word differences and transitions between them that were known at the time MAF exited. The states are labelled in the same way as for group.cos.midiff1c.
If you use kbprog/kbprogcos with -wd option or autcos then this file is given the suffix .midiff2 for compatibility with KBMAG. | If automata is interrupted while trying to prove a coset system automatic. |
| group.cos.preduce | This is an index automaton for the provisional rewriting system group.cos.pkbprog. | When automata was interrupted while trying to prove a minimal rewriting system confluent. |
| group.cos.reduce | This is the index automaton for group.cos.kbprog, usually a minimal confluent rewriting system. | When automata, kbprog or kbprogcos have also generated the file group.cos.kbprog. |
| group.cos.rr | This, "the reduction recogniser" is the automaton which reaches its single accept state, starting from an initial state labelled h for just those word pairs (u,v) in which u is not accepted by group.cos.wa, but every prefix of u is and v is accepted by group.cos.wa, and for which u=h*v is a true equation. It is the automaton from which group.cos.midiff2c is computed. | When automata has proved a coset system automatic. |
| group.cos.wa | This the coset word-acceptor. It is an acceptor in G-words for the coset representatives. It is not the acceptor for the possibly infinite minimal confluent rewriting system for the entire coset system. The size of the accepted language of this automaton is the index of the subgroup. | If coset system is proved either confluent or automatic by automata, or autgroup/autcos. |
| group.sub.pres | This is a file containing a presentation for the subgroup in the form of GAP source code. | When automata or autgroup/autcos with -p or -subpres have computed a subgroup presentation. |
| group.sub.rws | This is the rewriting system for the subgroup, and so contains a presentation for the subgroup. It can be used as an input file directly, but it will often be best to use simplify to eliminate redundant generators and relators first. | When automata has computed a subgroup presentation. |
| group.sub.wa | This is the subgroup word-acceptor for the subgroup. | When automata has found a subgroup word-acceptor and proved it correct. |
Several of the automata above can be used for reducing words u to the unique minimal coset representative v in the group under the chosen word-ordering, that is v is the least word in the word-ordering such that Hu and Hv are equal as sets. In particular, this enables the generalised word-problem to be solved for the subgroup H of G. See reduce for further information.