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 expresses the rule in terms of the original relators of the group. We represent such a rule by a triple [ u, [L1,L2,..,Lk], v]
, where [u,v]
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} \ldots n_k^{w_k} v\).
Rules of the form \(g^+g^-\) apply to the monoid presentation, but not to the group presentation, so are given an empty logged component.
The functions in this section are the logged versions of those in the previous chapter.
‣ LoggedOnePassKB ( loggedrules ) | ( operation ) |
Given a logged rewrite system, this function finds all the rules that would be added to complete the rewrite system of OnePassKB
in 2.2-3, 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.
In the example, we first convert the presentation for q8
into an initial set of logged rules, and then apply one pass of Knuth-Bendix.
In the development version the function LoggedOnePassKB
returns a two-element list of lists. The first element is a set of logged rules and the second element is an empty list of r-sequences, whatever they are! (Need more here.)
gap> l0 := ListWithIdenticalEntries( 8, 0 );; gap> for j in [1..8] do > r := r0[j]; > if ( j<5 ) then > l0[j] := [ r[1], [ [j,id] ], r[2] ]; > else > l0[j] := [ r[1], [ ], r[2] ]; > fi; > od; gap> l0; [ [ q8_M1^4, [ [ 1, <identity ...>] ], <identity. ..> ], [ q8_M2^4, [ [ 2, <identity ...>] ], <identity ...> ], [ q8_M1*q8_M2*q8_M1*q8_M4, [ [ 3, <identity ...> ] ], <identity ...> ], [ q8_M1^2*q8_M2^2, [ [ 4, <identity ...> ] ], <identity ...> ], [ q8_M1*q8_M3, [ ], <identity ...> ], [ q8_M2*q8_M4, [ ], <identity ...> ], [ q8_M3*q8_M1, [ ], <identity ...> ], [ q8_M4*q8_M2, [ ], <identity ...> ] ] gap> l1 := LoggedOnePassKB( l0 );; gap> Length( l1[1] ); 21
Note that the length \(21\) of l1
is, as expected, the same as that of r1
in 2.2-3.
‣ LoggedKnuthBendix ( loggedrules ) | ( operation ) |
‣ LoggedRewriteReduce ( loggedrules ) | ( operation ) |
The function LoggedRewriteReduce
removes unnecessary rules from a logged rewrite system. It works on the same principle as RewriteReduce
in 2.2-3.
The function LoggedKnuthBendix
repeatedly applies functions LoggedOnePassKB
and LoggedRewriteReduce
until no new rules are added and no unnecessary ones are included. The output is a reduced complete logged rewrite system.
In order to clarify the meaning of the rules below, consider the second rule in l2
which shows how \(b^+a^+\) reduces to \(a^+b^-\). For this rule [u,L,v]
we will verify that \(u = n_1^{w_1}n_2^{w_2}n_3^{w_3} v\), as in the introduction to this chapter. The rule is:
[ q8_M2*q8_M1, [ [3,q8_M3^-1], [-1,<identity...>], [4,q8_M1^-1] ], q8_M1*q8_M4 ].
As before, we write \(a^+,\;b^+,\;a^-,\;b^-\) for q8_M1,q8_M2,q8_M3,q8_M4
respectively. The relators \(3,4\) and the inverse of relator \(1\) (denoted by \(-1\)) are \(a^+b^+a^+b^-,\; a^{+2}b^{+2}\) and \(a^{-4}\), and these are conjugated by \((a^-)^{-1}=a^+, (a^+)^{-1}=a^-\) and the identity respectively. So the second and third parts of the rule expand to:
\[ (a^-(a^+b^+a^+b^-)a^+)(a^{-4})(a^+(a^{+2}b^{+2})a^-)a^+b^- ~=~ (a^-a^+)b^+a^+(b^-(a^+a^{-4}a^{+3})b^+)(b^+(a^-a^+)b^-) \]
which reduces to the first part of the rule, \(b^+a^+\).
In the development version the function LoggedOnePassKB
returns a two-element list of lists. The first element is a set of logged rules and the second element is a long list of r-sequences, whatever they are! (Need more here.)
gap> l11 := LoggedRewriteReduce( l1[1] ); [ [ q8_M1*q8_M3, [ ], <identity ...> ], [ q8_M2^2, [ [ -4, <identity ...> ], [ 2, q8_M1^-2 ] ], q8_M1^2 ], [ q8_M2*q8_M4, [ ], <identity ...> ], [ q8_M3*q8_M1, [ ], <identity ...> ], [ q8_M4*q8_M2, [ ], <identity ...> ], [ q8_M1^3, [ [ 1, <identity. ..> ] ], q8_M3 ], [ q8_M1^2*q8_M2, [ [ 4, <identity. ..> ] ], q8_M4 ], [ q8_M1*q8_M2*q8_M1, [ [ 3, <identity ...> ] ], q8_M2 ], [ q8_M2*q8_M1*q8_M4, [ [ 3, q8_M3^-1 ] ], q8_M3] ] gap> Length( l11 ); 9 gap> l2 := LoggedKnuthBendix( l11 );; gap> l2[1]; [ [ q8_M1*q8_M3, [ ], <identity ...> ], [ q8_M2*q8_M1, [ [ 3, q8_M3^-1 ], [-1, <identity. ..> ], [ 4, q8_M1^-1 ] ], q8_M1*q8_M4 ], [ q8_M2^2, [ [ -4, <identity ...> ], [2, q8_M1^-2] ], q8_M1^2 ], [ q8_M2*q8_M3, [ [ -3, <identity ...> ] ], q8_M1*q8_M2 ], [ q8_M2*q8_M4, [ ], <identity ...> ], [ q8_M3*q8_M1, [ ], <identity ...> ], [ q8_M3*q8_M2, [ [ -1, <identity ...>], [4, q8_M1^-1 ] ], q8_M1*q8_M4 ], [ q8_M3^2, [ [ -1, <identity ...>] ], q8_M1^2 ], [ q8_M3*q8_M4, [ [ -1, <identity ...>], [ -2, q8_M1^-2], [ 4, <identity ...> ], [ 3, q8_M3^-1*q8_M2^-1 ], [ -3, <identity. ..> ] ], q8_M1*q8_M2 ], [ q8_M4*q8_M1, [ [ -4, <identity ...> ], [ 3, q8_M1^-1 ] ], q8_M1*q8_M2 ], [ q8_M4*q8_M2, [ ], <identity ...> ], [ q8_M4*q8_M3, [ [ -3, q8_M3^-1*q8_M4^-1] ], q8_M1*q8_M4 ], [ q8_M4^2, [ [ -4, <identity. ..> ] ], q8_M1^2 ], [ q8_M1^3, [ [ 1, <identity ...> ] ], q8_M3 ], [ q8_M1^2*q8_M2, [ [4, <identity. ..> ] ], q8_M4 ], [ q8_M1^2*q8_M4, [ [ -4, q8_M1^-2], [ 1, <identity ...> ] ], q8_M2 ] ] gap> Length( l2[1] ); 16 gap> Length( l2[2] ); 49
‣ LoggedReduceWordKB ( word, loggedrules ) | ( operation ) |
‣ LoggedOnePassReduceWord ( word, loggedrules ) | ( operation ) |
‣ ShorterLoggedRule ( logrule1, logrule2 ) | ( operation ) |
Given a word and a logged rewrite system, the function LoggedOnePassReduceWord
makes one reduction pass of the word (possibly involving several reductions) (as does OnePassReduceWord
in 2.2-2) and records this, using the log part of the rule(s) used and the position in the original word of the replaced part.
The function LoggedReduceWordKB
repeatedly applies OnePassLoggedReduceWord
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 loggedrules
is complete the reduced word is a unique normal form for that group element. The log of the reduction depends on the order in which the rules are applied.
The function ShorterLoggedrule
decides whether one logged rule is better than another, using the same criteria as ShorterRule
in 2.2-3. In the example we perform logged reductions of \(w_0 = a^9b^9\) corresponding to the ordinary reductions performed in the previous chapter (section 2.2-2).
In order to clarify the following output, note that, in the log below, \(b^9a^9\) reduces to \(b^5a^5\) in lw1
and to \(ba\) in the first lw2
. These expand to the initial w0
using the given logged parts as follows:
\[ (b^{+9}a^{+4}b^{-9})(b^{+4})b^{+5}a^{+5} ~=~ b^{+9}a^{+9} ~=~ (b^{+9}a^{+4}b^{-9})(b^{+4})(b^{+5}a^{+4}b^{-5})(b^{+4})b^+a^+\,. \]
The corresponding expansion of the final lw2
is too lengthy to include here.
gap> w0; q8_M2^9*q8_M1^9 gap> lw1 := LoggedOnePassReduceWord( w0, l0 ); [ [ [ 1, q8_M2^-9 ], [ 2, <identity ...> ] ], q8_M2^5*q8_M1^5 ] gap> lw2 := LoggedReduceWordKB( w0, l0 ); [ [ [ 1, q8_M2^-9 ], [ 2, <identity ...> ], [ 1, q8_M2^-5 ], [ 2, <identity ...> ] ], q8_M2*q8_M1 ] gap> lw2 := LoggedReduceWordKB( w0, l2[1] ); [ [ [ 3, q8_M3^-1*q8_M2^-8 ], [ -1, q8_M2^-8 ], [ 4, q8_M1^-1*q8_M2^-8 ], [ -4, <identity ...> ], [ 2, q8_M1^-2 ], [ -4, q8_M1^-1*q8_M2^-6*q8_M1^-2 ], [ 3, q8_M1^-2*q8_M2^-6*q8_M1^-2 ], [ 1, q8_M2^-1*q8_M1^-2*q8_M2^-6*q8_M1^-2 ], [ 4, <identity ...> ], [ 3, q8_M3^-1*q8_M2^-4*q8_M4^-1 ], [ -1, q8_M2^-4*q8_M4^-1 ], [ 4, q8_M1^-1*q8_M2^-4*q8_M4^-1 ], [ -4, q8_M4^-1 ], [ 2, q8_M1^-2*q8_M4^-1 ], [ -3, q8_M1^-1*q8_M4^-1*q8_M1^-1*q8_M2^-2*q8_M1^-2*q8_M4^-1 ], [ -4, <identity ...> ], [ 3, q8_M1^-1 ], [ 1, q8_M2^-1*q8_M1^-2*q8_M4^-1*q8_M1^-1*q8_M2^-1*(q8_M2^-1*q8_M1^-1)^2 ], [ 4, q8_M4^-1*q8_M1^-1*q8_M2^-1*(q8_M2^-1*q8_M1^-1)^2 ], [ 3, q8_M3^-1*q8_M1^-1 ], [ -1, q8_M1^-1 ], [ 4, q8_M1^-2 ], [ -4, q8_M4^-1*q8_M1^-2 ], [ 2, q8_M1^-2*q8_M4^-1*q8_M1^-2 ], [ -4, q8_M1^-2 ], [ 3, q8_M1^-3 ], [ -4, q8_M1^-2*q8_M2^-1*q8_M1^-3 ], [ 1, <identity ...> ], [ 3, q8_M3^-2 ], [ -1, q8_M3^-1 ], [ 4, q8_M1^-1*q8_M3^-1 ], [ -4, <identity ...> ], [ 3, q8_M1^-1 ], [ 3, q8_M3^-1*q8_M1^-1 ], [ -1, q8_M1^-1 ], [ 4, q8_M1^-2 ], [ -4, q8_M1^-2 ], [ 3, q8_M1^-3 ], [ 1, <identity ...> ], [ -1, <identity ...> ], [ 4, q8_M1^-1 ] ], q8_M1*q8_M4 ]
‣ LoggedRewritingSystemFpGroup ( loggedrules ) | ( attribute ) |
Given a group presentation, the function LoggedRewritingSystemFpGroup
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 rel
of the group there is a logged rule [rel,[[1,rel]],id]
. For each inverse relator there is a logged rule [ gen*inv, [], id ]
. The function then attempts a completion of the logged rewrite system. The rules in the final system are partially ordered by the function ShorterLoggedRule
.
gap> lwrs := LoggedRewritingSystemFpGroup( q8 ); [ [ q8_M4*q8_M2, [ ], <identity ...> ], [ q8_M3*q8_Ml, [ ], <identity ...> ], [ q8_M2*q8_M4, [ ], <identity ...> ], [ q8_Ml*q8_M3, [ ], <identity ...> ], [ q8_Ml^2*q8_M4, [ [ -8, q8_Ml^-2 ], [ 5, <identity ...> ] ], q8_M2 ], [ q8_Ml^2*q8_M2, [ [ 8, <identity ...> ] ], q8_M4 ], [ q8_Ml^3, [ [ 5, <identity ...> ] ], q8_M3 ], [ q8_M4^2, [ [ -8, <identity ...> ] ], q8_Ml^2 ], [ q8_M4*q8_M3, [ [ -7, q8_M3^-1*q8_M4^-1 ] ], q8_Ml*q8_M4 ], [ q8_M4*q8_Ml, [ [ -8, <identity. ..> ], [ 7, q8_Ml^-1 ] ], q8_Ml*q8_M2 ], [ q8_M3*q8_M4, [ [ -5, <identity ...>], [ -6, q8_Ml^-2 ], [ 8, <identity ...> ], [ 7, q8_M3^-1*q8_M2^-1 ], [ -7, <identity. ..> ] ], q8_Ml*q8_M2 ], [ q8_M3^2, [ [ -5, <identity ...>] ], q8_Ml^2 ], [ q8_M3*q8_M2, [ [ -5, <identity. ..> ], [ 8, q8_Ml^-1 ] ], q8_Ml*q8_M4 ], [ q8_M2*q8_M3, [ [ -7, <identity ...> ] ], q8_M1*q8_M2 ], [ q8_M2^2, [ [ -a, <identity ...> ], [ 6, q8_M1^-2 ] ], q8_M1^2 ], [ q8_M2*q8_M1, [ [ 7, q8_M3^-1 ], [ -5, <identity ...> ], [ a, q8_M1^-1 ] ], q8_M1*q8_M4 ] ] gap> Length( lwrs ); 16
Consider now the two-generator abelian group \(T\) considered in the previous chapter (2.2-1). Using the alternative ordering on the monoid generators, [ T_M1
\(=a^+\), T_M2
\(=a^-\), T_M3
\(=b^+\), T_M4
\(=b^-\) ]
, we obtain the following set of \(8\) logged rules. The last of these may be checked as follows:
\[ (b^+a^+(b^-a^-b^+a^+)a^-b^-)a^+b^+ ~=~ b^+a^+(b^-(a^-(b^+(a^+a^-)b^-)a^+)b^+) \]
and is a logged version of the rule \(b^+a^+ \to a^+b^+\).
gap> lrwsT := LoggedRewritingSystemFpGroup( T ); [ [ T_M4*T_M3, [ ], <identity ...> ], [ T_M3*T_M4, [ ], <identity ...> ], [ T_M2*T_M1, [ ], <identity ...> ], [ T_M1*T_M2, [ ], <identity ...> ], [ T_M4*T_M2, [ [ -5, <identity ...> ] ], T_M2*T_M4 ], [ T_M4*T_M1, [ [ 5, T_M1^-1 ] ], T_M1*T_M4 ], [ T_M3*T_M2, [ [ 5, T_M3^-1 ] ], T_M2*T_M3 ], [ T_M3*T_M1, [ [ -5, T_M1^-1*T_M3^-1 ] ], T_M1*T_M3 ] ]
generated by GAPDoc2HTML