% This file was created automatically from rws.msk.
% DO NOT EDIT!
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%
%A  rws.msk                GAP documentation                Andrew Solomon
%%
%A  @(#)$Id: rws.msk,v 1.11 2003/07/31 20:04:19 gap Exp $
%%
%Y  (C) 1999 School Math and Comp. Sci., University of St.  Andrews, Scotland
%Y  Copyright (C) 2002 The GAP Group
%%
\Chapter{Rewriting Systems}

Rewriting systems in {\GAP} are a framework for dealing with 
the very general task of rewriting elements of a free (or *term*) algebra
in some normal form.  Although most rewriting systems currently in use
are *string rewriting systems* (where the algebra has only one 
binary operation which is associative) the framework in {\GAP}
is general enough to encompass the task of rewriting algebras of
any signature from groups to semirings.

Rewriting systems are already implemented in  {\GAP} 
for finitely presented semigroups and for pc groups. The use of these 
particular rewriting systems is described in the corresponding chapters.
We describe here only the general framework of rewriting systems with 
a particular emphasis on material which would be 
helpful for a  developer implementing a rewriting system. 

We fix some definitions and terminology for the rest of this chapter.
Let <T> be a term algebra in some signature. 
A *term rewriting system* for <T> is a set of ordered pairs of 
elements of <T> of the form <(l, r)>. Viewed as a set of relations, the 
rewriting system determines a presentation for a quotient algebra <A> of <T>. 

When we take into account the fact that
the relations are expressed as *ordered* pairs, we have a way of 
*reducing* the elements of <T>. Suppose an element <u> of <T> has a 
subword <l> and <(l,r)> is a rule of the rewriting system, then
we can replace the subterm <l> of <u> by the term <r> and obtain a new 
word <v>. We say that we have *rewritten* <u> as <v>. 
Note that <u> and <v> represent the same 
element of <A>.
If <u> can not be rewritten using any rule of the rewriting system
we sat that <u> is *reduced*. 


%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\Section{Operations on rewriting systems}

\>IsRewritingSystem( <obj> ) C

This is the category in which all rewriting systems lie.



\>Rules( <rws> ) A

The rules comprising the rewriting system. Note that these may 
change through the life of the rewriting system, however they
will always be a set of defining relations of the algebra
described by the rewriting system.


\>OrderOfRewritingSystem( <rws> ) A
\>OrderingOfRewritingSystem( <rws> ) A

return the ordering of the rewriting system <rws>.
%the synonym here guarantees compatibility with {\GAP}~4.1 and {\GAP}~4.2.



\>ReducedForm( <rws>, <u> ) O

Given an element <u> in the free (or term) algebra over which
<rws> is defined, rewrite <u> by successive applications of the
rules of <rws> until no further rewriting is possible, and return
the resulting element of <T>.



\>IsConfluent( <rws> ) P
\>IsConfluent( <A> ) P

return `true' if and only if the rewriting system <rws> is confluent. 
A rewriting system is *confluent* if, for every two words 
<u> and <v> in the free algebra <T> which represent the same element 
of the algebra <A> defined by <rws>,
`ReducedForm(<rws>,<u>) =  ReducedForm(<rws>,<v>)' as words in the
free algebra <T>. This element is the *unique normal form*
of the element represented by <u>.

In its second
form, if <A> is an algebra with a canonical rewriting system associated
with it, `IsConfluent' checks whether that rewriting system is confluent.

Also see~"IsConfluent!for pc groups".



\>ConfluentRws( <rws> ) A

Return a new rewriting system defining the same algebra as <rws> 
which is confluent.


\>IsReduced( <rws> ) P

A rewriting system is reduced if for each rule (<l>, <r>), 
<l> and <r> are both reduced.




\>ReduceRules( <rws> ) O

Reduce rules and remove redundant rules to make <rws> reduced.



\>AddRule( <rws>, <rule> ) O


Add  <rule> to a rewriting system <rws>. 



\>AddRuleReduced( <rws>, <rule> ) O

Add <rule> to rewriting system <rws>. Performs a reduction operation
on the resulting system, so that if <rws> is reduced it will remain reduced.



\>MakeConfluent( <rws> ) O

Add rules (and perhaps reduce) in order to make <rws> confluent



% Don't know what to make of these.
\>GeneratorsOfRws( <rws> ) A



\>AddGenerators( <rws>, <gens> ) O



%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\Section{Operations on elements of the algebra}

In this section let <u> denote an element of the term algebra
<T> representing <[u]> in  the quotient algebra <A>.

\>ReducedProduct( <rws>, <u>, <v> ) O

The result is  <w> where <[w]> = <[u]><[v]> in <A> and
<w> is  in reduced form.



The remaining operations are defined similarly when they 
are defined (as determined by the  signature  of the term algebra).
\>ReducedSum( <rws>, <left>, <right> ) O


\>ReducedOne( <rws> ) O


\>ReducedAdditiveInverse( <rws>, <obj> ) O


\>ReducedComm( <rws>, <left>, <right> ) O


\>ReducedConjugate( <rws>, <left>, <right> ) O


\>ReducedDifference( <rws>, <left>, <right> ) O


\>ReducedInverse( <rws>, <obj> ) O


\>ReducedLeftQuotient( <rws>, <left>, <right> ) O


\>ReducedPower( <rws>, <obj>, <pow> ) O


\>ReducedQuotient( <rws>, <left>, <right> ) O


\>ReducedScalarProduct( <rws>, <left>, <right> ) O


\>ReducedZero( <rws> ) O



%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\Section{Properties of rewriting systems}

The following properties may be used to identify the 
type of term algebra over which the rewriting system is defined.

\>IsBuiltFromAdditiveMagmaWithInverses( <obj> ) P


\>IsBuiltFromMagma( <obj> ) P


\>IsBuiltFromMagmaWithOne( <obj> ) P


\>IsBuiltFromMagmaWithInverses( <obj> ) P


\>IsBuiltFromSemigroup( <obj> ) P


\>IsBuiltFromGroup( <obj> ) P



%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\Section{Rewriting in Groups and Monoids}

One application of rewriting is to reduce words in finitely presented groups
and monoids. The rewriting system still has to be built for a finitely
presented monoid (using `IsomorphismFpMonoid' for conversion). Rewriting
then can take place for words in the underlying free monoid. (These can be
obtained from monoid elements with the command `UnderlyingElement'.)

\beginexample
gap> f:=FreeGroup(3);;
gap> rels:=[f.1*f.2^2/f.3,f.2*f.3^2/f.1,f.3*f.1^2/f.2];;
gap> g:=f/rels;
<fp group on the generators [ f1, f2, f3 ]>
gap> mhom:=IsomorphismFpMonoid(g);
MappingByFunction( <fp group on the generators 
[ f1, f2, f3 ]>, <fp monoid on the generators 
[ f1^-1, f1, f2^-1, f2, f3^-1, f3 
 ]>, function( x ) ... end, function( x ) ... end )
gap> mon:=Image(mhom);
<fp monoid on the generators [ f1^-1, f1, f2^-1, f2, f3^-1, f3 ]>
gap> k:=KnuthBendixRewritingSystem(mon);
Knuth Bendix Rewriting System for Monoid( [ f1^-1, f1, f2^-1, f2, f3^-1, f3 
 ], ... ) with rules 
[ [ f1^-1*f1, <identity ...> ], [ f1*f1^-1, <identity ...> ], 
  [ f2^-1*f2, <identity ...> ], [ f2*f2^-1, <identity ...> ], 
  [ f3^-1*f3, <identity ...> ], [ f3*f3^-1, <identity ...> ], 
  [ f1*f2^2*f3^-1, <identity ...> ], [ f2*f3^2*f1^-1, <identity ...> ], 
  [ f3*f1^2*f2^-1, <identity ...> ] ]
gap> MakeConfluent(k);
gap> a:=Product(GeneratorsOfMonoid(mon));
f1^-1*f1*f2^-1*f2*f3^-1*f3
gap> ReducedForm(k,UnderlyingElement(a));
<identity ...>
\endexample

To rewrite a word in the finitely presented group, one has to convert it to
a word in the monoid first, rewrite in the underlying free monoid and
convert back (by forming first again an element of the fp monoid) to the
finitely presented group.

% this example uses random and would be a hassle to modify every time
% something changes
\begintt
gap> r:=PseudoRandom(g);;
gap> Length(r);
3704
gap> red:=ReducedForm(k,UnderlyingElement(melm));
f1^-1^3*f2^-1*f1^2
gap> melm:=ElementOfFpMonoid(FamilyObj(One(mon)),red);
f1^-1^3*f2^-1*f1^2
gap> gpelm:=PreImagesRepresentative(mhom,melm);
f1^-3*f2^-1*f1^2
gap> r=gpelm;
true
gap> CategoriesOfObject(red);
[ "IsExtLElement", "IsExtRElement", "IsMultiplicativeElement", 
  "IsMultiplicativeElementWithOne", "IsAssociativeElement", "IsWord" ]
gap> CategoriesOfObject(melm);
[ "IsExtLElement", "IsExtRElement", "IsMultiplicativeElement", 
  "IsMultiplicativeElementWithOne", "IsAssociativeElement", 
  "IsElementOfFpMonoid" ]
gap> CategoriesOfObject(gpelm);
[ "IsExtLElement", "IsExtRElement", "IsMultiplicativeElement", 
  "IsMultiplicativeElementWithOne", "IsMultiplicativeElementWithInverse", 
  "IsAssociativeElement", "IsElementOfFpGroup" ]
\endtt

Note, that the elements `red' (free monoid) `melm' (fp monoid) and `gpelm'
(group) differ, though they are displayed identically.

Under Unix, it is possible to use the `kbmag' package to replace the
built-in rewriting by this packages efficient C implementation. You can do
this (after loading the `kbmag' package) by assigning the variable `KB_REW'
to `KBMAG_REW'.  Assignment to `GAPKB_REW' reverts to the built-in
implementation. (See section~"KB_REW".)
\begintt
gap> LoadPackage("kbmag");
true
gap> KB_REW:=KBMAG_REW;;
\endtt

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\Section{Developing rewriting systems}

The key point to note about rewriting systems is that they have 
properties such as `IsConfluent' and attributes such as `Rules', however
they are rarely stored, but rather computed afresh each time they
are asked for, from data stored in the private members of the rewriting
system object.  This is because a rewriting system often evolves
through a session, starting with some rules which define the
algebra <A> as relations, and then adding more rules to make
the system confluent.
For example, in the case of Knuth-Bendix rewriting systems
(see Chapter~"Finitely Presented Semigroups and Monoids"), the function
`CreateKnuthBendixRewritingSystem' creating the
rewriting system (in `kbsemi.gi') uses

\begintt
kbrws := Objectify(NewType(rwsfam, 
  IsMutable and IsKnuthBendixRewritingSystem and 
  IsKnuthBendixRewritingSystemRep), 
  rec(family:= fam,
  reduced:=false,
  tzrules:=List(relwco,i->
   [LetterRepAssocWord(i[1]),LetterRepAssocWord(i[2])]),
  pairs2check:=CantorList(Length(r)),
  ordering:=wordord,
  freefam:=freefam));
\endtt

In particular, since we don't use the filter `IsAttributeStoringRep'
in the `Objectify', whenever `IsConfluent' is called, the appropriate
method to determine confluence is called. 



%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%
%E