-
-
Notifications
You must be signed in to change notification settings - Fork 4.4k
New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
FpGroup: Implemented rewriting systems #12893
Conversation
if w1 < w2: | ||
s1 = w1 | ||
w1 = w2 | ||
w2 = s1 |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
The swap can be a single line.
len2 = len(r2) | ||
result = [] | ||
j = 0 | ||
while j < len1 + len2 - 1: |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Could this be a for loop like for j in range(1, len1 + len2)
?
# preceding ones. there is probably a better way | ||
# to handle this | ||
for r2 in lhs: | ||
overlaps = _overlaps(r1, r2) |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Is it necessary to do this also when r1 and r2 are the same? It seems that, in that case, the overlap w is also the same, and then _process_overlap(w, r1, r2)
would do nothing.
j = 0 | ||
while j < len1 + len2 - 1: | ||
j += 1 | ||
for j in range(1, len1 + len2 - 1): |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Note that this will make the last j
equal to len1 + len2 - 2
. Will that suffice?
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Nope, should change that.
using the group's rewriting system. If the system is | ||
confluent, the returned answer is necessarily correct. | ||
(If it isn't, `False` could be returned in some cases | ||
where in fact `word1 == word2`) |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Probably None
should be returned instead of False
if the system is not confluent.
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
That would make sense.
return self._is_confluent | ||
|
||
def _init_rules(self): | ||
rels = self.group.relators[:] |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
A local copy doesn't seem necessary.
# the overlaps. See [1], Section 3 for details. | ||
|
||
# overlaps on the right | ||
while len(s1) - len(s2) > 0: |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
If the difference is 1 and no cancelling occurs, then it may become -1. It seems that the rule will not be stored.
# the overlaps. See [1], Section 3 for details. | ||
|
||
# overlaps on the right | ||
while len(s1) - len(s2) > 1: |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
It looks like the rules where len(w1) - len(w2)
is 0 or 1 are not stored at all. Should that be the first thing to do before these two loops?
def add_rule(self, w1, w2): | ||
new_keys = set() | ||
if len(self.rules) + 1 > self.maxeqns: | ||
self._is_confluent = self._check_confluence() |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
_check_confidence
may try to add new rules. It should be called at most once The following might work:
if not self._max_exceeded:
self._max_exceeded = True
self._is_confluent = = self._check_confluence()
return ValueError("Too many rules were defined.")
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Hmm, actually maybe ._check_confluence()
shouldn't try to add rules at all. Otherwise if someone runs it, it could return False
while in practice the system is already confluent because of the rules it added.
sympy/combinatorics/fp_groups.py
Outdated
@@ -58,10 +58,8 @@ class FpGroup(DefaultPrinting): | |||
def __init__(self, fr_grp, relators): | |||
relators = _parse_relators(relators) | |||
# return the corresponding FreeGroup if no relators are specified |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
This line is no longer valid.
The list of rules is extended in the double loop in make_confluent but the for loop ignored the new elements. This is fixed now. Additionally, _reduce_redundacies was run too early in the loop and would sometimes lead to a dictionary key error. This is also taken care of now.
if the first rule in make_confluent is made redundant, the second loop should be broken, not continued
if not check: | ||
self.rules[s1] = s2 | ||
new_keys.add(s1) | ||
elif s1 < s2: |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Can this occur?
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Yes, when len(s1)==len(s2)
, e.g. a*b < b*a
.
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Even after these lines?
if w1 < w2:
w1, w2 = w2, w1
s1, s2 = w1, w2
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Ah, okay. Then it can't. Will change.
This PR implements rewriting systems for
FpGroup
s by creating a new classRewritingSystem
. This is added to anFpGroup
instance as an attribute._rewriting_system
, and three newFpGroup
methods are implemented:make_confluent()
attempts to make the group's rewriting system confluent by employing the Knuth-Bendix algorithmreduce()
takes a word as an argument and returns its reduced form under the rewriting systemequals()
takes two words and checks if they are equal under the rewriting system. If the system is confluent, this checks for actual equality of two elements ofFpGroup
.Additionally,
eliminate_words()
method from theFreeGroupElement
class is extended to handle the keyword_all
properly andeliminate_word()
is given a keyword attributeinverse
- when this is set toFalse
, the method won't try to substitute for the inverse of the requested substitution.