rotate_simp is slow!
6 views
Skip to first unread message
Ross Duncan
Nov 3, 2016, 8:29:55 AM11/3/16
to quant...@googlegroups.com
Maybe this is not news to anyone, but rotate_simp has some performance issues. I’ve been running it on a graph with ~25 vertices, avg degree 4, for about 24 hours now and it has found only 3 rewrites!
So I think the following could be a nice project for a student at some future point:
1. An analysis of the runtime of rotate_simp — which necessarily will include how !-box matching works
2. Produce a new tactic equivalent to rotate_simp with better performance
3. A proof of the equivalence of the new tactic and the original rotate_simp.
It’s probably a bit late in the calendar for this to happen this year, but something worth doing for next year.
-r
So I think the following could be a nice project for a student at some future point:
1. An analysis of the runtime of rotate_simp — which necessarily will include how !-box matching works
2. Produce a new tactic equivalent to rotate_simp with better performance
3. A proof of the equivalence of the new tactic and the original rotate_simp.
It’s probably a bit late in the calendar for this to happen this year, but something worth doing for next year.
-r
Ross Duncan
Nov 3, 2016, 10:34:00 AM11/3/16
to quant...@googlegroups.com
A small follow-up: a couple of hours later it terminated with the attached image as its final state. It’s obviously not normal. However at that point it seems that core fell over so I’m not sure if rotate_simp terminated cleanly or just crashed out.
-r
Aleks Kissinger
Nov 4, 2016, 5:33:25 AM11/4/16
to quant...@googlegroups.com
Wow, 24 hours is some dedication. :)
I know exactly why its so slow. There is currently no way to tell the matcher to start by matching vertex X in pattern to vertex Y in target then go from there. So, it just tries all matchings until it gets lucky and rewrites the correct thing. And it does this for *every* rotation step. Since the rotate rule has 3 bboxes and 3 nested bboxes, this finds a lot of matchings!
This is very nearly fixable. Simprocs just need to be able to hook into the matcher appropriately. I'll try to have a look at this over the weekend.
I think having a student to work on tactics is a good idea, since a lot can be done there. For instance, implementing Miriam's procedure for reducing cliffords to a quasi-normal form.
-r
--
You received this message because you are subscribed to the Google Groups "Quantomatic" group.
To unsubscribe from this group and stop receiving emails from it, send an email to quantomatic+unsubscribe@googlegroups.com.
To post to this group, send email to quant...@googlegroups.com.
Visit this group at https://groups.google.com/group/quantomatic.
For more options, visit https://groups.google.com/d/optout.
Aleks Kissinger
Nov 4, 2016, 9:23:27 AM11/4/16
to quant...@googlegroups.com
Can you send me the qgraph file you are trying to reduce?
Ross Duncan
Nov 4, 2016, 9:41:51 AM11/4/16
to quant...@googlegroups.com
Hi Aleks,
Here’s 2 qgrpahs. First one is the one at the start of the mega long rotate_simp run, the second is the point where it gave up/fell over. It’s pretty easy to reduce the graph by hand from there using (bialg [inverse] ; basic_simp)*
-r
Here’s 2 qgrpahs. First one is the one at the start of the mega long rotate_simp run, the second is the point where it gave up/fell over. It’s pretty easy to reduce the graph by hand from there using (bialg [inverse] ; basic_simp)*
-r
Aleks Kissinger
Nov 4, 2016, 11:23:39 AM11/4/16
to quant...@googlegroups.com
okay, I've now got a simproc that reduces this to id in ~20 seconds, but it still exhibits some funky non-determinism, which I think has to do with how the node-selection is being done. Progress!
You can try it yourself if you want. New rule goes in theorems/, new simproc goes anywhere in project (they don't care). You need to pull and rebuild the core to get the new simproc combinators.
-r
--
You received this message because you are subscribed to the Google Groups "Quantomatic" group.
To unsubscribe from this group and stop receiving emails from it, send an email to quantomatic+unsubscribe@googlegroups.com.
To post to this group, send email to quant...@googlegroups.com.
Visit this group at https://groups.google.com/group/quantomatic.
For more options, visit https://groups.google.com/d/optout.
Ross Duncan
Nov 4, 2016, 1:21:13 PM11/4/16
to quant...@googlegroups.com
Woop woop!
Unfortunately it looks like your project has different rules (or at least different names for rules) than the one I have. So the simproc doesn’t compile here.
I am in sync with zx-project from the github.
-r
On 4 Nov 2016, at 15:23, Aleks Kissinger <ale...@gmail.com> wrote:
> okay, I've now got a simproc that reduces this to id in ~20 seconds, but it still exhibits some funky non-determinism, which I think has to do with how the node-selection is being done. Progress!
>
> You can try it yourself if you want. New rule goes in theorems/, new simproc goes anywhere in project (they don't care). You need to pull and rebuild the core to get the new simproc combinators.
>
> On 4 November 2016 at 14:35, Ross Duncan <dr.ross...@gmail.com> wrote:
> Hi Aleks,
> Here’s 2 qgrpahs. First one is the one at the start of the mega long rotate_simp run, the second is the point where it gave up/fell over. It’s pretty easy to reduce the graph by hand from there using (bialg [inverse] ; basic_simp)*
>
> -r
>
> --
> You received this message because you are subscribed to the Google Groups "Quantomatic" group.
> To unsubscribe from this group and stop receiving emails from it, send an email to quantomatic...@googlegroups.com.
Unfortunately it looks like your project has different rules (or at least different names for rules) than the one I have. So the simproc doesn’t compile here.
I am in sync with zx-project from the github.
-r
On 4 Nov 2016, at 15:23, Aleks Kissinger <ale...@gmail.com> wrote:
> okay, I've now got a simproc that reduces this to id in ~20 seconds, but it still exhibits some funky non-determinism, which I think has to do with how the node-selection is being done. Progress!
>
> You can try it yourself if you want. New rule goes in theorems/, new simproc goes anywhere in project (they don't care). You need to pull and rebuild the core to get the new simproc combinators.
>
> On 4 November 2016 at 14:35, Ross Duncan <dr.ross...@gmail.com> wrote:
> Hi Aleks,
> Here’s 2 qgrpahs. First one is the one at the start of the mega long rotate_simp run, the second is the point where it gave up/fell over. It’s pretty easy to reduce the graph by hand from there using (bialg [inverse] ; basic_simp)*
>
> -r
>
> --
> You received this message because you are subscribed to the Google Groups "Quantomatic" group.
> To post to this group, send email to quant...@googlegroups.com.
> Visit this group at https://groups.google.com/group/quantomatic.
> For more options, visit https://groups.google.com/d/optout.
>
>
> On 4 Nov 2016, at 13:16, Aleks Kissinger <ale...@gmail.com> wrote:
>
> > Can you send me the qgraph file you are trying to reduce?
> >
> > On 4 November 2016 at 10:33, Aleks Kissinger <ale...@gmail.com> wrote:
> > Wow, 24 hours is some dedication. :)
> >
> > I know exactly why its so slow. There is currently no way to tell the matcher to start by matching vertex X in pattern to vertex Y in target then go from there. So, it just tries all matchings until it gets lucky and rewrites the correct thing. And it does this for *every* rotation step. Since the rotate rule has 3 bboxes and 3 nested bboxes, this finds a lot of matchings!
> >
> > This is very nearly fixable. Simprocs just need to be able to hook into the matcher appropriately. I'll try to have a look at this over the weekend.
> >
> > I think having a student to work on tactics is a good idea, since a lot can be done there. For instance, implementing Miriam's procedure for reducing cliffords to a quasi-normal form.
> >
> >
> >
> >
> > On 3 November 2016 at 13:29, Ross Duncan <dr.ross...@gmail.com> wrote:
> > Maybe this is not news to anyone, but rotate_simp has some performance issues. I’ve been running it on a graph with ~25 vertices, avg degree 4, for about 24 hours now and it has found only 3 rewrites!
> >
> > So I think the following could be a nice project for a student at some future point:
> > 1. An analysis of the runtime of rotate_simp — which necessarily will include how !-box matching works
> > 2. Produce a new tactic equivalent to rotate_simp with better performance
> > 3. A proof of the equivalence of the new tactic and the original rotate_simp.
> >
> > It’s probably a bit late in the calendar for this to happen this year, but something worth doing for next year.
> >
> > -r
> >
> > --
> > You received this message because you are subscribed to the Google Groups "Quantomatic" group.
> > To unsubscribe from this group and stop receiving emails from it, send an email to quantomatic...@googlegroups.com.
> Visit this group at https://groups.google.com/group/quantomatic.
> For more options, visit https://groups.google.com/d/optout.
>
>
> On 4 Nov 2016, at 13:16, Aleks Kissinger <ale...@gmail.com> wrote:
>
> > Can you send me the qgraph file you are trying to reduce?
> >
> > On 4 November 2016 at 10:33, Aleks Kissinger <ale...@gmail.com> wrote:
> > Wow, 24 hours is some dedication. :)
> >
> > I know exactly why its so slow. There is currently no way to tell the matcher to start by matching vertex X in pattern to vertex Y in target then go from there. So, it just tries all matchings until it gets lucky and rewrites the correct thing. And it does this for *every* rotation step. Since the rotate rule has 3 bboxes and 3 nested bboxes, this finds a lot of matchings!
> >
> > This is very nearly fixable. Simprocs just need to be able to hook into the matcher appropriately. I'll try to have a look at this over the weekend.
> >
> > I think having a student to work on tactics is a good idea, since a lot can be done there. For instance, implementing Miriam's procedure for reducing cliffords to a quasi-normal form.
> >
> >
> >
> >
> > On 3 November 2016 at 13:29, Ross Duncan <dr.ross...@gmail.com> wrote:
> > Maybe this is not news to anyone, but rotate_simp has some performance issues. I’ve been running it on a graph with ~25 vertices, avg degree 4, for about 24 hours now and it has found only 3 rewrites!
> >
> > So I think the following could be a nice project for a student at some future point:
> > 1. An analysis of the runtime of rotate_simp — which necessarily will include how !-box matching works
> > 2. Produce a new tactic equivalent to rotate_simp with better performance
> > 3. A proof of the equivalence of the new tactic and the original rotate_simp.
> >
> > It’s probably a bit late in the calendar for this to happen this year, but something worth doing for next year.
> >
> > -r
> >
> > --
> > You received this message because you are subscribed to the Google Groups "Quantomatic" group.
> > To post to this group, send email to quant...@googlegroups.com.
> > Visit this group at https://groups.google.com/group/quantomatic.
> > For more options, visit https://groups.google.com/d/optout.
> >
> >
> >
> > --
> > You received this message because you are subscribed to the Google Groups "Quantomatic" group.
> > To unsubscribe from this group and stop receiving emails from it, send an email to quantomatic...@googlegroups.com.
> > Visit this group at https://groups.google.com/group/quantomatic.
> > For more options, visit https://groups.google.com/d/optout.
> >
> >
> >
> > --
> > You received this message because you are subscribed to the Google Groups "Quantomatic" group.
> > To post to this group, send email to quant...@googlegroups.com.
> > Visit this group at https://groups.google.com/group/quantomatic.
> > For more options, visit https://groups.google.com/d/optout.
>
> --
> You received this message because you are subscribed to the Google Groups "Quantomatic" group.
> To unsubscribe from this group and stop receiving emails from it, send an email to quantomatic...@googlegroups.com.
> > Visit this group at https://groups.google.com/group/quantomatic.
> > For more options, visit https://groups.google.com/d/optout.
>
> --
> You received this message because you are subscribed to the Google Groups "Quantomatic" group.
> To post to this group, send email to quant...@googlegroups.com.
> Visit this group at https://groups.google.com/group/quantomatic.
> For more options, visit https://groups.google.com/d/optout.
>
>
>
> --
> You received this message because you are subscribed to the Google Groups "Quantomatic" group.
> To unsubscribe from this group and stop receiving emails from it, send an email to quantomatic...@googlegroups.com.
> Visit this group at https://groups.google.com/group/quantomatic.
> For more options, visit https://groups.google.com/d/optout.
>
>
>
> --
> You received this message because you are subscribed to the Google Groups "Quantomatic" group.
> To post to this group, send email to quant...@googlegroups.com.
> Visit this group at https://groups.google.com/group/quantomatic.
> For more options, visit https://groups.google.com/d/optout.
> <rotate-targeted.qrule><rotate_targeted.ML>
> Visit this group at https://groups.google.com/group/quantomatic.
> For more options, visit https://groups.google.com/d/optout.
Aleks Kissinger
Nov 5, 2016, 11:26:57 AM11/5/16
to quant...@googlegroups.com
I just incorporated into zx-project and pushed.
Also, after some optimisations in the matcher, this example now takes about 8 seconds. Generally you should find matching rules with multiple bang-boxes a bit zippier now.
On 4 November 2016 at 18:21, Ross Duncan <dr.ross...@gmail.com> wrote:
Woop woop!
Unfortunately it looks like your project has different rules (or at least different names for rules) than the one I have. So the simproc doesn’t compile here.
I am in sync with zx-project from the github.
-r
On 4 Nov 2016, at 15:23, Aleks Kissinger <ale...@gmail.com> wrote:
> okay, I've now got a simproc that reduces this to id in ~20 seconds, but it still exhibits some funky non-determinism, which I think has to do with how the node-selection is being done. Progress!
>
> You can try it yourself if you want. New rule goes in theorems/, new simproc goes anywhere in project (they don't care). You need to pull and rebuild the core to get the new simproc combinators.
>
> On 4 November 2016 at 14:35, Ross Duncan <dr.ross...@gmail.com> wrote:
> Hi Aleks,
> Here’s 2 qgrpahs. First one is the one at the start of the mega long rotate_simp run, the second is the point where it gave up/fell over. It’s pretty easy to reduce the graph by hand from there using (bialg [inverse] ; basic_simp)*
>
> -r
>
> --
> You received this message because you are subscribed to the Google Groups "Quantomatic" group.
> To unsubscribe from this group and stop receiving emails from it, send an email to quantomatic+unsubscribe@googlegroups.com.
> To post to this group, send email to quant...@googlegroups.com.
> Visit this group at https://groups.google.com/group/quantomatic.
> For more options, visit https://groups.google.com/d/optout.
>
>
> On 4 Nov 2016, at 13:16, Aleks Kissinger <ale...@gmail.com> wrote:
>
> > Can you send me the qgraph file you are trying to reduce?
> >
> > On 4 November 2016 at 10:33, Aleks Kissinger <ale...@gmail.com> wrote:
> > Wow, 24 hours is some dedication. :)
> >
> > I know exactly why its so slow. There is currently no way to tell the matcher to start by matching vertex X in pattern to vertex Y in target then go from there. So, it just tries all matchings until it gets lucky and rewrites the correct thing. And it does this for *every* rotation step. Since the rotate rule has 3 bboxes and 3 nested bboxes, this finds a lot of matchings!
> >
> > This is very nearly fixable. Simprocs just need to be able to hook into the matcher appropriately. I'll try to have a look at this over the weekend.
> >
> > I think having a student to work on tactics is a good idea, since a lot can be done there. For instance, implementing Miriam's procedure for reducing cliffords to a quasi-normal form.
> >
> >
> >
> >
> > On 3 November 2016 at 13:29, Ross Duncan <dr.ross...@gmail.com> wrote:
> > Maybe this is not news to anyone, but rotate_simp has some performance issues. I’ve been running it on a graph with ~25 vertices, avg degree 4, for about 24 hours now and it has found only 3 rewrites!
> >
> > So I think the following could be a nice project for a student at some future point:
> > 1. An analysis of the runtime of rotate_simp — which necessarily will include how !-box matching works
> > 2. Produce a new tactic equivalent to rotate_simp with better performance
> > 3. A proof of the equivalence of the new tactic and the original rotate_simp.
> >
> > It’s probably a bit late in the calendar for this to happen this year, but something worth doing for next year.
> >
> > -r
> >
> > --
> > You received this message because you are subscribed to the Google Groups "Quantomatic" group.
> > To unsubscribe from this group and stop receiving emails from it, send an email to quantomatic+unsubscribe@googlegroups.com.
> > To post to this group, send email to quant...@googlegroups.com.
> > Visit this group at https://groups.google.com/group/quantomatic.
> > For more options, visit https://groups.google.com/d/optout.
> >
> >
> >
> > --
> > You received this message because you are subscribed to the Google Groups "Quantomatic" group.
> > To unsubscribe from this group and stop receiving emails from it, send an email to quantomatic+unsubscribe@googlegroups.com.
> > To post to this group, send email to quant...@googlegroups.com.
> > Visit this group at https://groups.google.com/group/quantomatic.
> > For more options, visit https://groups.google.com/d/optout.
>
> --
> You received this message because you are subscribed to the Google Groups "Quantomatic" group.
> To unsubscribe from this group and stop receiving emails from it, send an email to quantomatic+unsubscribe@googlegroups.com.
> To post to this group, send email to quant...@googlegroups.com.
> Visit this group at https://groups.google.com/group/quantomatic.
> For more options, visit https://groups.google.com/d/optout.
>
>
>
> --
> You received this message because you are subscribed to the Google Groups "Quantomatic" group.
> To unsubscribe from this group and stop receiving emails from it, send an email to quantomatic+unsubscribe@googlegroups.com.
> To post to this group, send email to quant...@googlegroups.com.
> Visit this group at https://groups.google.com/group/quantomatic.
> For more options, visit https://groups.google.com/d/optout.
> <rotate-targeted.qrule><rotate_targeted.ML>
--
You received this message because you are subscribed to the Google Groups "Quantomatic" group.
To unsubscribe from this group and stop receiving emails from it, send an email to quantomatic+unsubscribe@googlegroups.com.
Ross Duncan
Nov 10, 2017, 8:46:59 AM11/10/17
to quant...@googlegroups.com
Hi all,
One feature that would be very good for Quantomatic would be to link a theorem to its proof, so that when a lemma is used in another development, it wouldn’t be necessary to take the lemma on trust — the lemma’s proof could be inserted into the larger development.
An approach that would integrate nicely with the idea of having an online repository of proofs is identifying each proof with a cryptographic hash. This would allow (in principle at least) the entire body of work done in quantomatic to be arranged into a blockchain-like structure.
Thoughts?
-r
One feature that would be very good for Quantomatic would be to link a theorem to its proof, so that when a lemma is used in another development, it wouldn’t be necessary to take the lemma on trust — the lemma’s proof could be inserted into the larger development.
An approach that would integrate nicely with the idea of having an online repository of proofs is identifying each proof with a cryptographic hash. This would allow (in principle at least) the entire body of work done in quantomatic to be arranged into a blockchain-like structure.
Thoughts?
-r
Lucas Dixon
Nov 10, 2017, 9:20:12 AM11/10/17
to quant...@googlegroups.com
Blockchained quantomatic....!
I guess I'd be inclined to not use hashes, but unique IDs of some sort. Hashes do sometimes collide at larger scale. At small scale, one can typically ignore that, but at larger scales (we have to dream big, right?) It does happen and can bite you. Of course the downside of unique ID's is that you need a service, or a good compression algorithm (where you use the lemma itself as it's Id, and hashes as just for a quicker lookup function). A web service, for all quantomatic theories and theorems would be a cool thing too.
Aleks Kissinger
Nov 12, 2017, 10:27:08 AM11/12/17
to quant...@googlegroups.com, zx-ca...@maillist.ox.ac.uk
ZX-calculus people: I'm adding you to this discussion, because we've
been talking about this as well.
It has been brought up several times that providing a consistent way
to store and access "ZX knowledge", namely axioms, theorems, and
formal proofs, would be very useful. I think blockchain (as mentioned
by Ross below) is overkill, but something that plays much the same
role as Isabelle's "Achive of Formal Proofs" (isa-afp.org) could be of
great benefit to the community.
What I imagine is a central repository, where people can submit
Quantomatic projects, which are subjected to an automated review
process then (possibly) manually reviewed by one of a small number of
moderators. Projects that are accepted are issued a unique ID and a
version number. Theorems and proofs in these projects can be viewed in
a web browser. This should be easy enough to navigate that it is
useful to non-experts as well. This unique ID can be cited in papers
or in other Quantomatic projects.
Standards for success:
1. simple, lightweight, and easy to maintain. After an initial setup
period, we can't depend on anyone having gobs of time to devote to
keeping things ticking over. However, realistically speaking:
maintenance and moderation will take some time, and these things
should have well-defined procedures and be taken seriously.
2. a useful, searchable, and (importantly) *permanent* repository for
ZX knowledge (and possibly other graphical calculi, but I think ZX
should be the focus)
3. the ability now, and always, to automatically check the correctness
of the repository contents. For example: theorems should only depend
on the axioms they say they do, and dependencies should be acyclic.
There are a lot of details of this to hammer out (scope, technical
issues, socialogical issues). Maybe it would be good to set aside a ZX
meeting for discussion?
Best,
Aleks
>> email to quantomatic...@googlegroups.com.
been talking about this as well.
It has been brought up several times that providing a consistent way
to store and access "ZX knowledge", namely axioms, theorems, and
formal proofs, would be very useful. I think blockchain (as mentioned
by Ross below) is overkill, but something that plays much the same
role as Isabelle's "Achive of Formal Proofs" (isa-afp.org) could be of
great benefit to the community.
What I imagine is a central repository, where people can submit
Quantomatic projects, which are subjected to an automated review
process then (possibly) manually reviewed by one of a small number of
moderators. Projects that are accepted are issued a unique ID and a
version number. Theorems and proofs in these projects can be viewed in
a web browser. This should be easy enough to navigate that it is
useful to non-experts as well. This unique ID can be cited in papers
or in other Quantomatic projects.
Standards for success:
1. simple, lightweight, and easy to maintain. After an initial setup
period, we can't depend on anyone having gobs of time to devote to
keeping things ticking over. However, realistically speaking:
maintenance and moderation will take some time, and these things
should have well-defined procedures and be taken seriously.
2. a useful, searchable, and (importantly) *permanent* repository for
ZX knowledge (and possibly other graphical calculi, but I think ZX
should be the focus)
3. the ability now, and always, to automatically check the correctness
of the repository contents. For example: theorems should only depend
on the axioms they say they do, and dependencies should be acyclic.
There are a lot of details of this to hammer out (scope, technical
issues, socialogical issues). Maybe it would be good to set aside a ZX
meeting for discussion?
Best,
Aleks
>> To post to this group, send email to quant...@googlegroups.com.
>> Visit this group at https://groups.google.com/group/quantomatic.
>> For more options, visit https://groups.google.com/d/optout.
>
>> Visit this group at https://groups.google.com/group/quantomatic.
>> For more options, visit https://groups.google.com/d/optout.
>
> --
> You received this message because you are subscribed to the Google Groups
> "Quantomatic" group.
> To unsubscribe from this group and stop receiving emails from it, send an
> email to quantomatic...@googlegroups.com.
> You received this message because you are subscribed to the Google Groups
> "Quantomatic" group.
> To unsubscribe from this group and stop receiving emails from it, send an
Reply all
Reply to author
Forward
0 new messages