Quantomatic rewriting edges with data

[Konstantin Devyatov]

Hi Quantomatic team,

My name is Konstantin Devyatov. I'm a student at Heriot-Watt University working on my bachelor dissertation, supervised by Gudmund Grov. My project is mechanising Hume Box calculus by encoding it as Quantomatic theory. I've been using Quantomatic for over 9 months and the experience had been pleasant and inspiring. Thank you for that!

The reason I'm writing this is hope that you will help me understand my issue with Quantomatic rewriting edges with data. The issue: when applying a rule, lhs and rhs boundaries become different.

To test this out, I have created an identity rule, which matches any vertex with any two edges connecting it, and substitutes it with itself. The rule has lhs = rhs. LHS contains a vertex with data variables and two edges, also with data variables. Rewriting has no problem with vertices, just with edge substitution.

My edge substitution function is work exactly like my vertex substitution. The problem I'm suspecting, is when rewrite happens, only rhs edges is substituted, leaving lhs edges different with variable data. I have tested my code with manual matching and substitution of each edge one by one, which was successful.

Please spend 20 minutes of your time looking into this, I really believe you can help me out.

Link to carefully chosen snippets of code: http://pastebin.com/muc8fRTq

Link to the error message given by polyML: http://pastebin.com/QauXtNTD

Kind regards,

Kos

[Aleks Kissinger]

Just to see if I understand:

Is the LHS getting replaced with the RHS, but without performing any
substitutions on the free variables in the edges? I.e. not applying
the subst data correctly?

a

> --
> 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.
> To post to this group, send email to quant...@googlegroups.com.
> Visit this group at http://groups.google.com/group/quantomatic.
> For more options, visit https://groups.google.com/d/optout.

[Konstantin Devyatov]

Hi Aleks,

Thanks for your shift response.

LHS is replaced by RHS, which is not apparent in this example, since rhs = lhs.

The problem, in my opinion based on the error linked, that LHS is not substituted on the free variables, while RHS is.

Kind regards,

[Konstantin Devyatov]

Hi Aleks,

Sorry to be nagging, but my dissertation submission date is approaching.

Did you manage to reproduce the issue? Do you think this is Quantomatic issue? Would you like any more information?

Kind regards,

Kos

[Aleks Kissinger]

Okay, I'm starting to see what's going on. Is it the call to
Rewriter.rewrite_at the part that is throwing the exception? It would
be useful if you wrapped your code in PolyML.exception_trace (fn () =>
....) then uploaded the output again.

[Aleks Kissinger]

You're right. When the rewriter applies a rewrite, it first creates a
new instantiated rule to apply. However, it wasn't instantiating free
vars on the LHS. So, if there is a free var on a boundary edge, this
will crash. We never noticed because none of the existing theories in
quanto have free vars on edges.

Pull the latest integration on Quantomatic/quantomatic and see if that
fixes the problem.

[Konstantin Devyatov]

Hi Aleks,

Thanks for fixing this.

To test the change I've pulled the updated integration branch and tried to compile. Make clean both isalib and quantomatic/core.

The error I got on make quantomatic/core:

Error- in 'bang_graph.ML', line 1252.
Value or constructor (restrict_dom) has not been declared in structure VSub
Found near
  VSub.restrict_dom old_vertices (VSub.extend_fresh old_vertices vsub)
Error- in 'bang_graph.ML', line 1340.
Value or constructor (filter_dom) has not been declared in structure VSub
Found near VSub.filter_dom (V.NSet.contains (get_vertices_in_bbox g bb)) vrn'

Did you have any problems with it? Can you compile it fine. Any suggestions on this exception?

Much appreciate the time you spend helping me out!

[Aleks Kissinger]

You need to pull the latest isaplib from Quantomatic/isaplib.

[Konstantin Devyatov]

Thanks for pointing this silly mistake, Aleks.

The fix had worked, boundary edge rewriting is fully functional for my application.

Kind regards,

[Aleks Kissinger]

Great!