search

rogerburtonpatel / vml

Code and proofs for Verse-ML, an equation-style sub-ml language. Part of an undergraduate senior thesis with Norman Ramsey, Milod Kazerounian, and Roger Burtonpatel.
5 stars 0 forks source link

A *formal* attempt at "like pattern matching" #7

Closed nrnrnr closed 8 months ago

nrnrnr commented 8 months ago

Pick something that might mean "like pattern matching" and try to formalize it. Issue #4 is an option but not the only option.

rogerburtonpatel commented 8 months ago

I think "like pattern matching" means you can compile it to a decision tree.

Writing this here so I don't forget, and so you see it.

nrnrnr commented 8 months ago

I suspect this property will be difficult to formalize in a useful way. But I will look forward to seeing what you have by Thursday.

rogerburtonpatel commented 8 months ago

https://github.com/rogerburtonpatel/vml/commit/e8967e5cfaa717ebfeba926f677adbe76c1c50a7

nrnrnr commented 8 months ago

FYI, github is rendering the $\;$ as a semicolon: https://github.com/rogerburtonpatel/vml/blob/main/like-pattern-matching.md

Other comments:

rogerburtonpatel commented 8 months ago

FYI, github is rendering the ; as a semicolon: https://github.com/rogerburtonpatel/vml/blob/main/like-pattern-matching.md

Gosh darn it. Missed this. Just want my latex \; spaces. Thanks for the heads-up.

Other comments:

* I'm not seeing the cycle among x,y,z.  I'm seeing "x depends on y; x depends on z".  But those equations aren't `let` bindings.  What are you seeing for dependencies?

I see a logical variable $x$ that depend on tuples containing logical variables $y, z$. Those variables, in turn, don't depend on external values. They're only related to $x$. I agree that I need to formalize this idea. Does what I'm getting at- that logical variables that depend only on logical variables with no overall scrutinee is what creates logical-variables-at-runtime scenarios? 

* According to Figure 1 in the Verse paper, a logical variable can be a value.  So your `value_bound_var` doesn't create the restriction you are hoping for.

Yep. I'll fix this. 

* The draft is still from formal.  And I don't yet grasp the idea well enough to be confident that it is ready to formalize.  In particular, I worry that "dependency graph" is a complex concept.  Perhaps there is a simpler piece of spaghetti to pull on?

I agree. I'll think on this more. Thank you for your sincerity.

rogerburtonpatel commented 8 months ago

Revising tomorrow with translations.