Introduction

The class of finitely presented groups defined by finite rewrite systems provide a Magma level interface to Derek Holt's KBMAG programs, and specifically to the Knuth--Bendix completion procedure for groups defined by a finite (monoid) presentation. Much of the material 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.

Terminology

A rewrite group G is a finitely presented group in which equality between elements of G, called words or strings, may be 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 group G are ordered, as are the reduction relations of G. Several possible orderings of words are supported, namely short-lex, recursive, weighted short-lex and wreath-product orderings. A rewrite group can be confluent or non-confluent. If a rewrite group G is confluent its reduction relations, or more specifically its reduction machine, can be used to reduce words in G to their irreducible normal forms under the given ordering, and so the word problem for G can be efficiently solved.

The Category of Rewrite Groups

The family of all rewrite groups forms a category. The objects are the rewrite groups and the morphisms are group homomorphisms. The Magma designation for this category of groups is GrpRWS. Elements of a rewrite group are designated as GrpRWSElt.

The Construction of a Rewrite Group

A rewrite group G is constructed in a three-step process:

(i)

We construct a free group FG.

(ii)

We construct a quotient F of FG.

(iii)

We create a monoid presentation of F and then run a Knuth--Bendix completion procedure on this presentation to create a rewrite group G.