The category of monoids defined by finite sets of rewrite rules provide a Magma level interface to Derek Holt's KBMAG programs, and specifically to KBMAG's Knuth--Bendix completion procedure on monoids defined by a finite presentation. As such much of the documentation in this chapter is taken from the KBMAG documentation [Hol97]. Familiarity with the Knuth--Bendix completion procedure is assumed. Some familiarity with KBMAG would be beneficial.
A rewrite monoid M is a finitely presented monoid in which equality between elements of M, called words or strings, is decidable via a sequence of rewriting equations, called reduction relations, rules, or equations. In the interests of efficiency the reduction rules are codified into a finite state automaton called a reduction machine. The words in a rewrite monoid M are ordered, as are the reduction relations of M. Several possible orderings of words are supported, namely short-lex, recursive, weighted short-lex and wreath-product orderings. A rewrite monoid can be confluent or non-confluent. If a rewrite monoid M is confluent its reduction relations, or more specifically its reduction machine, can be used to reduce words in M to their irreducible normal forms under the given ordering, and so the word problem for M can be efficiently solved.
The family of all rewrite monoids forms a category. The objects are the rewrite monoids and the morphisms are monoid homomorphisms. The Magma designation for this category of monoids is MonRWS. Elements of a rewrite monoid are designated as MonRWSElt.
A rewrite monoid M is constructed in a three-step process: