|
#############################################################################
##
## This file is part of GAP, a system for computational discrete algebra.
## This file's authors include Isabel Araújo and Andrew Solomon.
##
## Copyright of GAP belongs to its developers, whose names are too numerous
## to list here. Please refer to the COPYRIGHT file for details.
##
## SPDX-License-Identifier: GPL-2.0-or-later
##
## This file contains code for the Knuth-Bendix rewriting system for semigroups
## and monoids.
##
InstallGlobalFunction(EmptyKBDAG,function(genids)
local offset,deadend;
if Length(genids)=0 then
offset:=0;
deadend:=[];
else
offset:=Minimum(genids);
deadend:=ListWithIdenticalEntries(Maximum(genids)-offset+1,fail);
fi;
# index shifting so we always start at 1
if offset>0 then offset:=offset-1;
else offset:=1-offset;fi;
return rec(IsKBDAG:=true,
genids:=genids,
offset:=offset,
deadend:=deadend,
backpoint:=[],
dag:=ShallowCopy(deadend));
end);
InstallGlobalFunction(AddRuleKBDAG,function(d,left,idx)
local offset,node,j,a;
offset:=d.offset;
node:=d.dag;
for j in [1..Length(left)] do
a:=left[j]+offset;
if node[a]=fail then
if j=Length(left) then
# store index position
d.backpoint[idx]:=[node,a];
node[a]:=idx;
return true;
else
node[a]:=ShallowCopy(d.deadend); # at least one symbol more
node:=node[a];
fi;
elif IsList(node[a]) then
if j<Length(left) then
node:=node[a]; # go to next letter
else
# rule would reduce existing LHS
return fail;
fi;
else
#LHS could have been reduced with existing rules
return false;
fi;
od;
return true;
end);
InstallGlobalFunction(DeleteRuleKBDAG, function(d,left,idx)
local backpoint,i,a,node,offset;
backpoint:=d.backpoint;
backpoint[idx][1][backpoint[idx][2]]:=fail; # #rule indicator is gone
for i in [idx+1..Length(backpoint)] do
a:=backpoint[i][2];
#if backpoint[i][1][a]<>i then Error("poss");fi;
backpoint[i][1][a]:=backpoint[i][1][a]-1; # decrease index numbers
backpoint[i-1]:=backpoint[i]; # and correct back pointers
od;
Remove(backpoint);
# now trace through the word and kill nodes that are all fail
offset:=d.offset;
a:=Length(left)-2;
while a>-1 do
node:=d.dag;
for i in [1..a] do
node:=node[left[i]+offset];
od;
# where are we at length a+1?
if node[left[a+1]+offset]=d.deadend then
node[left[a+1]+offset]:=fail;
else
a:=0;
fi;
a:=a-1;
od;
end);
InstallGlobalFunction(RuleAtPosKBDAG,function(d,w,p)
local node,q;
node:=d.dag;
q:=p;
while IsList(node) and q<=Length(w) do
node:=node[w[q]+d.offset];
q:=q+1;
od;
if IsInt(node) then
return node; # the rule number to apply
else
# fail or list -- no rule applies
return fail;
fi;
end);
# Function to test validity of DAG structure
# BindGlobal("VerifyKBDAG",function(d,tzrules)
# local offset,node,j,a,idx,left,recurse;
# if Length(d!.backpoint)<>Length(tzrules) then Error("len");fi;
# offset:=d.offset;
# for idx in [1..Length(tzrules)] do
# left:=tzrules[idx][1];
#
# node:=d.dag;
# for j in [1..Length(left)] do
# a:=left[j]+offset;
# if node[a]=fail then
# Error("not stored");
# elif j=Length(left) then
# # end -- check
# if d.backpoint[idx]<>[node,a] or node[a]<>idx then Error("data!"); fi;
# else
# if not IsList(node[a]) then Error("too short");fi;
# node:=node[a]; # go to next letter
# fi;
# od;
# od;
#
# recurse:=function(n)
# local i,flag;
# if not IsList(n) then
# return;
# else
# flag:=true;
# for i in n do
# if IsList(i) then
# recurse(i);
# flag:=false;
# elif IsInt(i) then
# flag:=false;
# fi;
# od;
# if flag and n<>d.dag then Error("stored fail list");fi;
# fi;
# end;
#
# recurse(d.dag);
#end);
############################################################################
##
#R IsKnuthBendixRewritingSystemRep(<obj>)
##
## reduced - is the system known to be reduced
## fam - the family of elements of the fp smg/monoid
##
DeclareRepresentation("IsKnuthBendixRewritingSystemRep",
IsComponentObjectRep,
["family", "tzrules","pairs2check", "reduced", "ordering"]);
#############################################################################
##
#F CreateKnuthBendixRewritingSystem(<fam>, <wordord>)
##
## <wordord> is a reduction ordering
## (compatible with left and right multiplication).
##
## A Knuth Bendix rewriting system consists of a list of relations,
## which we call rules, and a list of pairs of numbers
## or more generalized form for saving memory (pairs2check).
## Each lhs of a rule has to be greater than its rhs
## (so when we apply a rule to a word, we are effectively reducing it -
## according to the ordering considered)
## Each number in a pair of the list pairs2check
## refers to one of the rules. A pair corresponds to a pair
## of rules where confluence was not yet checked (according to
## the Knuth Bendix algorithm).
## Pairs might also be given in the form of a 3-entry list
## ['A',x,l] to denote all pairs of the form [x,y] for y in l,
## respectively ['B',l,y] for pairs [x,y] with x in l.
##
## Note that at this stage the kb rws obtained might not be reduced
## (the same relation might even appear several times).
##
InstallGlobalFunction(CreateKnuthBendixRewritingSystem,
function(fam, wordord)
local r,kbrws,rwsfam,relations_with_correct_order,CantorList,relwco,
w,freefam,gens;
#changes the set of relations so that lhs is greater then rhs
# and removes trivial rules (like u=u)
relations_with_correct_order:=function(r,wordord)
local i,q;
q:=ShallowCopy(r);
for i in [1..Length(q)] do
if q[i][1]=q[i][2] then
Unbind(q[i]);
elif IsLessThanUnder(wordord,q[i][1],q[i][2]) then
q[i]:=[q[i][2],q[i][1]];
fi;
od;
return Unique(q);
end;
# generates the list of all pairs (x,y)
# where x,y are distinct elements of the set [1..n]
# encoded in compact form
CantorList:=function(n)
local i,l;
l:=[];
for i in [2..n] do
Add(l,['A',i,[1..i-1]]);
Add(l,['B',[1..i-1],i]);
od;
return(l);
end;
if ValueOption("isconfluent")=true then
CantorList:=n->[];
fi;
# check that fam is a family of elements of an fp smg or monoid
if not (IsElementOfFpMonoidFamily(fam) or IsElementOfFpSemigroupFamily(fam))
then
Error(
"Can only create a KB rewriting system for an fp semigroup or monoid");
fi;
# check the second argument is a reduction ordering
if not (IsOrdering(wordord) and IsReductionOrdering(wordord)) then
Error("Second argument must be a reduction ordering");
fi;
if IsElementOfFpMonoidFamily(fam) then
w:=CollectionsFamily(fam)!.wholeMonoid;
r:=RelationsOfFpMonoid(w);
freefam:=ElementsFamily(FamilyObj(FreeMonoidOfFpMonoid(w)));
gens:=GeneratorsOfMonoid(FreeMonoidOfFpMonoid(w));
else
w:=CollectionsFamily(fam)!.wholeSemigroup;
r:=RelationsOfFpSemigroup(w);
freefam:=ElementsFamily(FamilyObj(FreeSemigroupOfFpSemigroup(w)));
gens:=GeneratorsOfSemigroup(FreeSemigroupOfFpSemigroup(w));
fi;
rwsfam := NewFamily("Family of Knuth-Bendix Rewriting systems",
IsKnuthBendixRewritingSystem);
relwco:=relations_with_correct_order(r,wordord);
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,
generators:=gens));
kbrws!.kbdag:=EmptyKBDAG(Concatenation(List(gens,LetterRepAssocWord)));
if ValueOption("isconfluent")=true then
kbrws!.createdconfluent:=true;
fi;
if HasLetterRepWordsLessFunc(wordord) then
kbrws!.tzordering:=LetterRepWordsLessFunc(wordord);
else
kbrws!.tzordering:=false;
fi;
if IsElementOfFpMonoidFamily(fam) then
SetIsBuiltFromMonoid(kbrws,true);
else
SetIsBuiltFromSemigroup(kbrws,true);
fi;
return kbrws;
end);
#############################################################################
##
#A ReduceRules(<RWS>)
##
## Reduces the set of rules of a Knuth Bendix Rewriting System
##
InstallMethod(ReduceRules,
"for a Knuth Bendix rewriting system", true,
[ IsKnuthBendixRewritingSystem and IsKnuthBendixRewritingSystemRep and IsMutable ], 0,
function(rws)
local
r, # local copy of the rules
ptc, # do we need to check pairs
v; # a rule
ptc:=not (IsBound(rws!.createdconfluent) and rws!.createdconfluent);
r := ShallowCopy(rws!.tzrules);
rws!.tzrules:=[];
if ptc then
rws!.pairs2check:=[];
else
Unbind(rws!.pairs2check);
fi;
rws!.reduced := true;
if IsBound(rws!.kbdag) then
rws!.kbdag.stepback:=11;
fi;
for v in r do
AddRuleReduced(rws, v);
od;
if not ptc then
rws!.pairs2check:=[];
fi;
end);
# use bit lists to reduce the numbers of rules to test
# this should ultimately become part of the kernel routine
BindGlobal("ReduceLetterRepWordsRewSysNew",function(tzrules,w,dag)
local has,n,p,back;
if not IsRecord(dag) then
return ReduceLetterRepWordsRewSys(tzrules,w);
fi;
w:=ShallowCopy(w); # so we can replace
if IsBound(dag.stepback) then back:=dag.stepback;
else back:=11;fi;
repeat
has:=false;
p:=1;
while p<=Length(w) do
# find the rule applying at the position in the dag
n:=RuleAtPosKBDAG(dag,w,p);
if n<>fail then
# now apply rule
if Length(tzrules[n][1])=Length(tzrules[n][2]) then
w{[p..p+Length(tzrules[n][1])-1]}:=tzrules[n][2];
else
w:=Concatenation(w{[1..p-1]},tzrules[n][2],
w{[p+Length(tzrules[n][1])..Length(w)]});
fi;
has:=true;
# step a bit back. It doesn't really matter, as we only terminate if
# we have once run through the whole list without doing any change.
p:=Maximum(0,p-back);
fi;
p:=p+1;
od;
until has=false;
return w;
end);
InstallOtherMethod(AddRule,
"Fallback Method, call AddRuleReduced", true,
[ IsKnuthBendixRewritingSystem and IsMutable
and IsKnuthBendixRewritingSystemRep, IsList ], -1,
function(kbrws,v)
Info(InfoWarning,1,"Fallback method -- calling `AddRuleReduced` instead");
AddRuleReduced(kbrws,v);
end);
#############################################################################
##
#O AddRuleReduced(<RWS>, <tzrule>)
##
## Add a rule to a rewriting system and, if the system is already
## reduced it will remain reduced. Note, this also changes the pairs
## of rules to check.
##
## given a pair v of words that have to be equal it checks whether that
## happens or not and adjoin new rules if necessary. Then checks that we
## still have something reduced and keep removing and adding rules, until
## we have a reduced system where the given equality holds and everything
## that was equal before is still equal. It returns the resulting rws
##
## See Sims: "Computation with finitely presented groups".
##
InstallOtherMethod(AddRuleReduced,
"for a Knuth Bendix rewriting system and a rule", true,
[ IsKnuthBendixRewritingSystem and IsMutable
and IsKnuthBendixRewritingSystemRep, IsList ], 0,
function(kbrws,v)
local u,a,b,c,k,n,s,add_rule,fam,ptc,kbdag,abi,rem,
remove_rules;
# did anyone fiddle with the rules that there are invalid pairs?
# This happens e.g. in the fr package.
if IsBound(kbrws!.pairs2check)
# only do this if its within the fr package to not slow down other uses
and not IsBound(kbrws!.kbdag) then
b:=kbrws!.pairs2check;
k:=false;
a:=Length(kbrws!.tzrules);
for n in [1..Length(b)] do
s:=b[n];
if (Length(s)=2 and s[1]>a or s[2]>a)
or (s[1]='A' and s[2]>a) or (s[1]='B' and s[3]>a) then
b[n]:=fail; k:=true;
elif s[1]='A' and ForAny(s[3],x->x>a) then
s[3]:=Filtered(s[3],x->x<=a);
elif s[1]='B' and ForAny(s[2],x->x>a) then
s[2]:=Filtered(s[2],x->x<=a);
fi;
od;
if k then kbrws!.pairs2check:=Filtered(b,x->x<>fail);fi;
fi;
# the fr package assigns initial tzrules on its own, this messes up
# the dag structure. Delete ...
if IsBound(kbrws!.kbdag) and
Length(kbrws!.kbdag.backpoint)<>Length(kbrws!.tzrules) then
Info(InfoPerformance,2,
"Cannot use dag for lookup since rules were assigned directly");
#a:=EmptyKBDAG(kbrws!.kbdag.genids);
#kbrws!.kbdag:=a;
#for b in [1..Length(kbrws!.tzrules)] do
# AddRuleKBDAG(a,kbrws!.tzrules[b][1],b);
#od;
Unbind(kbrws!.kbdag);
fi;
# allow to give rule also as words in free monoid
if ForAll(v,IsAssocWord) and
IsIdenticalObj(kbrws!.freefam,FamilyObj(v[1])) then
v:=List(v,LetterRepAssocWord);
fi;
ptc:=IsBound(kbrws!.pairs2check);
if IsBound(kbrws!.kbdag) then
kbdag:=kbrws!.kbdag;
else
kbdag:=fail;
fi;
# older, less efficient version for just single rule
# #given a Knuth Bendix Rewriting System, kbrws,
# #removes rule i of the set of rules of kbrws and
# #modifies the list pairs2check in such a way that the previous indexes
# #are modified so they correspond to same pairs as before
# remove_rule:=function(i)
# local j,q,l,kk;
#
# if kbdag<>fail then
# # update lookup structure
# DeleteRuleKBDAG(kbdag,kbrws!.tzrules[i][1],i);
# fi;
#
# #remove rule from the set of rules
# #q:=kbrws!.tzrules{[1..i-1]};
# #Append(q,kbrws!.tzrules{[i+1..Length(kbrws!.tzrules)]});
# #kbrws!.tzrules:=q;
# q:=kbrws!.tzrules;
# Remove(q,i);
#
# if ptc then
# #delete pairs of indexes that include i
# #and change occurrences of indexes k greater than i in the
# #list of pairs and change them to k-1
#
# kk:=kbrws!.pairs2check;
#
# #So we'll construct a new list with the right pairs
# l:=[];
# for j in [1..Length(kk)] do
# if Length(kk[j])=2 then
# if kk[j][1]<i then
# if kk[j][2]<i then
# Add(l,kk[j]);
# elif kk[j][2]>i then
# # reindex
# Add(l,[kk[j][1],kk[j][2]-1]);
# fi;
# elif kk[j][1]>i then
# if kk[j][2]<i then
# # reindex
# Add(l,[kk[j][1]-1,kk[j][2]]);
# elif kk[j][2]>i then
# # reindex
# Add(l,[kk[j][1]-1,kk[j][2]-1]);
# fi;
# # else rule gets deleted
# fi;
# elif kk[j][1]='A' then
# if kk[j][2]<i then
# Add(l,kk[j]); # all smaller, no delete
# elif kk[j][2]>i then
# Add(l,['A',kk[j][2]-1,Concatenation(
# Filtered(kk[j][3],x->x<i),Filtered(kk[j][3],x->x>i)-1)]);
# # else pairs deleted since rule deleted
# fi;
# else # 'B' case
# if kk[j][3]<i then
# Add(l,kk[j]); # all smaller, no delete
# elif kk[j][3]>i then
# Add(l,['B',Concatenation(Filtered(kk[j][2],x->x<i),
# Filtered(kk[j][2],x->x>i)-1),kk[j][3]-1]);
# # else pairs deleted since rule deleted
# fi;
# fi;
#
# od;
# kbrws!.pairs2check:=l;
# fi;
#
# end;
#given a Knuth Bendix Rewriting System, kbrws,
#removes the rules indexed by weg from the set of rules of kbrws and
#modifies the list pairs2check in such a way that the previous indexes
#are modified so they correspond to same pairs as before
remove_rules:=function(weg)
local j,q,a,l,kk,i,neu,x,y;
if kbdag<>fail then
for i in weg do
# update lookup structure
DeleteRuleKBDAG(kbdag,kbrws!.tzrules[i][1],i);
od;
fi;
#remove rule from the set of rules
q:=kbrws!.tzrules;
kk:=Minimum(weg);
neu:=[1..kk-1];
for i in [kk..Length(q)] do
if i in weg then
neu[i]:=fail;
else
q[kk]:=q[i];
neu[i]:=kk;
kk:=kk+1;
fi;
od;
for i in [Length(q),Length(q)-1..Length(q)-Length(weg)+1] do
Unbind(q[i]);
od;
if ptc then
#delete pairs of indexes that include i
#and change occurrences of indexes k greater than i in the
#list of pairs and change them to k-1
kk:=kbrws!.pairs2check;
#So we'll construct a new list with the right pairs
l:=[];
for j in [1..Length(kk)] do
if Length(kk[j])=2 then
if not(kk[j][1] in weg or kk[j][2] in weg) then
Add(l,neu{kk[j]});
# otherwise, one is killed
fi;
elif kk[j][1]='A' and not kk[j][2] in weg then
#a:=Difference(neu{kk[j][3]},[fail]);
a:=kk[j][3];
x:=neu[a[1]];y:=neu[Last(a)];
if IsRange(a) and x<>fail and y<>fail then
a:=[x..y];
else
a:=Set(neu{kk[j][3]});
if Last(a)=fail then Remove(a);fi;
fi;
if Length(a)>0 then
Add(l,['A',neu[kk[j][2]],a]);
fi;
elif kk[j][1]='B' and not kk[j][3] in weg then
#a:=Difference(neu{kk[j][2]},[fail]);
a:=kk[j][2];
x:=neu[a[1]];y:=neu[Last(a)];
if IsRange(a) and x<>fail and y<>fail then
a:=[x..y];
else
a:=Set(neu{kk[j][2]});
if Last(a)=fail then Remove(a);fi;
fi;
if Length(a)>0 then
Add(l,['B',a,neu[kk[j][3]]]);
fi;
fi;
od;
kbrws!.pairs2check:=l;
fi;
end;
#given a Knuth Bendix Rewriting System this function returns it
#with the given extra rule adjoined to the set of rules
#and the necessary pairs adjoined to pairs2check
#(the pairs that we have to put in pairs2check correspond to the
#new rule together with all the ones that were in the set of rules
#previously)
add_rule:=function(u,kbrws)
local l,i,j,n,p,any;
#insert rule
Add(kbrws!.tzrules,u);
if kbdag<>fail then
l:=AddRuleKBDAG(kbdag,u[1],Length(kbrws!.tzrules));
if l<>true then Error("rulesubset"); fi;
fi;
#VerifyKBDAG(kbdag,kbrws!.tzrules);
if ptc then
#insert new pairs
l:=kbrws!.pairs2check;
n:=Length(kbrws!.tzrules);
Add(l,[n,n]);
#for i in [1..n-1] do
# Append(l,[[i,n],[n,i]]);
#od;
if n>1 then
Add(l,['A',n,[1..n-1]]);
Add(l,['B',[1..n-1],n]);
fi;
kbrws!.pairs2check:=l;
fi;
if IsBound(kbrws!.invmap) then
# free cancel part
u:=List(u,ShallowCopy);
i:=1;
while i<=Length(u[1]) and i<=Length(u[2]) and u[1][i]=u[2][i] do
i:=i+1;
od;
any:=false;
for j in [i..Length(u[2])] do
p:=Concatenation(kbrws!.invmap{u[1]{[j,j-1..i]}},
u[2]{[i..j]});
l:=ReduceLetterRepWordsRewSysNew(kbrws!.tzrules,p,kbdag);
#Print("fellow ",List(u,Length),Length(p)," ",Length(l),"\n");
if not l in kbrws!.fellowTravel then
Add(kbrws!.fellowTravel,l);
any:=true;
if Length(kbrws!.fellowTravel) mod 200=0 then
kbrws!.fellowTravel:=List(kbrws!.fellowTravel,
x->ReduceLetterRepWordsRewSysNew(kbrws!.tzrules,x,kbdag));
kbrws!.fellowTravel:=Unique(kbrws!.fellowTravel);
fi;
fi;
od;
if any then
kbrws!.flaute:=0;
else
kbrws!.flaute:=kbrws!.flaute+1;
fi;
fi;
end;
#the stack is a list of pairs of words such that if two words form a pair
#they have to be equivalent, that is, they have to reduce to same word
#TODO
fam:=kbrws!.freefam;
#we put the pair v in the stack
s:=[v];
#while the stack is non empty
while not(IsEmpty(s)) do
#VerifyKBDAG(kbdag,kbrws!.tzrules);
#pop the first rule from the stack
#use rules available to reduce both sides of rule
u:=s[1];
s:=s{[2..Length(s)]};
a:=ReduceLetterRepWordsRewSysNew(kbrws!.tzrules,u[1],kbdag);
b:=ReduceLetterRepWordsRewSysNew(kbrws!.tzrules,u[2],kbdag);
#if both sides reduce to different words
#have to adjoin a new rule to the set of rules
if not(a=b) then
#TODO
if kbrws!.tzordering=false then
c:=IsLessThanUnder(kbrws!.ordering,
AssocWordByLetterRep(fam,a),AssocWordByLetterRep(fam,b));
else
c:=kbrws!.tzordering(a,b);
fi;
if c then
c:=a; a:=b; b:=c;
fi;
#Now we have to check if by adjoining this rule
#any of the other active ones become redundant
n:=Length(kbrws!.tzrules);
# go descending to avoid having to reindex
rem:=[];
for k in [n,n-1..1] do
#if lhs of rule k contains lhs of new rule
#as a subword then we delete rule k
#but add it to the stack, since it has to still hold
if PositionSublist(kbrws!.tzrules[k][1],a,0)<>fail then
Add(s,kbrws!.tzrules[k]);
Add(rem,k);
n:=Length(kbrws!.tzrules)-1;
fi;
od;
if Length(rem)>0 then
remove_rules(rem);
fi;
#VerifyKBDAG(kbdag,kbrws!.tzrules);
# and store new rule
add_rule([a,b],kbrws);
kbrws!.reduced := false;
n:=Length(kbrws!.tzrules);
for k in [n,n-1..1] do
#else if rhs of rule k contains the new rule
#as a subword then we use the new rule
#to reduce that rhs
if PositionSublist(kbrws!.tzrules[k][2],a,0)<>fail then
kbrws!.tzrules[k][2]:=
ReduceLetterRepWordsRewSysNew(kbrws!.tzrules,
kbrws!.tzrules[k][2],kbdag);
fi;
od;
fi;
od;
kbrws!.reduced := true;
end);
#############################################################################
##
#M MakeKnuthBendixRewritingSystemConfluent (<KBRWS>)
##
## RWS is a Knuth Bendix Rewriting System
## This function takes a Knuth Bendix Rws (ie a set of rules
## and a set of pairs which indicate the rules that
## still have to be checked for confluence) and
## applies the Knuth Bendix algorithm for strigs to it to get a reduced
## confluent rewriting system.
##
## Confluence means the following: if w is a word which can be reduced
## using two different rules, say w->u and w->v, then the irreducible forms
## of u and v are the same word.
##
## To construct a rws from a set of rules consists of adjoining new
## rules if necessary to be sure the confluence property holds
##
## This implementation of Knuth-bendix also guarantees that we will
## obtain a reduced rws, meaning that there are not redundant rules
##
## Note (see Sims, `Computation with finitely presented groups', 1994)
## a reduced confluent rewriting system for a semigroup with a given set of
## generators is unique, under a given ordering.
InstallGlobalFunction( MakeKnuthBendixRewritingSystemConfluent,
function ( rws )
Info( InfoKnuthBendix, 1, "MakeKnuthBendixRewritingSystemConfluent called" );
# call the KB plugin
KB_REW.MakeKnuthBendixRewritingSystemConfluent(rws);
Info( InfoKnuthBendix, 1, "KB terminates with ",Length(rws!.tzrules),
" rules" );
end);
# We store compressed data -- expand, (and also delete old stuff)
BindGlobal("KBRWSUnpackPairsAt",function(kbrws,p)
local i,a;
i:=kbrws!.pairs2check[p];
if IsChar(i[1]) then
# We store compressed data -- expand, (and also delete old stuff)
if i[1]='A' then
a:=List(i[3],x->[i[2],x]);
elif i[1]='B' then
a:=List(i[2],x->[x,i[3]]);
else Error("kind"); fi;
kbrws!.pairs2check:=Concatenation(a,kbrws!.pairs2check{[p+1..Length(kbrws!.pairs2check)]});
p:=1;
fi;
return p;
end);
#u and v are pairs of rules, kbrws is a kb RWS
#look for proper overlaps of lhs (lhs of u ends as lhs of v starts)
#Check confluence does not fail here, adjoining extra rules if necessary
BindGlobal("KBOverlaps",function(ui,vi,kbrws,p)
local u,v,m,k,a,c,lsu,lsv,lu,eq,i,j;
# work around copied code in kan package
if IsChar(ui) then # must unpack
p:=KBRWSUnpackPairsAt(kbrws,p);
vi:=kbrws!.pairs2check[p];
ui:=vi[1];vi:=vi[2];
fi;
u:=kbrws!.tzrules[ui]; v:=kbrws!.tzrules[vi];
lsu:=u[1];
lu:=Length(lsu);
lsv:=v[1];
#we are only going to consider proper overlaps
#m:=Minimum(lu,Length(lsv))-1;
m:=Length(lsv)-1;
if lu<=m then
m:=lu-1;
fi;
#any overlap will have length less than m
k:=1;
while k<=m do
#if the last k letters of u[1] are the same as the 1st k letters of v[1]
#they overlap
#if Subword(u[1],Length(u[1])-k+1,Length(u[1]))=Subword(v[1],1,k) then
eq:=true;
i:=lu-k+1;
j:=1;
while eq and j<=k do
eq:=lsu[i]=lsv[j];
i:=i+1;
j:=j+1;
od;
if eq then
#a:=Subword(u[1],1,Length(u[1])-k)*v[2];
#c:=u[2]*Subword(v[1],k+1,Length(v[1]));
# we can't have cancellation
a:=Concatenation(lsu{[1..lu-k]},v[2]);
c:=Concatenation(u[2],lsv{[j..Length(lsv)]});
#for guarantee confluence a=c has to hold
#we change rws, if necessary, so a=c is verified
if a <> c then
# `AddRuleReduced' might affect the pairs. So first throw away the
# already used pairs
kbrws!.pairs2check:=
kbrws!.pairs2check{[p+1..Length(kbrws!.pairs2check)]};
p:=0; # no remaining pair was looked at
AddRuleReduced(kbrws,[a,c]);
fi;
fi;
k:=k+1;
od;
return p;
end);
############################################################
#
# Function proper
#
###########################################################
BindGlobal("GKB_MakeKnuthBendixRewritingSystemConfluent",
function(kbrws)
local pn,lp,rl,p,i;
if IsBound(kbrws!.invmap) then
kbrws!.fellowTravel:=[];
fi;
kbrws!.flaute:=0; # how often no new fellow traveler?
# kbrws!.reduced is true than it means that the system know it is
# reduced. If it is false it might be reduced or not.
if not kbrws!.reduced then
ReduceRules(kbrws);
fi;
# we check all pairs of relations for overlaps. In most cases there will
# be no overlaps. Therefore cally an inde xp in the pairs list and reduce
# this list, only if `AddRules' gets called. This avoids creating a lot of
# garbage lists.
p:=1;
rl:=49;
pn:=Length(kbrws!.pairs2check);
lp:=Length(kbrws!.pairs2check);
while lp>=p do
i:=kbrws!.pairs2check[p];
if IsChar(i[1]) then
# We store compressed data -- expand, (and also delete old stuff)
p:=KBRWSUnpackPairsAt(kbrws,p);
fi;
p:=KBOverlaps(i[1],i[2],kbrws,p)+1;
lp:=Length(kbrws!.pairs2check);
if Length(kbrws!.tzrules)>rl
or AbsInt(lp-pn)>10000 then
Info(InfoKnuthBendix,1,Length(kbrws!.tzrules)," rules, ",
lp," pairs, ",kbrws!.flaute," no new fellow");
rl:=Length(kbrws!.tzrules)+49;
pn:=lp;
fi;
od;
kbrws!.pairs2check:=[];
end);
GAPKB_REW.MakeKnuthBendixRewritingSystemConfluent :=
GKB_MakeKnuthBendixRewritingSystemConfluent;
if IsHPCGAP then
MakeReadOnlyObj( GAPKB_REW );
fi;
#############################################################################
##
#M MakeConfluent (<KB RWS>)
##
InstallMethod(MakeConfluent,
"for Knuth Bendix Rewriting System",
true,
[IsKnuthBendixRewritingSystem and IsKnuthBendixRewritingSystemRep and IsMutable
and IsBuiltFromSemigroup],0,
function(kbrws)
local rws;
MakeKnuthBendixRewritingSystemConfluent(kbrws);
# if the semigroup of the kbrws does not have a
# ReducedConfluentRws build one from kbrws and then store it in
# the semigroup
if not HasReducedConfluentRewritingSystem(
SemigroupOfRewritingSystem(kbrws)) then
rws := ReducedConfluentRwsFromKbrwsNC(kbrws);
SetReducedConfluentRewritingSystem(SemigroupOfRewritingSystem(kbrws),
rws);
fi;
end);
InstallMethod(MakeConfluent,
"for Knuth Bendix Rewriting System",
true,
[IsKnuthBendixRewritingSystem and IsKnuthBendixRewritingSystemRep and IsMutable
and IsBuiltFromMonoid],0,
function(kbrws)
local rws;
MakeKnuthBendixRewritingSystemConfluent(kbrws);
# if the monoid of the kbrws does not have a
# ReducedConfluentRws build one from kbrws and then store it in
# the monoid
if not HasReducedConfluentRewritingSystem(
MonoidOfRewritingSystem(kbrws)) then
rws := ReducedConfluentRwsFromKbrwsNC(kbrws);
SetReducedConfluentRewritingSystem(MonoidOfRewritingSystem(kbrws),
rws);
fi;
end);
#############################################################################
##
#P IsReduced( <rws> )
##
## True iff the rws is reduced
## A rws is reduced if for each (u,v) in rws both u and v are
## irreducible with respect to rws-{(u,v)}
##
InstallMethod(IsReduced,
"for a Knuth Bendix rewriting system", true,
[IsKnuthBendixRewritingSystem and IsKnuthBendixRewritingSystemRep and IsMutable], 0,
function(kbrws)
local i, copy_of_kbrws, u, tzr;
# if the rws already knows it is reduced return true
if kbrws!.reduced then return true; fi;
tzr := TzRules(kbrws);
for i in [1..Length(tzr)] do
u := tzr[i];
copy_of_kbrws := ShallowCopy(kbrws);
copy_of_kbrws!.tzrules := [];
Append(copy_of_kbrws!.tzrules,kbrws!.tzrules{[1..i-1]});
Append(copy_of_kbrws!.tzrules,kbrws!.tzrules
{[i+1..Length(kbrws!.tzrules)]});
if ReduceLetterRepWordsRewSys(copy_of_kbrws!.tzrules,u[1])<>u[1] or
ReduceLetterRepWordsRewSys(copy_of_kbrws!.tzrules,u[2])<>u[2] then
return false;
fi;
od;
return true;
end);
#############################################################################
##
#M KnuthBendixRewritingSystem(<fam>)
#M KnuthBendixRewritingSystem(<fam>,<wordord>)
#M KnuthBendixRewritingSystem(<m>)
#M KnuthBendixRewritingSystem(<m>,<wordord>)
#M KnuthBendixRewritingSystem(<s>)
#M KnuthBendixRewritingSystem(<s>,<wordord>)
##
## creates the Knuth Bendix rewriting system for a family of
## word of an fp monoid or semigroup
## using a supplied reduction ordering.
##
## We also allow using a function giving the ordering
## to assure compatibility with gap4.2
## In that case the function <lteq> should be the less than or equal
## function of a reduction ordering (no checking is performed)
##
InstallMethod(KnuthBendixRewritingSystem,
"for a family of words of an fp semigroup and on ordering on that family", true,
[IsElementOfFpSemigroupFamily, IsOrdering], 0,
function(fam,wordord)
local freefam,kbrws;
freefam := ElementsFamily(FamilyObj(fam!.freeSemigroup));
# the ordering has to be an ordering on the family freefam
if not freefam=FamilyForOrdering(wordord) then
Error("family <fam> and ordering <wordord> are not compatible");
fi;
kbrws := CreateKnuthBendixRewritingSystem(fam,wordord);
return kbrws;
end);
InstallMethod(KnuthBendixRewritingSystem,
"for a family of words of an fp monoid and on ordering on that family", true,
[IsElementOfFpMonoidFamily, IsOrdering], 0,
function(fam,wordord)
local freefam,kbrws;
freefam := ElementsFamily(FamilyObj(fam!.freeMonoid));
# the ordering has to be an ordering on the family fam
if not freefam=FamilyForOrdering(wordord) then
Error("family <fam> and ordering <wordord> are not compatible");
fi;
kbrws := CreateKnuthBendixRewritingSystem(fam,wordord);
return kbrws;
end);
InstallOtherMethod(KnuthBendixRewritingSystem,
"for an fp semigroup and an order on the family of words of the underlying free semigroup", true,
[IsFpSemigroup, IsOrdering], 0,
function(s,wordord)
local fam;
fam := ElementsFamily(FamilyObj(s));
return KnuthBendixRewritingSystem(fam,wordord);
end);
InstallOtherMethod(KnuthBendixRewritingSystem,
"for an fp monoid and an order on the family of words of the underlying free monoid", true,
[IsFpMonoid, IsOrdering], 0,
function(m,wordord)
local fam;
fam := ElementsFamily(FamilyObj(m));
return KnuthBendixRewritingSystem(fam,wordord);
end);
InstallOtherMethod(KnuthBendixRewritingSystem,
"for an fp semigroup and a function", true,
[IsFpSemigroup, IsFunction], 0,
function(s,lt)
local wordord,fam;
wordord := OrderingByLessThanOrEqualFunctionNC(ElementsFamily
(FamilyObj(FreeSemigroupOfFpSemigroup(s))),lt,[IsReductionOrdering]);
fam := ElementsFamily(FamilyObj(s));
return KnuthBendixRewritingSystem(fam,wordord);
end);
InstallOtherMethod(KnuthBendixRewritingSystem,
"for an fp monoid and a function", true,
[IsFpMonoid, IsFunction], 0,
function(m,lt)
local wordord,fam;
wordord := OrderingByLessThanOrEqualFunctionNC(ElementsFamily
(FamilyObj(FreeMonoidOfFpMonoid(m))),lt,[IsReductionOrdering]);
fam := ElementsFamily(FamilyObj(m));
return KnuthBendixRewritingSystem(fam,wordord);
end);
#############################################################################
##
#M KnuthBendixRewritingSystem(<m>)
##
## Create the a KB rewriting system for the fp monoid <m> using the
## shortlex order.
##
InstallOtherMethod(KnuthBendixRewritingSystem,
"for an fp monoid", true,
[IsFpMonoid], 0,
function(m)
return KnuthBendixRewritingSystem(m,
ShortLexOrdering(ElementsFamily(FamilyObj(
FreeMonoidOfFpMonoid(m)))));
end);
InstallOtherMethod(KnuthBendixRewritingSystem,
"for an fp semigroup", true,
[IsFpSemigroup], 0,
function(s)
return KnuthBendixRewritingSystem(s,
ShortLexOrdering(ElementsFamily(FamilyObj(
FreeSemigroupOfFpSemigroup(s)))));
end);
#############################################################################
##
#M MonoidOfRewritingSystem(<KB RWS>)
##
## for a Knuth Bendix Rewriting System
## returns the monoid of the rewriting system
##
InstallMethod(MonoidOfRewritingSystem,
"for a Knuth Bendix rewriting system", true,
[IsRewritingSystem and IsBuiltFromMonoid], 0,
function(kbrws)
local fam;
fam := FamilyForRewritingSystem(kbrws);
return CollectionsFamily(fam)!.wholeMonoid;
end);
#############################################################################
##
#M SemigroupOfRewritingSystem(<KB RWS>)
##
## for a Knuth Bendix Rewriting System
## returns the semigroup of the rewriting system
##
InstallMethod(SemigroupOfRewritingSystem,
"for a Knuth Bendix rewriting system", true,
[IsRewritingSystem and IsBuiltFromSemigroup], 0,
function(kbrws)
local fam;
fam := FamilyForRewritingSystem(kbrws);
return CollectionsFamily(fam)!.wholeSemigroup;
end);
#############################################################################
##
#M Rules(<KB RWS>)
##
## for a Knuth Bendix Rewriting System
## returns the set of rules of the rewriting system
##
InstallMethod(Rules,
"for a Knuth Bendix rewriting system", true,
[IsKnuthBendixRewritingSystem and IsKnuthBendixRewritingSystemRep], 0,
function(kbrws)
local fam;
fam:=kbrws!.freefam;
return List(kbrws!.tzrules,
i->[AssocWordByLetterRep(fam,i[1]),AssocWordByLetterRep(fam,i[2])]);
end);
#############################################################################
##
#M TzRules(<KB RWS>)
##
## for a Knuth Bendix Rewriting System
## returns the set of rules of the rewriting system in compact form
##
InstallMethod(TzRules,"for a Knuth Bendix rewriting system", true,
[IsKnuthBendixRewritingSystem and IsKnuthBendixRewritingSystemRep], 0,
function(kbrws)
return List(kbrws!.tzrules,i->[ShallowCopy(i[1]),ShallowCopy(i[2])]);
end);
#############################################################################
##
#A OrderingOfRewritingSystem(<rws>)
##
## for a rewriting system rws
## returns the order used by the rewriting system
##
InstallMethod(OrderingOfRewritingSystem,
"for a Knuth Bendix rewriting system", true,
[IsKnuthBendixRewritingSystem and IsKnuthBendixRewritingSystemRep], 0,
function(kbrws)
return kbrws!.ordering;
end);
#############################################################################
##
#A FamilyForRewritingSystem(<rws>)
##
## for a rewriting system rws
##
InstallMethod(FamilyForRewritingSystem,
"for a Knuth Bendix rewriting system", true,
[IsKnuthBendixRewritingSystem and IsKnuthBendixRewritingSystemRep], 0,
function(kbrws)
return kbrws!.family;
end);
############################################################################
##
#A ViewObj(<KB RWS>)
##
##
InstallMethod(ViewObj, "for a Knuth Bendix rewriting system", true,
[IsKnuthBendixRewritingSystem and IsBuiltFromMonoid], 0,
function(kbrws)
Print("Knuth Bendix Rewriting System for ");
Print(MonoidOfRewritingSystem(kbrws));
Print(" with rules \n");
Print(Rules(kbrws));
end);
InstallMethod(ViewObj, "for a Knuth Bendix rewriting system", true,
[IsKnuthBendixRewritingSystem and IsBuiltFromSemigroup], 0,
function(kbrws)
Print("Knuth Bendix Rewriting System for ");
Print(SemigroupOfRewritingSystem(kbrws));
Print(" with rules \n");
Print(Rules(kbrws));
end);
###############################################################################
##
#M ShallowCopy
##
InstallMethod( ShallowCopy,
"for a Knuth Bendix rewriting system",
true,
[IsKnuthBendixRewritingSystem and IsKnuthBendixRewritingSystemRep], 0,
function(kbrws)
local new;
new:=Objectify( Subtype( TypeObj(kbrws), IsMutable ),
rec(
generators:=StructuralCopy(kbrws!.generators),
family := kbrws!.family,
reduced := false,
tzrules:= StructuralCopy(kbrws!.tzrules),
pairs2check:= [],
ordering :=kbrws!.ordering,
freefam := kbrws!.freefam,
tzordering := kbrws!.tzordering));
if IsBound(kbrws!.kbdag) then
new!.kbdag:=StructuralCopy(kbrws!.kbdag);
fi;
return new;
end);
###############################################################################
##
#M \=
##
InstallMethod( \=,
"for two Knuth-Bendix rewriting systems",
IsIdenticalObj,
[IsKnuthBendixRewritingSystem and IsKnuthBendixRewritingSystemRep,
IsKnuthBendixRewritingSystem and IsKnuthBendixRewritingSystemRep],0,
function(rws1,rws2)
return
rws1!.family=rws2!.family
and
IsSubset(rws1!.tzrules,rws2!.tzrules)
and
IsSubset(rws2!.tzrules,rws1!.tzrules)
and
rws1!.ordering=rws2!.ordering;
end);
[ Dauer der Verarbeitung: 0.39 Sekunden
(vorverarbeitet)
]
|
