search

zxcalc / quantomatic

Quantomatic is a tool for doing automated graph rewriting.
http://quantomatic.github.io
151 stars 22 forks source link

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

Open SaraWolffs opened 6 years ago

SaraWolffs commented 6 years ago

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.

hmillerbakewell commented 6 years ago

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

SaraWolffs commented 5 years ago

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) c8851ae3 (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.