  
  [1m[4m[31m3. Logged Rewriting Systems[0m
  
  A logged rewrite system is associated with a group presentation. Each logged
  rewrite rule contains, in addition to the standard rewrite rule, a record or
  log  component  which  express the rule in terms of the original relators of
  the  group.  Here  a  logged  rewrite  rule  is represented by a triple [22m[32m[ u,
  [L1,L2,..,Lk],  v][0m,  where [22m[32m[u,v][0m is a rewrite rule and L_i = [n_i,w_i] where
  n_i  is  a  group relator and w_i is a word. These three components obey the
  identity u = n_1^w_1 ... n_k^w_k v.
  
  Rules of the form g^+g^- are relevant to the monoid presentation, but not to
  the group presentation, so are not included in the logging.
  
  
  [1m[4m[31m3.1 Logged Knuth-Bendix Completion[0m
  
  The  functions  in  this  section  are  the  logged versions of those in the
  previous chapter.
  
  [1m[4m[31m3.1-1 LoggedOnePassKB[0m
  
  [1m[34m> LoggedOnePassKB( [0m[22m[34mloggedrules[0m[1m[34m ) __________________________________[0moperation
  
  Given  a logged rewrite system, this function finds all the rules that would
  be  added  to  complete  the  rewrite system in [22m[32mOnePassKB[0m, and also the logs
  which  relate  the  new  rules to the originals. The result of applying this
  function  to  loggedrules  is  to add new logged rules to the system without
  changing the monoid it defines.
  
  [22m[35m---------------------------  Example  ----------------------------[0m
    [22m[35m[0m
    [22m[35mgap> l0 := ListWithIdenticalEntries( 8, 0 );;[0m
    [22m[35mgap> for j in [1..8] do [0m
    [22m[35m         r := r0[j];[0m
    [22m[35m         if ( j<5 ) then[0m
    [22m[35m            l0[j] := [ r[1], [ [j,id] ], r[2] ];[0m
    [22m[35m         else[0m
    [22m[35m            l0[j] := [ r[1], [ ], r[2] ];[0m
    [22m[35m         fi;[0m
    [22m[35m     od;[0m
    [22m[35mgap> l0;[0m
    [22m[35m[ [ q8_M1^4, [ [ 1, <identity ...>] ], <identity. ..> ], [0m
    [22m[35m  [ q8_M2^4, [ [ 2, <identity ...>] ], <identity ...> ], [0m
    [22m[35m  [ q8_M1*q8_M2*q8_M1*q8_M4, [ [ 3, <identity ...> ] ], <identity ...> ],   [0m
    [22m[35m  [ q8_M1^2*q8_M2^2, [ [ 4, <identity ...> ] ], <identity ...> ], [0m
    [22m[35m  [ q8_M1*q8_M3, [ ], <identity ...> ], [0m
    [22m[35m  [ q8_M2*q8_M4, [ ], <identity ...> ], [0m
    [22m[35m  [ q8_M3*q8_M1, [ ], <identity ...> ], [0m
    [22m[35m  [ q8_M4*q8_M2, [ ], <identity ...> ] ] [0m
    [22m[35mgap> l1 := LoggedOnePassKB( l0 );[0m
    [22m[35m[ [ q8_M1^4, [ [ 1, <identity. ..> ] ], <identity ...> ], [0m
    [22m[35m  [ q8_M2^4, [ [ 2, <identity ...> ] ], <identity ...> ], [0m
    [22m[35m  [ q8_M1*q8_M2*q8_M1*q8_M4, [ [ 3, <identity ...> ] ], <identity ...> ], [0m
    [22m[35m  [ q8_M1^2*q8_M2^2, [ [ 4, <identity ...>] ], <identity ...> ], [0m
    [22m[35m  [ q8_M1*q8_M3, [ ], <identity ...> ], [ q8_M2*q8_M4, [ ], <identity ...> ], [0m
    [22m[35m  [ q8_M3*q8_M1, [ ], <identity ...> ], [ q8_M4*q8_M2, [ ], <identity ...> ], [0m
    [22m[35m  [ q8_M2*q8_M1*q8_M4, [ [ -1, <identity. ..> ], [ 3, q8_M1^-3] ], q8_M1^3], [0m
    [22m[35m  [ q8_M1*q8_M2^2, [ [ -1, <identity ...> ], [ 4, q8_M1^-3] ], q8_M1^3], [0m
    [22m[35m  [ q8_M2^2, [ [ -1, <identity ...> ], [ 4, q8_M1^-2] ], q8_M1^2], [0m
    [22m[35m  [ q8_M1^3, [ [ 1, <identity ...>] ], q8_M3], [0m
    [22m[35m  [ q8_M2^3, [ [ 2, <identity ...>] ], q8_M4], [0m
    [22m[35m  [ q8_M1*q8_M2*q8_M1, [ [ 3, <identity ...> ] ], q8_M2 ], [0m
    [22m[35m  [ q8_M2^3, [ [ -4, <identity ...> ], [ 2, q8_M2^-1*q8_M1^-2] ], [0m
    [22m[35m      q8_M1^2*q8_M2], [0m
    [22m[35m  [ q8_M2^2, [ [ -4, <identity ...> ], [ 2, q8_M1^-2] ], q8_M1^2], [0m
    [22m[35m  [ q8_M1^2*q8_M2, [ [ 4, <identity ...>] ], q8_M4], [0m
    [22m[35m  [ q8_M1^3, [ [ 1, q8_M3^-1 ] ], q8_M3], [0m
    [22m[35m  [ q8_M2*q8_M1*q8_M4, [ [ 3, q8_M3^-1 ] ], q8_M3 ], [0m
    [22m[35m  [ q8_M1*q8_M2^2, [ [ 4, q8_M3^-1 ] ], q8_M3 ], [0m
    [22m[35m  [ q8_M2^3, [ [ 2, q8_M4^-1 ] ], q8_M4] ][0m
    [22m[35m[0m
  [22m[35m------------------------------------------------------------------[0m
  
  [1m[4m[31m3.1-2 LoggedKnuthBendix[0m
  
  [1m[34m> LoggedKnuthBendix( [0m[22m[34mloggedrules[0m[1m[34m ) ________________________________[0moperation
  [1m[34m> LoggedRewriteReduce( [0m[22m[34mloggedrules[0m[1m[34m ) ______________________________[0moperation
  
  The  function  [22m[32mLoggedRewriteReduce[0m  removes  unnecessary rules from a logged
  rewrite system. It works on the same principle as [22m[32mRewriteReduce[0m.
  
  The   function  [22m[32mLoggedKnuthBendix[0m  repeatedly  applies  [22m[32mLoggedOnePassKB[0m  and
  [22m[32mLoggedRewriteReduce[0m until no new rules are added and no unnecessary ones are
  included. The output is a reduced complete logged rewrite system.
  
  [22m[35m---------------------------  Example  ----------------------------[0m
    [22m[35m[0m
    [22m[35mgap> l1 := LoggedRewriteReduce( l1 );[0m
    [22m[35m[ [ q8_M1*q8_M3, [ ], <identity ...> ], [0m
    [22m[35m  [ q8_M2^2, [ [ -4, <identity ...> ], [ 2, q8_M1^-2 ] ], q8_M1^2 ], [0m
    [22m[35m  [ q8_M2*q8_M4, [ ], <identity ...> ], [ q8_M3*q8_M1, [ ], <identity ...> ], [0m
    [22m[35m      [ q8_M4*q8_M2, [ ], <identity ...> ], [0m
    [22m[35m  [ q8_M1^3, [ [ 1, <identity. ..> ] ], q8_M3 ], [0m
    [22m[35m  [ q8_M1^2*q8_M2, [ [ 4, <identity. ..> ] ], q8_M4 ], [0m
    [22m[35m  [ q8_M1*q8_M2*q8_M1, [ [ 3, <identity ...> ] ], q8_M2 ], [0m
    [22m[35m  [ q8_M2*q8_M1*q8_M4, [ [ 3, q8_M3^-1 ] ], q8_M3] ][0m
    [22m[35mgap> l2 := LoggedKnuthBendix( l1 );[0m
    [22m[35m[ [ q8_M1*q8_M3, [ ], <identity ...> ], [0m
    [22m[35m  [ q8_M2*q8_M1, [ [ 3, q8_M3^-1 ], [-1, <identity. ..> ], [ 4, q8_M1^-1 ] ], [0m
    [22m[35m      q8_M1*q8_M4 ], [0m
    [22m[35m  [ q8_M2^2, [ [ -4, <identity ...> ], [2, q8_M1^-2] ], q8_M1^2 ], [0m
    [22m[35m  [ q8_M2*q8_M3, [ [ -3, <identity ...> ] ], q8_M1*q8_M2 ], [0m
    [22m[35m  [ q8_M2*q8_M4, [ ], <identity ...> ], [ q8_M3*q8_M1, [ ], <identity ...> ], [0m
    [22m[35m  [ q8_M3*q8_M2, [ [ -1, <identity ...>], [4, q8_M1^-1 ] ], q8_M1*q8_M4 ],[0m
    [22m[35m  [ q8_M3^2, [ [ -1, <identity ...>] ], q8_M1^2 ], [0m
    [22m[35m  [ q8_M3*q8_M4, [ [ -1, <identity ...>], [ -2, q8_M1^-2], [0m
    [22m[35m        [ 4, <identity ...> ], [ 3, q8_M3^-1*q8_M2^-1 ], [0m
    [22m[35m        [ -3, <identity. ..> ] ], q8_M1*q8_M2 ], [0m
    [22m[35m  [ q8_M4*q8_M1, [ [ -4, <identity ...> ], [ 3, q8_M1^-1 ] ], q8_M1*q8_M2 ], [0m
    [22m[35m  [ q8_M4*q8_M2, [ ], <identity ...> ], [0m
    [22m[35m  [ q8_M4*q8_M3, [ [ -3, q8_M3^-1*q8_M4^-1] ], q8_M1*q8_M4 ], [0m
    [22m[35m  [ q8_M4^2, [ [ -4, <identity. ..> ] ], q8_M1^2 ], [0m
    [22m[35m  [ q8_M1^3, [ [ 1, <identity ...> ] ], q8_M3 ], [0m
    [22m[35m  [ q8_M1^2*q8_M2, [ [4, <identity. ..> ] ], q8_M4 ], [0m
    [22m[35m  [ q8_M1^2*q8_M4, [ [ -4, q8_M1^-2], [ 1, <identity ...> ] ], q8_M2 ] ] [0m
    [22m[35m[0m
  [22m[35m------------------------------------------------------------------[0m
  
  
  [1m[4m[31m3.2 Logged reduction of a word[0m
  
  [1m[4m[31m3.2-1 LoggedReduceWordKB[0m
  
  [1m[34m> LoggedReduceWordKB( [0m[22m[34mloggedrules[0m[1m[34m ) _______________________________[0moperation
  [1m[34m> LoggedOnePassReduceWord( [0m[22m[34mword, loggedrules[0m[1m[34m ) ____________________[0moperation
  [1m[34m> ShorterLoggedRule( [0m[22m[34mlogrule1, logrule2[0m[1m[34m ) _________________________[0moperation
  
  Given    a    word    and    a   logged   rewrite   system,   the   function
  [22m[32mLoggedOnePassReduceWord[0m   makes   one   reduction   of   the   word  (as  in
  [22m[32mOnePassReduceWord[0m) and records this, using the log part of the rule used and
  the position in the original word of the replaced part.
  
  The  function  [22m[32mLoggedReduceWordKB[0m repeatedly applies [22m[32mOnePassLoggedReduceWord[0m
  until  the  word  can  no  longer  be reduced. Each step of the reduction is
  logged,  showing  how  the  original  word  can be expressed in terms of the
  original relators and the irreducible word. When [22m[32mloggedrules[0m is complete the
  reduced  word is a unique normal form for that group element. The log of the
  reduction  however  has  no uniqueness but depends on the order in which the
  rules are applied and on the non-unique logs of the rules themselves.
  
  The  function  [22m[32mShorterloggedrule[0m  decides  whether one logged rule is better
  than another, using the same criteria as [22m[32mShorterRule[0m.
  
  [22m[35m---------------------------  Example  ----------------------------[0m
    [22m[35m[0m
    [22m[35mgap> w0;[0m
    [22m[35mq8_M1^3*q8_M2^3*q8_M1^3*q8_M2^3*q8_M1^3*q8_M2^3[0m
    [22m[35mgap> lw1 := LoggedOnePassReduceWord( w0, l2 );[0m
    [22m[35m[ [ [ 3, q8_M3^-1*q8_M2^-2*q8_M1^-3 ], [ -1, q8_M2^-2*q8_M1^-3 ],[0m
    [22m[35m      [ 4, q8_M1^-1*q8_M2^-2*q8_M1^-3 ], [ -4, q8_M1^-3 ], [ 2, q8_M1^-5 ],[0m
    [22m[35m      [ -4, q8_M1^-6 ], [ 3, q8_M1^-7 ], [ 1, <identity ...> ],[0m
    [22m[35m      [ 4, q8_M1^-2*q8_M3^-1 ], [ -4, q8_M1^-2*q8_M3^-1 ], [ 1, q8_M3^-1 ] ],[0m
    [22m[35m  q8_M3*q8_M2*q8_M1*q8_M2^3*q8_M1^3*q8_M2^3 ][0m
    [22m[35mgap> lw2 := LoggedReduceWordKB( w0, l2 );[0m
    [22m[35m[ [ [ 3, q8_M3^-1*q8_M2^-2*q8_M1^-3 ], [ -1, q8_M2^-2*q8_M1^-3 ],[0m
    [22m[35m      [ 4, q8_M1^-1*q8_M2^-2*q8_M1^-3 ], [ -4, q8_M1^-3 ], [ 2, q8_M1^-5 ],[0m
    [22m[35m      [ -4, q8_M1^-6 ], [ 3, q8_M1^-7 ], [ 1, <identity ...> ],[0m
    [22m[35m      [ 4, q8_M1^-2*q8_M3^-1 ], [ -4, q8_M1^-2*q8_M3^-1 ], [ 1, q8_M3^-1 ],[0m
    [22m[35m      [ 3, q8_M3^-2 ], [ -1, q8_M3^-1 ], [ 4, q8_M1^-1*q8_M3^-1 ],[0m
    [22m[35m      [ -4, q8_M4^-1*q8_M1^-1*q8_M3^-1 ],[0m
    [22m[35m      [ 2, q8_M1^-2*q8_M4^-1*q8_M1^-1*q8_M3^-1 ], [ -4, <identity ...> ],[0m
    [22m[35m      [ 3, q8_M1^-1 ], [ 1, q8_M2^-1*q8_M1^-1*q8_M2^-1*q8_M1^-1 ],[0m
    [22m[35m      [ 3, q8_M3^-1*q8_M1^-1 ], [ -1, q8_M1^-1 ], [ 4, q8_M1^-2 ],[0m
    [22m[35m      [ -4, q8_M3^-1*q8_M2^-1*q8_M4^-1*q8_M1^-2 ],[0m
    [22m[35m      [ 2, q8_M1^-2*q8_M3^-1*q8_M2^-1*q8_M4^-1*q8_M1^-2 ],[0m
    [22m[35m      [ -3, q8_M4^-1*q8_M1^-2 ], [ -4, q8_M1^-2 ], [ 3, q8_M1^-3 ],[0m
    [22m[35m      [ 1, <identity ...> ], [ 4, q8_M2^-2*q8_M3^-1 ], [ -4, q8_M3^-1 ],[0m
    [22m[35m      [ 2, q8_M1^-2*q8_M3^-1 ] ], q8_M1*q8_M4 ][0m
    [22m[35m[0m
  [22m[35m------------------------------------------------------------------[0m
  
  [1m[4m[31m3.2-2 LoggedRewritingSystemFpGroup[0m
  
  [1m[34m> LoggedRewritingSystemFpGroup( [0m[22m[34mloggedrules[0m[1m[34m ) _____________________[0mattribute
  
  Given   a  group  presentation,  the  function  [22m[32mLoggedRewritingSystemFpGroup[0m
  determines a logged rewrite system based on the relators. The initial logged
  rewrite system associated with a group presentation consists of two types of
  rule.  These  are  logged  versions  of  the two types of rule in the monoid
  presentation.  For  each  relator  [22m[32mrel[0m of the group there is a logged rule [22m[32m[
  rel,  [  [  1,  rel] ], id][0m. For each inverse relator there is a logged rule
  [22m[32m[gen*inv,  [],  id  ][0m.  It  then attempts a completion of the logged rewrite
  system.  The rules in the final system are partially ordered by the function
  [22m[32mShorterLoggedRule[0m.
  
  [22m[35m---------------------------  Example  ----------------------------[0m
    [22m[35m[0m
    [22m[35mgap> LoggedRewritingSystemFpGroup( q8 );[0m
    [22m[35m[ [ q8_M4*q8_M2, [ ], <identity ...> ], [ q8_M3*q8_Ml, [ ], <identity ...> ], [0m
    [22m[35m    [ q8_M2*q8_M4, [ ], <identity ...> ], [0m
    [22m[35m  [ q8_Ml*q8_M3, [ ], <identity ...> ], [0m
    [22m[35m  [ q8_Ml^2*q8_M4, [ [ -8, q8_Ml^-2 ], [ 5, <identity ...> ] ], q8_M2 ], [0m
    [22m[35m  [ q8_Ml^2*q8_M2, [ [ 8, <identity ...> ] ], q8_M4 ], [0m
    [22m[35m  [ q8_Ml^3, [ [ 5, <identity ...> ] ], q8_M3 ], [0m
    [22m[35m  [ q8_M4^2, [ [ -8, <identity ...> ] ], q8_Ml^2 ], [0m
    [22m[35m  [ q8_M4*q8_M3, [ [ -7, q8_M3^-1*q8_M4^-1 ] ], q8_Ml*q8_M4 ], [0m
    [22m[35m  [ q8_M4*q8_Ml, [ [ -8, <identity. ..> ], [ 7, q8_Ml^-1 ] ], q8_Ml*q8_M2 ], [0m
    [22m[35m  [ q8_M3*q8_M4, [0m
    [22m[35m      [ [ -5, <identity ...>], [ -6, q8_Ml^-2 ], [ 8, <identity ...> ], [0m
    [22m[35m          [ 7, q8_M3^-1*q8_M2^-1 ], [ -7, <identity. ..> ] ], q8_Ml*q8_M2 ], [0m
    [22m[35m  [ q8_M3^2, [ [ -5, <identity ...>] ], q8_Ml^2 ], [0m
    [22m[35m  [ q8_M3*q8_M2, [ [ -5, <identity. ..> ], [ 8, q8_Ml^-1 ] ], q8_Ml*q8_M4 ], [0m
    [22m[35m  [ q8_M2*q8_M3, [ [ -7, <identity ...> ] ], q8_M1*q8_M2 ], [0m
    [22m[35m  [ q8_M2^2, [ [ -a, <identity ...> ], [ 6, q8_M1^-2 ] ], q8_M1^2 ], [0m
    [22m[35m  [ q8_M2*q8_M1, [ [ 7, q8_M3^-1 ], [ -5, <identity ...> ], [ a, q8_M1^-1 ] ], [0m
    [22m[35m      q8_M1*q8_M4 ] ] [0m
    [22m[35m[0m
  [22m[35m------------------------------------------------------------------[0m
  
