You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert
See title. It makes perfect sense, but becomes an issue when it happens in a simplify script, because it can increase the number of explicit (\pi) angles, or keep it equal without changing any other measure. This is a problem for scripts which are intended to guarantee termination by monotonically decreasing graph complexity.
Since phases of (\beta + \pi) do occur during rewriting, scripts are weakened by having no rule for them, but due to this issue, I think no rule can be written which a script can use without risking non-termination.
The text was updated successfully, but these errors were encountered:
jvdwetering
changed the title
[qpc2018][rewriting] (\theta + \pi) in rules matches on (\alpha) as (\alpha + \pi + \pi) in derivation
(\theta + \pi) in rules matches on (\alpha) as (\alpha + \pi + \pi) in derivation
Jun 1, 2018
Apologies for the delay. This should be a minimal project demonstrating the issue. derivations/demo-issue-218.qderive was produced by running the included demo simproc (simprocs/demo.py) for a few steps on (if I did my build correctly) c8851ae (current stable/HEAD, v0.7). What I would hope to see is
after which nothing matches anymore. What happens instead is that it matches (lhs + \pi) on terms which don't contain an explicit \pi, which means Z-pi-simp-bound always matches here, which means it gets stuck in a loop instead of settling on an approximate normal form.
EDIT: last-minute change hadn't made it into the tarball. Should be fixed now.
See title. It makes perfect sense, but becomes an issue when it happens in a simplify script, because it can increase the number of explicit (\pi) angles, or keep it equal without changing any other measure. This is a problem for scripts which are intended to guarantee termination by monotonically decreasing graph complexity.
Since phases of (\beta + \pi) do occur during rewriting, scripts are weakened by having no rule for them, but due to this issue, I think no rule can be written which a script can use without risking non-termination.
The text was updated successfully, but these errors were encountered: