Whatever automata MAF constructs to solve the word problem for a group or monoid, or the generalised word problem for a subgroup, the same utility, reduce, is used afterwards to solve particular cases of the problem. For any input word, reduce will output the corresponding irreducible word. Two distinct input words will represent distinct elements of a group or monoid, or cosets of a subgroup, if and only if the corresponding output words computed for them by reduce are different. In most cases you do not even need to concern yourself with what automata are available to solve the word problem: if no specific instructions are given to it, reduce will pick the automaton that is expected to be fastest.
In the remainder of this section we describe the various automata MAF provides for solving the word problem.
As implemented by MAF and KBMAG, an automatic structure consists of two automata: the first is called the word-acceptor; the second the general multiplier. The latter is a compendium of a number of similar automata, each one telling us how to multiply elements by either a generator, or by the identity element. The definition of an automatic structure requires that the word-acceptor accepts at least one word for every element. The automatic structures usually constructed by MAF and KBMAG have a more useful property: the word-acceptor accepts exactly one word for each element of the group, and it is the least word in the word-ordering specified in the rewriting system describing the group.
Algorithms for the construction of automatic structures are described in [ECH+92] and [HEO05]. MAF uses the same general plan as KBMAG - it uses the Knuth-Bendix procedure to discover equations between words representing equal elements, computes their word-differences, and then tries to build first a word-acceptor and then a general multiplier using these word-differences.
More information about automatic structures can be found in Background material: Automatic structures.
All finite and many infinite groups have automatic structures. Although word-reduction using an automatic structure is generally slower than word-reduction using a confluent rewriting system this is by no means always be the case. In particular, when a recursive word-ordering is used, it might well be the case that word reduction with the multiplier is actually faster, because the number of word-reductions required to reduce even short words using a rewriting system can be extremely large.
It should be noted that a rewriting system is not an automaton. However, both MAF and KBMAG implement word reduction with a rewriting system by using a special type of automaton, called an index automaton; this is constructed from the rewriting system, and its use requires the data from it. There are other, slower, ways of using a rewriting system to perform word reduction that do not need an index automaton, for example, the Rabin-Karp string matching algorithm. These require less memory, but MAF does not implement any such method as yet.
In general, reducing a word with a rewriting system may lead to a different output word depending on the implementation of the procedure that uses the rewriting system. This might potentially happen whenever the input word needs to be reduced more than once, and at some stage of the reduction process there are two choices for the next reduction to apply. Clearly a rewriting system like this cannot solve the word problem. If a rewriting system does not have this undesirable feature, and the output word is independent of any choice made by the procedure, then it is said to be confluent. The essence of the Knuth-Bendix procedure is the attempt to make a rewriting system confluent by systematically searching for words w which have distinct reductions u and v and adjoining a new rule u=v or v=u whenever we find one. If we attempt to follow this process, but the input file does not present a finite object then this process might never terminate. If the input file does present a finite object then the process will terminate, but it might take an arbitrarily long time to do so.
When a finite confluent rewriting system exists for an input file, then there is a smallest such system, which is called the minimal confluent rewriting system. This is the only system that KBMAG constructs, and it is also constructed by MAF. MAF constructs another confluent system, which it calls the "fast" confluent rewriting system. It will be able to directly reduce more words than the minimal system, so reduction will be faster, possibly much faster in some cases. If the object underlying the rewriting system is finite then there is a canonical rewriting system of this type: the one that can directly reduce all reducible words that have an irreducible prefix. MAF does not yet construct this, though in many cases the "fast" rewriting system is probably close to it, provided the -nowd option is not used, because MAF usually creates a large number of secondary equations when a rewriting system becomes confluent, in order to discover the secondary word-differences. For infinite objects this canonical fast rewriting system is almost always infinite, but there is another possibility for a canonical rewriting system larger than the minimal confluent one: the rewriting system that contains all direct reductions that can be recognised by an index automaton with the same states as the minimal rewriting system's index automaton. For infinite objects the "fast" rewriting system constructed by MAF is usually close to being this system.
In MAF, a coset table is an FSA in which there is one state for each coset, and in which the transitions are determined by the group multiplication (i.e. by the right action of the generator on the coset). Each state is labelled by the last generator in the irreducible word for the least coset representative. In the case of a coset table for a subgroup of a group this is sufficient information to allow the irreducible word for the coset represented by the state to be constructed. The coset table for an entire group is simply the coset table of the trivial subgroup of the group. Coset tables only exist for finite index subgroups, and automata only constructs them for subgroups of groups. Although one could construct a coset table for a subgroup of a monoid it could not be used to perform word-reduction without computation of the "state definitions" for the coset table.
automata does not construct coset tables unless a coset system is being processed, but the utility gpcosets can be used to construct it from one of the other automata that solve the word problem, or gptcenum can be used to attempt do so using Todd-Coxeter coset enumeration.
The language of the coset table FSA consists of all words which are in the identity coset, i.e. that correspond to elements of the subgroup. The intersection of two finite index subgroups can be computed by using the fsaand utility to compute the intersection of the languages of the coset tables.
Word-difference machines encapsulate much of the information present in the general multiplier, and can be used to perform word reduction. Although in general word reduction using the general multiplier will be faster there are cases where this might not necessarily be so. In general the general multiplier has many more states than a word-difference machine, so that if memory is short it may be that using one of the word-difference machines to perform word reduction is faster.
The best word-difference machine to use is usually the "correct word-difference machine" (with suffix .diff2c or .midiff2c), but it might sometimes be the case that the "correct primary word-difference machine" (suffix .diff1c or .midiff1c) is actually faster due its usually much smaller number of transitions. The "complete word-difference machine" (suffix .diff2) can also be used, but generally should not be.
Reduction using a word-difference machine is actually probably most useful at times when MAF's computations have failed to find either an automatic structure or a confluent rewriting system. In such cases a word-difference machine computed from the set of known equations will be the best hope of proving that distinct words do not represent different elements.
The "reduction recogniser" (.rr suffix), "primary equation recogniser" (.minkb suffix), and "equation recogniser" (.maxkb suffix) automata are also essentially word-difference machines, and could be used to perform word-reduction, but MAF does not currently support this, though it is likely that at least the first will be supported properly in future. The principal reason these automata are currently constructed is to allow the computation of the two "correct" word-difference machines.