MAF for Subgroups and Cosets

Introducing Coset Rewriting Systems

So far we have seen how to use MAF in order to try to solve the word problem for a group or monoid. In the cases where we have done so we are able to say whether two words are equal or not. However, one is frequently concerned with the properties of subgroups of a group. We may want to know what the structure of the subgroup generated by a certain set of elements of the group is, and which members of the original group are actually members of it, and, for the elements that are not, whether two elements are in the same (right) coset of the subgroup. Having a solution to the word problem for the group is not enough to let us solve these problems. The coset membership problem is called the generalised word problem: subgroup membership is then just the special case of whether a word belongs to the same coset as the identity. This problem can be investigated, though not necessarily solved, for a particular group and subgroup, through the use of a coset rewriting system. Coset rewriting systems, or coset systems for short, are very similar to the monoid and group rewriting systems we have been dealing with up until now.

Creating a Coset Rewriting System

The main difference between coset rewriting systems and the rewriting systems previously considered, lies, from the MAF user's point of view, in how they are set up in the first place: owing to their greater complexity, it is not advisable to create them by "hand editing" an existing file. Instead they are created by MAF itself, based on an ordinary rewriting system for a group or monoid, and a substucture file, both of which the user must create. MAF then constructs the input coset rewriting system from these files. A substructure file should always describe a subgroup, because the notion of cosets is somewhat meaningless for submonoids (as will be explained shortly), so it may be referred to as a subgroup file, even though, in the case of a monoid, it would be up to the user to verify that the given set of substructure generators did in fact generate a group and not just a monoid (though MAF may detect this in some cases).

Cosets of submonoids of monoids do not in general behave in a manner suitable for use with coset rewriting systems (or much else for that matter). For example, if L is a submonoid of M and xL, then it does not even follow that Lx=L - it may be a proper subset of L: as an example consider the monoid of positive integers under multiplication, and any submonoid of the form {N*n ∪ 1}.

How Coset Systems are Processed in MAF

As, in the case of rewriting systems for groups, MAF tries to generate both a confluent rewriting system and an automatic structure, so, in the case of coset systems, it usually tries to generate both a confluent coset system and an automatic coset structure, and as is the case with rewriting systems for groups, either, neither, or both of these, may exist. There are actually three different types of coset system. The first two types of coset system are supported by both KBMAG and MAF. The third type is new to MAF, and will be explained later. To understand the difference between the first two types we first need to explain what we mean by a coset equation:

KBMAG can only produce an automatic coset system for a coset rewriting system that uses coset equations of the second type. MAF however, can produce automatic coset systems with any type of coset system, and can also generate a subgroup presentation and subgroup word acceptor equally well with either kind of coset system. However, it can only generate a presentation using the specified subgroup generators for the second type of coset system, so it is to this second type that most attention will be paid in what follows. Nevertheless, there are situations where the first type of system may well give better results, for example where the subgroup has a very large number of generators, as might be the case if you are trying to find a subgroup such as the subgroup generated by all words of the form w^4. Additionally, it can happen that the H words appearing in the prefix of the RHS of equations involving the _H word become extremely long, and in these cases it is usually better to use the first type of coset system. So, unless you do want to generate a presentation for the subgroup using the specified generators, it is best to use the first type of coset system.

In general it is difficult to know whether such an automatic coset structure does actually exist: it is neither a necessary nor a sufficient condition that an automatic structure exists for the whole group, though it is certainly more likely that MAF will succeed in finding such an automatic coset structure if an automatic structure for the group has already been found. Of course, a coset system for a subgroup of finite index is always automatic.

Before we can use MAF to analyse coset rewriting systems we first need to learn how to produce the substructure files they will be built from.

Substructure Files

In this section G will denote a group (or monoid) defined by a rewriting system in the file groupname, and H a subgroup of G.

For any computation involving subgroups of a group or monoid, the user must first prepare an input file that defines generators of the substructure H as words in the generators of the parent structure G. These substructure generators may also be given their own names (which we shall refer to as H-generators), which must be distinct from those of the generators of G (which we shall call G-generators), even in the case where H-generators are actually equal to G-generators. Words in these two types of generator will be known as H-words and G-words; "mixed" words only occur in coset systems of the second type, and only in the form implied by the second type of coset equation. If the file containing the rewriting system for G is called groupname, then the file containing the definitions (and possibly names) of the generators of H should be called groupname.subsuffix, where it is strongly recommended that subsuffix has the string sub as its first three letters. Some examples can be found in the directory examples/subgroups. For example, there is a file called ab2 that defines the 2-generator free abelian group:

#free abelian group of rank 2
_RWS := rec
(
  isRWS := true,
  ordering := "shortlex",
  generatorOrder := [a,b,A,B],
  inverses := [A,B,a,b],
  equations := 
  [ 
    [b*a,a*b] 
  ]
);

and one called ab2.sub that defines a subgroup of index 6.

_RWS_Sub := rec
(
  subGenerators:=[a^2*b^3, a^4*b^9],
  subGeneratorNames:=[x,y]
);

The syntax is once again based on that of the GAP record, and should be self-explanatory. Note that the G-generators are a, b, A and B, and the H-generators x and y. It is important that no generator should be named _H, since that will be used by MAF itself as a symbol that represents the subgroup H itself. You should note the following points:

Inverses

Another optional field, not present in the previous example, is subGeneratorInverseNames. This list must have the same length as subGeneratorNames, but it may have gaps. The names occurring in it must all occur in subGeneratorNames. It is used to record the fact that certain of these generators are inverse to each other; it is the user's responsibility to ensure that this information is accurate. An example of a file with this feature, specifying another subgroup of the same group, is as follows:

_RWS_Sub := rec
(
  subGenerators:=[a^2, A^2, b^5, B^5],
  subGeneratorNames:=[x,X,y,Y],
  subGeneratorInverseNames:=[X,x,Y,y]
);

It is not actually necessary to specify inverse generators for subgroups explicitly in this fashion, since MAF will adjoin them automatically if required. However it is useful to do so if you want to follow the "case change" convention for naming inverses, since MAF will use ^-1 names for names it generates itself. It is also useful to do so if you want the words in the subgroup generators to be ordered using the [x,X,y,Y,] type of ordering, because otherwise you will get [x,y,X,Y] instead, and this is much less likely to be confluent.

Normal Closure substructure files

To create a coset system for the normal closure of s set of subgroup generators the substructure file should use the following syntax instead:
_RWS_Sub := rec
(
  normalSubGenerators:=[a^2,b^5]
);

With this type of substructure file you may not specify names for the subgroup generators, and there is no need to include the inverse of the generators as generators. With this type of coset system MAF uses the symbol _N to represent the subgroup, rathet than _H. Therefore, in this case you must not use _N as the name of a generator.

Use of Substructure Files

Only two significant uses are made of substructure files. In the first place, and by far the more important use, is, as we have already said, that MAF programs use the combination of a group file and a substructure file to automatically generate a coset rewriting system. The other use, which we shall not consider for now, is to generate composite multipliers for a specific collection of words using the program gpmult. Generation of a coset system is usually done automatically whenever you use the -cos option with one of the MAF programs that understands this option. However you can generate such a file explicitly using the program makecosfile, and once the file is generated you can invoke MAF utilities directly with the name of this file, so before examining the format of these coset rewriting system files, we shall explain how they are named. (This would be useful if you want to edit the coset system manually afterwards, for example to change the levels of the generators.)

Auto-generated Coset Rewriting System files, and their Name

When you use the -cos option and supply MAF with a base rewriting system file groupname and a substructure suffix subsuffix MAF will generate a coset rewriting system named groupname.cossuffix where cossuffix is defined as follows. If (as is recommended), subsuffix has the form substring for some (possibly empty) string string, then cossuffix is cosstring. Otherwise, cossuffix is subsuffix_cos. The default for subsuffix is just sub, and then cossuffix is just cos. If the file containing the coset rewriting system is named groupname.cossuffix, then in general the automata and any other files created from it will have names of form groupname.cossuffix.suffix. However, a few files will have names based on groupname.subsuffix.suffix. This applies in particular to the presentation that may be generated for the subgroup, and, in KBMAG only, to the word-acceptor for the subgroup.

MAF will always try to generate a coset rewriting system with names and inverses when the -cos command tail is used. So, if you want to generate a coset system of the first type, then make sure you do not give the subgroup generators names. A coset system of this type may be useful, particularly if what you are trying to do is to prove that the index of the subgroup is finite, and the more usual type of coset system would not be confluent or automatic. However, less information about the subgroup H will be available from this type of system : in particular a presentation on the specified subgroup generators cannot be calculated.

Coset Rewriting Systems and makecosfile

We shall explain the use of makecosfile next, since it provides a convenient opportunity to examine what a coset rewriting system file looks like, and how the two different types of coset rewriting systems are created. Remember that you do not normally need to invoke makecosfile explicitly: if you invoke a MAF program with the -cos option, and do not specify an explicit cossuffix, or you specify an explicit subsuffix, then MAF will automatically create the required coset system.

Like other MAF programs that generate coset systems makecosfile assumes that we are dealing with a subgroup H of a group or monoid G. The program itself will not attempt to verify this, however, and it is not necessary for all generators to have inverses defined in the input file. It is invoked as follows:

makecosfile [-sg] [-ni] groupname [subsuffix]

makecosfile takes its input from the file groupname, which should contain a declaration of a record defining a rewriting system, in the format described in Creating Input Files for automata, and from a substructure file groupname.subsuffix, which should contain a list of subgroup generators and (optionally) names for them, in the format described in Substructure Files. The input rewriting system is not allowed to have a weighted-lex ordering. Output is to the file groupname.cossuffix, and is a coset rewriting system, the contents of which will be desribed in the next paragraph. How cossuffix is determined was explained above in Auto-generated Coset Rewriting System files and their Name.

A coset rewriting system contains the same generators and equations as the original one defined in groupname, and also some additional generators and equations. In particular, a new symbol named _H (or _N if the substructure file used the normalSubGenerators field) will be present. This symbol is not really a generator of G or of H, but is nevertheless defined as one. Sometimes this symbol represents H itself, and sometimes is just an alias for the identity element.

Coset Systems without H-words

If the option -sg is not specified, then _H will be the only new generator, and the new equations will have the form [_H*w,_H], where w is a word defining one of the subgroup generators, as listed in the substructure file. The new symbol _H has no inverse, and so it does not cancel on the left, and the new equation represents the coset equation H*w=H. The ordering for a coset rewriting system is always either "wreathprod","rt_wreathprod", or "coset" where the level of _H is 1, and those of the G-generators is increased by one if necessary to make them greater than that of _H. (This is why weighted-lex orderings are not possible - in general this would cause the reduced words for the group elements to be different in the coset-system ordering than in the original group). In the first example in the preceding section, the output file is ab2.cos and looks like this:

_RWS := rec
(
 isRWS := true,
 isConfluent := false,
 generatorOrder := [a,b,A,B,_H],
 ordering := "wreathprod",
 level := [2,2,2,2,1],
 inverses := [A,B,a,b,],
 equations := 
 [
   [b*a,a*b],
   [_H*a^2*b^3,_H],
   [_H*a^4*b^9,_H]
 ]
);

Coset Systems with H-words

If the option -sg (for "subgroup generators") is specified, then the record defined in the substructure file must contain a subGeneratorNames field. The names specified in this list will also be introduced as new generators in the coset rewriting system, with level 1. The new equations will now have the form [_H*w,x*_H], where x is the name for the subgroup generator whose G-word is w. In this situation, the symbol _H is being used purely as a separator, and the equation represents an exact equation in the group if _H is equated with the identity element (or just ignored). In general, words in the group can be represented as v*_H*w, where v is a word in the H-generators, and w is a word in the G-generators. This represents the element v*w of G.

By default, if the substructure file does not contain a subGeneratorInverseNames field, then inverses of the H-generators will be appended as further H-generators. (The inverse symbol for H-generator x is named x^-1.) If the -ni option is specified, however, then these inverse generators are not introduced. (This option is provided because KBMAG has it: it is not clear to the author of MAF why this would ever be useful). The output of makecosfile -sg in the case of the example above is as follows:

_RWS_Cos := rec
(
  isRWS := true,
  isConfluent := false,
  generatorOrder := [a,b,A,B,_H,x,y,x^-1,y^-1],
  ordering := "wreathprod",
  level := [2,2,2,2,1,1,1,1,1],
  inverses := [A,B,a,b,,x^-1,y^-1,x,y],
  equations := 
  [
    [b*a,a*b],
    [_H*a^2*b^3,x*_H],
    [_H*a^4*b^9,y*_H]
  ]
);

Remarks on Word Ordering

In KBMAG's implementation of coset systems, use of "wreathprod" ordering is mandated. The intention behind this is to ensure that all equations produced by Knuth Bendix expansion will take the desired form: _H*u=h*_H*v. This is the case if the original input rewriting system uses "shortlex" ordering. However, if "recursive" ordering is used, then "wreathprod" ordering does not work. In fact if the ab2 example is changed to use recursive ordering, KBMAG's kbprogcos will not work properly with the coset system at all. This arises because in wreath product ordering h*_H*b is greater than _H*b*a. KBMAG assumes it can move the h word from the LHS to the RHS of this equation, when clearly it cannot. Therefore KBMAG should not really allow coset systems to based on input rewriting systems that do not use shortlex ordering.

MAF is able to deal with such a system however: it does this by examining the level field of the coset system. If it determines that problems with word order will arise then it silently changes the ordering method from "wreathprod" to "coset". This is an ordering method new to MAF which works as follows: to compare two words u,v first split each word into its initial "H part" and its final "G part". Then compare the G parts. If these are not equal then this determines the order. If the words have equal G parts compare the H parts.

This approach would work for any method of ordering G-words and H-words, so MAF could in principle be much more flexible in the range of word ordering methods it supports for coset rewriting systems. It is the author's intention to support this in future.

MAF also allows the original rewriting system to use the "rt_recursive" and "rt_wreathprod" ordering methods. In either case the coset system will use "rt_wreathprod" ordering. This does not suffer from the same problem as "wreathprod" with coset systems.

Detailed description of a Coset Rewriting System

There are three types of generator in a coset rewriting system, the G-generators, which are the generators of G coming from the original rewriting system for G, the symbol _H or _N, which represents the subgroup H itself and, optionally, the H-generators, which should be distinct from the G-generators, and are independent names for the generators of the subgroup H.

There are also three types of equations, those in the G-generators alone, those involving the generator _H or _N, and those in the H-generators alone. (Of course, there will be none of the third type if H-generators are not present.) Unless you are especially interested the next few indented paragraphs can be skipped.

The left and right hand sides of the equations involving _H should both have the form v_Hw, where v is a (possibly empty) word in the H-generators, and w a (possibly empty) word in the G-generators. In fact, those in the input file should all have the form [_Hw,_H], or [_Hw,x_H] for some H-generator x, and they define the generators of H as words w in the G-generators. The order of the equations in the input file is unimportant. The ordering of words in a coset rewriting system must be "wreathprod", and _H and the H-generators must all have a strictly smaller level than each of the G-generators. This is to ensure that words containing _H get reduced to the desired form v_Hw with the word w coming as early as possible in the ordering of the G-words.

The previous paragraph can be taken as a definition of a coset rewriting system. Any input not conforming to these rules will not be regarded as a coset system (a warning will be issued), and will probably produce meaningless results. Of course, if the input file for the coset system is produced by MAF itself via use of the -cos option with a substructure file,as recommended, then it will be guaranteed to be valid.

Using automata with Coset Rewriting Systems

All the programs in MAF work equally well with rewriting systems that define groups or monoids, and with coset rewriting systems. So here we merely introduce programs and details that were not relevant when considering the use of automata to solve the word problem for groups and monoids. Usually this just means starting the relevant part of MAF with a command line option of -cos, and possibly an explicit subgroup suffix (in the case where your substructure file is not called simply groupname.sub, or as previously mentioned, you can simply supply the program with the full name of the coset system file if you prefer (and you should do this if you hand-edit the coset system file)

The aim of automata, when used with a coset system, is either to find a confluent rewriting system for it, or to generate an automatic structure for it, preferably both. So in fact there is almost no difference in the operation and use of automata from what has previously been described.

The pre-conditions under which it may be possible to find a confluent coset rewriting system are as follows:

Creating Subgroup Word Acceptors

A subgroup word acceptor for a subgroup H of a group G is a finite state automaton with alphabet equal to the monoid generating set for G, which accepts precisely those words that lie in H and are accepted by the word-acceptor for G. Thus they accept a unique word for each element of H. If such an acceptor can be constructed then an arbitrary word in the G-generators can then be tested for membership in H by first reducing to its G-normal form (using reduce) and then testing for acceptance by the word-acceptor for H. Thus the membership problem (that is the generalized word problem) can be solved for H. In fact MAF creates such word acceptors by first creating a "membership" FSA which tries to decide this question for an arbitrary word (this is similar to performing a Todd-Coxeter coset enumeration). However, this latter membership FSA can only ever be correct if the index of the subgroup is finite (because otherwise it would have to have an infinite number of states). In the infinite case, for some words this FSA will reach the failure state, which means the coset for the word is unknown (though it would be possible to find it if the coset rewriting system is either confluent or automatic). Yet, it may happen that when we restrict ourselves to considering the language, L0, of reduced words of G, that we may be able to create a more limited membership FSA that says whether an irreducible word is in the subgroup (and this is the subgroup word acceptor), because it may be the case that |{H*w : w ∈ L0 and w=p(h) for some hL0 and hH}| ∈ N; i.e. the set of all cosets corresponding to prefixes of irreducible words that are members of the subgroup - a set that is called C_H in what follows - this set may be finite. In this case we can construct a subgroup word acceptor by "anding" the word acceptor for the group with a suitably large provisional "membership" FSA. Indeed it is not to hard to prove that this is both a necessary and sufficient condition for the subgroup word acceptor to exist, given the existence of a word-acceptor for G in the first place.

Even so, whether or not we can construct such a word acceptor is rather a tricky question in practice. Even if we have successfully computed a confluent or an automatic structure for a coset system, (in which case we certainly can compute whether a reduced word w lies in H, by the simple expedient of reducing _H*w), we might not be able to construct the desired FSA, because the set C_H might not in fact be finite. Conversely, even when we cannot find a confluent or an automatic structure for a coset system, then, at least in the case where G was shortlex automatic, if C_H is finite, we can construct the subgroup word acceptor, through the use of a suitable large provisional coset rewriting system.

Theoretically, if G is automatic, and an automatic structure has previously been computed, then this method will work precisely when H is a quasiconvex subgroup of G. (The last sentence has been copied verbatim from KBMAG's documentation and the present author does not understand it because he does not know what it means to say that a subgroup is quasiconvex - but hopes it might be something to do with what he said in the previous paragraphs about the set C_H being finite, since there would be a pleasing analogy between the geometric concept of a convex set as set containing the line between any two points in the set, and the set C_H which contains the "line" P(r(U*v)) where r(w) denotes the reduced word for a word w and where P(w) denotes the set of all prefixes of w and w itself). The algorithm used for constructing a subgroup word acceptor is as follows:

  1. Construct the general multiplier in the group G for the sub-generators of H. (We can always do this since G is automatic). Let us call this FSA GM_G_H.

  2. Construct a "membership" FSA M_H which we hope can recognise all the cosets C_H.

  3. Then construct a candidate subgroup word acceptor WA_H by "anding" M_H with the the word-acceptor, WA_G, for the group.

  4. Clearly WA_H should be closed under the multiplication in G defined by GM_G_H. So we construct a candidate general multiplier in H by intersecting GM_G_H and WA_H, and this should contain an accept state for every word accepted by WA_H and every sub-generator. In fact it should contain such an accept state whether we form either the "left" or the "right" "exists" FSA for the multiplier. If it does not, then we can find one or more G-reduced words that are in H but are not accepted by WA_H, which means that our M_H did not have a big enough language. We then return to step ii), and use these words to improve M_H.

  5. If, as we hope, C_H really is finite, then eventually this process will terminate, and not only have we found the subgroup word acceptor, we have found a multiplier for it, and so have proved that the language it accepts really does define a subgroup.

When automata is attempting to analyse a coset system, its primary aim is to find a confluent rewriting system or automatic structure for it. In the latter case if it succeeds in doing so, it will then attempt to construct a subgroup word acceptor, using the algorithm described, provided the automatic structure for G has previously been computed. However, in other cases it does not do. The program gpsubwa can be used to attempt to construct a subgroup word acceptor in the case were automata only found a provisional (or possibly a confluent) coset rewriting system, but G itself already does have an automatic structure.

Table of automata and other files created by automata or related programs

The table below lists the various types of coset system automaton, 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 two 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 earlier, the name of the coset system would be altered accordingly too.

SuffixFile DescriptionWhen produced
group.cos.waThis the coset word-acceptor. It is an acceptor in G-words for the cosets. In other words it is not the acceptor for the possibly infinite minimal rewriting system for the entire coset system.If presentation is proved either confluent or automatic
group.cos.minredThis the FSA that accepts minimally coset reducible words. automata will calculate this to prove that there is no confluent rewriting system, or as an additional check that it has been found correctly. A word is minimally coset reducible if no prefix is coset reducible and no trailing subword is reducible in the ordinary sense.If coset system is proved either confluent or automatic
group.cos.diff1cThis 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 systemIf presentation is proved either confluent or automatic.
group.cos.diff2cThis is the FSA that contains all the word differences needed for the coset general multiplier, and just the transitions that occur in the general multiplier and the difference machine which recognises all the equations this gives rise to.If coset system is proved shortlex automatic.
group.cos.gmThis the determinised version of the coset general multiplier. It should be noted that 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.If coset system is proved shortlex automatic. See the corresponding entry in the table in "MAF for Groups and Monoid" for reasons why this file might not be produced.
group.cos.fastreduceThis is the reduction FSA for a confluent fast coset rewriting system. It contains the correct reduction for all words for which both the word itself and its correct reduction appear in the minimal rewriting system. If feasible it contains the correct reduction for all equations. This FSA can be much larger than group.cos.reduce, and, in the case where the group is infinite it may not exist at all. In such cases the group.cos.fastreduce FSA contains as many reductions as can be include without increasing the number of states of the FSA.When MAF has proved a coset rewriting system confluent.
group.cos.maxkbThis 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 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 shortlex automatic.
group.cos.midiff2This 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. In KBMAG it often contains spurious word differences.If coset system presentation is proved shortlex automatic.
group.cos.migmThe 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 generator x, for which ux=hv is a true equation. MAF labels initial states with both the accepted G-word and the best known H-word for the element h, whereas KBMAG only uses a best known G-word.If a coset system presentation is proved shortlex automatic. If a group presentation is proved shortlex confluent, and finite, then any coset system for the group is certainly shortlex 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 shortlex confluent and infinite, then the coset system might not be shortlex 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.minkbThis is the FSA which reaches its single accept state, which is also its initial 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 presentation is proved shortlex confluent or shortlex automatic.
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. This FSA is correct in the sense that any equation it can prove is true, and that it can prove all the primary equations that were known when MAF was interrupted, but incorrect in the sense that it may contain more than one state for the same group element, and there may be true equations it cannot prove. There may even be true 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 kbprogcos or autcos then this file is given the suffix .midiff1.

If MAF is interrupted while trying to prove a coset system shortlex automatic.
group.cos.pmidiff2

Provisional complete difference machine. It contains all the word differences and transitions between them that were known at the time. This FSA is correct in the sense that any equation it can prove is true, and that it could reduce all words at least as well as the provisional reduction FSA, but incorrect in the sense that it may contain more than one state for the same group element, and there may be true equations it cannot prove.

KBMAG uses the midiff2 extenstion for this FSA. MAF normally reserves the midiff2 extension for an FSA that has been proved correct, but if you use kbprogcos or autcos then this file is given the suffix .midiff2.

If MAF is interrupted while trying to prove a coset system automatic.
group.cos.preduceThis is the provisional reduction FSA for a rewriting system. This contains the reduction equations for G and possibly H, not just the coset equationsWhen MAF was interrupted while trying to prove a minimal rewriting system confluent.
group.cos.reduceThis is the reduction FSA for a confluent minimal rewriting system.When MAF has proved a minimal coset rewriting system confluent.
group.cos.subwaThis is the subgroup word acceptor for the subgroup.When MAF has found a subgroup word acceptor.
group.sub.rwsThis is the rewriting system for the subgroup that contains the presentation for the subgroup.When MAF has calculated a subgroup presentation.
group.sub.presThis is a file containing a presentation for the subgroup in the form of GAP source code.When MAF has calculated a subgroup presentation.

Several of the automata above can be used for reducing words u to the unique minimal coset represenative v in the group under the chosen ordering, such that Hu=Hv. In particular, this enables the generalised word-problem to be solved for the subgroup H of G. They can also be used for counting and enumerating the accepted language, and therefore to calculate the index of the subgroup.

gpsubpres and simplify

If a presentation of the subgroup H is required, then it can be computed using the program gpsubpres. In fact automata will automatically compute the presentation when it processes an automatic coset system.

The KBMAG work-alike autcos only computes a subgroup presentation if the -p option is specified. It does not invoke gpsubpres to do it however.

MAF can compute a subgroup presentation using either the generators you specified in the substructure file, (if these where named), or on the same set of generators as KBMAG, the Schreier generators, that are the subgroup elements corresponding to the initial states of the MIDFA coset multiplier. (These must obviously generate the subgroup, otherwise the coset multiplier would be invalid, since some subgroup elements would not be in the identity coset). For finite index subgroups it can also calculate a presentation using the Reidermeister-Schreier algorithm - this is done if you specify the -rs option.

If you use autcos, or run gpsubpres against files created by autcos (whether the KBMAG or the MAF version), then the Schreier generators are always used, because the necessary information for calculating the other presentation is not present in the multiplier.

If you use automata, or run gpsubpres against a coset multiplier produced by automata then, by default the presentation is based on the generators in the substructure file, if these were named. However, you can still get a presentation based on the Schreier generators, by specifying the -schreier command line option to either gpsubpres or automata.

From autcos the presentation is always output using GAP source code presentation, with a view to its being simplified, because the KBMAG version of gpsubpres generates a highly redundant presentation. However, the other programs can produce either a MAF/KBMAG rewriting system, which will be named groupname.sub_suffix.rws, or a GAP source code presentation groupname.sub_suffix.pres

In fact the presentations produced by MAF will not be usually be very redundant (at least for low index subgroups) and in fact for simple examples may be genuinely independent axiom systems. For subgroups with a high index the number of generators can be very high, particularly if Schreier generators are used: for example, while investigating the group in examples/g9(1_3), whose order is unknown, the author tried to compute a presentation of a subgroup of index 9576 which is known to be a perfect group. It is known that there are fairly small generating sets for this subgroup, but it does not seem to be at all easy to calculate a presentation using them: using named generators results in a coset system which quickly produces unmanagageably large equations, with unnamed generators the coset multiplier and table can be found quickly, but a presentation calculated on the Schreier generators has in excess of 17000 generators.

MAF comes with a rudimentary Tietze transformation program, called simplify, which can also be used to simplify the ".rws" files generated by gpsubpres or automata, or indeed any rewriting system in KBMAG/MAF format. simplify will happily increase the size of the presentation if it can eliminate generators by doing so, except that it will stop if the total length of the axioms has doubled (so running it more than once may eliminate more generators at the cost of increasing the total length of the relators further). The -keep_generators option stops simplify from eliminating generators so that the only changes to the presentation will be ones that reduce the total size of the presentation. The -eliminate option causes simplify to perform the Knuth-Bendix procedure to try to eliminate more axioms. This should only be attempted when the number of generators is less than about 50 as otherwise it is likely to be prohibitively slow. The -abelian option causes simplify to compute a presentation of the abelianisation of the presentation. It does this without using linear algebra. This is slow (so that programs like GAP may well be able to do much better), but it does mean that abelianisation can be computed for presentations with very large generating sets for which linear algebra techniques might not be practical.

Examples of Knuth-Bendix on coset rewriting systems

The examples/subgroups directory contains a number of examples of rewriting systems for groups together with some defined subgroups. examples/wallpaper contains a presentation of the 244 (or more accurately the 424) triangle group, together with subgroup files for each of the crystallographic wallpaper groups which occur as its subgroups - these can be used to generate nice presentations of each of these groups: there is at least one subgroup file for each group that will generate a confluent and automatic presentation.