Skip to content
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

(\theta + \pi) in rules matches on (\alpha) as (\alpha + \pi + \pi) in derivation #218

Open
SaraWolffs opened this issue Jun 1, 2018 · 2 comments
Labels
qpc2018 Issues filed during QPC 2018 practical rewriting

Comments

@SaraWolffs
Copy link
Contributor

SaraWolffs commented Jun 1, 2018

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.

@jvdwetering jvdwetering added rewriting qpc2018 Issues filed during QPC 2018 practical labels Jun 1, 2018
@jvdwetering 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
@hmillerbakewell
Copy link
Contributor

Could you possibly upload an example rule and graph? I can't reproduce it from your description.

@SaraWolffs
Copy link
Contributor Author

SaraWolffs commented Oct 17, 2018

issue218.tar.gz

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

demo-Z-pi-simp-bound-0
demo-red-id-0
demo-green-fusion-0

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.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
qpc2018 Issues filed during QPC 2018 practical rewriting
Projects
None yet
Development

No branches or pull requests

3 participants