-
Notifications
You must be signed in to change notification settings - Fork 1
/
knuthBendix.txt
89 lines (78 loc) · 2.62 KB
/
knuthBendix.txt
1
# This code has been neither formally proven correct not thoroughly tested. def lenlex(u): if len(u[0])<len(u[1]): return([u[1],u[0]]); elif len(u[0])>len(u[1]): return(u); else: return(sorted(u,reverse=True));class monoid: def __init__(self,relations,ordering=lenlex): self.rels=relations; self.compare=ordering; def rewrite(self): return [self.compare(i) for i in self.rels];## The optional variable ordering is to be a function which takes two words## and sorts them into descending order.def overlaps(curr_rule,rule,monoid): returns=[]; for i in range(1,min(len(rule[0]),len(curr_rule[0]))): match=True; for j in range(i): if rule[0][j]!=curr_rule[0][j-i]: match=False; break; if match: returns.append(monoid.compare([curr_rule[0][:-i]+ rule[1],curr_rule[1]+rule[0][i:]])); for i in range(1,min(len(rule[0]),len(curr_rule[0]))): match=True; for j in range(i): if curr_rule[0][j]!=rule[0][j-i]: match=False; break; if match: returns.append(monoid.compare([rule[0][:-i]+ curr_rule[1],rule[1]+curr_rule[0][i:]])); return returns; def reduce(rules,xyz,monoid,new_rules): loop=True; while loop==True: loop=False; for i in rules: if xyz[0]==xyz[1]: return; if i[0] in xyz[0]: loop=True; xyz[0]=xyz[0].replace(i[0],i[1]); if i[0] in xyz[1]: loop=True; xyz[1]=xyz[1].replace(i[0],i[1]); if xyz[0]!=xyz[1]: abc=monoid.compare(xyz); rules.append(abc); new_rules.append(abc);def KnuthBendix(monoid,n=50): rules=monoid.rewrite(); for i in rules: if i[0]==i[1]: rules.remove(i); new_rules=rules.copy(); steps=0; while steps<n: if len(new_rules)==0: return rules; curr_rule=new_rules.pop(); for i in rules: returns=overlaps(curr_rule,i,monoid); for j in returns: reduce(rules,j,monoid,new_rules); steps+=1; print("Algorithm failed to terminate after",n, "steps."); #return rules;## Input the relations for the semigroup (as ordered pairs in a nested list)## and an ordering function. Generators which don't appear in the relations## won't affect the output of the algorithm. m=monoid([["aaa","a"],["bbbb","b"],["aab","ba"]]);print(KnuthBendix(m));