4 ms·

Formulog: ML + Datalog + SMT

129 points by matt_d 6y ago

siraben 6y ago
There's a reason why a lot of programming language papers use formal math notation, because it's a lot more concise to express the entire typing rules of your language in a dozen or so inference rules rather than a more convoluted implementation.[0] Formulog looks like it could potentially replace that math notation for something as rigorous yet executable. On the other hand, denotational semantics are usually straightforward enough to be implemented by reading off the math. As an example, it was quite easy for me to translate Scheme's semantics to code.[1] I hope it gets reimplemented in a functional language as well, Formulog's current implementation is in Java[2] which might not be ideal for reducing implementation bugs. [0] Contrast the code and math: https://www.andres-loeh.de/LambdaPi/LambdaPi.pdf https://www.andres-loeh.de/LambdaPi/LambdaPi.pdf [1] https://github.com/siraben/r5rs-denot https://github.com/siraben/r5rs-denot [2] https://github.com/HarvardPL/formulog https://github.com/HarvardPL/formulog
- benrbray 6y ago
  Any advice for learning to read the PL math notation? The PL papers I've seen normally take it for granted, so I don't even know what it's called to search for it! EDIT: Thank you all for the references :)
  - siraben 6y ago
    If you're talking about the inference rules used to specify the type system of a programming language, one of Wikipedia's[0] references is[1] which from a quick skim seems adequate. The main takeaway is that the things above the line are the assumptions, and the things below the line is what you conclude. Γ is usually used for typing environments (a map from variables to their types), the turnstile ⊢ can be read as "from the context on the left, it entails the typing information on the right". As a quick example: Γ ⊢ e1 : Int Γ ⊢ e2 : Int ---------------------------- Γ ⊢ e1 + e2 : Int Which reads, if e1 has type Int in Γ, and e2 has type Int in Γ, then e1 + e2 also has type Int in Γ. These rules are really bidirectional which is what allows you to perform typechecking. If you have an expression (a + b) of type Int, you can reduce it into two subproblems, typechecking a expecting an Int, and similarly for b. [0] https://en.wikipedia.org/wiki/Type_rule https://en.wikipedia.org/wiki/Type_rule [1] https://www.cs.colorado.edu/~bec/courses/csci5535/reading/cardelli-typesystems.pdf https://www.cs.colorado.edu/~bec/courses/csci5535/reading/ca...
    - mgreenbe 6y ago
      See also: http://siek.blogspot.com/2012/07/crash-course-on-notation-in-programming.html http://siek.blogspot.com/2012/07/crash-course-on-notation-in...
      - chubot 6y ago
        (Nice to see your work shared here :) ) I went through the corresponding videos last year: https://www.youtube.com/watch?v=vU3caZPtT2I https://www.youtube.com/watch?v=vU3caZPtT2I https://www.youtube.com/watch?v=MhuK_aepu1Y https://www.youtube.com/watch?v=MhuK_aepu1Y It was a great refresher as someone who once liked math but hasn't done much of it in ~20 years :) I had seen the blog posts, but there was some "color" in the videos that helped. For example I didn't realize that the fonts sometimes matter! Honestly, I still don't really read the notation, as I haven't had a strong reason to, but I feel it would be useful at some point. ---- For others, I also recommend this 2017 talk by Guy Steele It's Time for a New Old Language https://www.youtube.com/watch?v=7HKbjYqqPPQ https://www.youtube.com/watch?v=7HKbjYqqPPQ Because even people in the field seem to have problems with the notation. He also was asked about this work a few days ago here and said he was still working on it in the background (being a "completionist"): https://www.youtube.com/watch?v=c_ZJECVlpog https://www.youtube.com/watch?v=c_ZJECVlpog ----- FWIW as you know, Oil is more static than shell, and that was largely motivated by tools and static analysis (and negatively motivated by false positives in ShellCheck https://news.ycombinator.com/item?id=22213155 https://news.ycombinator.com/item?id=22213155) I would like to go further in that direction, but getting the basic functionality and performance up to par has taken up essentially 100% of the time so far :-( My use of Zephyr ASDL was also partly motivated by some vague desire to get the AST into OCaml. However I haven't used OCaml in quite awhile and I get hung up on small things like writing a serializer and deserializer. I don't want to do it for every type/schema, so it requires some kind of reflection. And my understanding is that there are a bunch of packages that do this like sexplib, but I never got further than that. Formulog sounds very nice, so I wonder if there is some recommended way of bridging the gap? For example imagine you want to load enormous Clang AST or TypeScript ASTs into Formulog. The parsers alone are 10K-30K lines of code, i.e. it's essentially infeasible to reproduce those parsers in another language in a reasonable time. And even just duplicating the schema is a pretty big engineering issue, since there are so many node types! I could generate them from Zephyr ASDL, but other projects can't. I wonder if you have any thoughts on that? i.e. to make the work more accessible on codebases "in the wild" ----- Also FWIW I mentioned this "microgrammars" work a few days ago because I'm always looking for ways to make things less work in practice :) https://news.ycombinator.com/item?id=23978432 https://news.ycombinator.com/item?id=23978432 Doing anything with languages seems to be very "long winded" so I'm glad to see work in that direction!
  - matt_d 6y ago
    I can recommend the references listed in "Background: Notation" section of Program Analysis Resources: https://gist.github.com/MattPD/00573ee14bf85ccac6bed3c0678ddbef#background-notation https://gist.github.com/MattPD/00573ee14bf85ccac6bed3c0678dd...
  - gmfawcett 6y ago
    Also try searching for "sequent calculus" or "Gentzen proof calculus" which describe the underlying logical framework. You might enjoy this tutorial: http://logitext.mit.edu/logitext.fcgi/tutorial http://logitext.mit.edu/logitext.fcgi/tutorial
    - guerrilla 6y ago
      Dag Prawitz's book "Natural Deduction" isn't too hard to read .
  - remexre 6y ago
    And if you're fine with something much longer than others have suggested, Types And Programming Languages [0] covers the notation, in addition to most of the other knowledge most PL papers take for granted. [0]: https://www.cis.upenn.edu/~bcpierce/tapl/ https://www.cis.upenn.edu/~bcpierce/tapl/
Ericson2314 6y ago
It is also integesting to see how typeclasses/traits and OCaml's (still upcoming?) "modular implicits" are related to logic programming. I commend the rustc team for taking this lineage seriously in developing Chalk[1] and using differential-dataflow for the next borrow checker. If they combine those into a differential-dataflow-powered Chalk it will be very formidable! We'll have to catch up Haskell at some point, sigh. [1]: https://github.com/rust-lang/chalk.git https://github.com/rust-lang/chalk.git [2]: https://github.com/TimelyDataflow/differential-dataflow https://github.com/TimelyDataflow/differential-dataflow
carterschonwald 6y ago
A really cool prject in that space is/was datafun. http://www.rntz.net/datafun/ http://www.rntz.net/datafun/ Roughly: the way facts work in Datalog and similar stuff have pretty strong monotonicity properties. So if you want to allow adding more predicates and computations to the system, you kinda wanna only allow monotonic functions! This has some pretty interesting surprises when it comes to how to model things like true or false!
- mgreenbe 6y ago
  Datafun is quite cool! Formulog and Datafun seem similar---both combine logic programming and pure functional programming---but they take wildly different approaches. Datafun is a foundational re-imagining of what a Datalog could look like: start with a higher-order programming language and give it a first-class notion of least fixed points. A type system for tracking monotonicity lets you roll your own Datalog. It's impressive that you can reconstruct semi-naive evaluation (morally: in each 'round' of evaluation, only apply rules matching new results) in their setting (https://dl.acm.org/doi/abs/10.1145/3371090 https://dl.acm.org/doi/abs/10.1145/3371090). Datafun is still a ways away from the performance and implementation maturity of existing Datalogs, though. Formulog's approach is to try to let Datalog be Datalog as much as possible. We end up with restrictions around higher-order functions and other FP features in order to keep things simple on the Datalog side---quite the opposite of Datafun's fancy type system. Our Formulog interpreter does pretty well with internment, parallel execution, and magic sets, but you could easily port our design to existing Datalog compilers and get even bigger speedups. It's not clear how to do that for Datafun... yet. (I suspect you could port our SMT interface to Datafun without too much of a problem, too.)
fovc 6y ago
I would have thought the SMT queries would be the most time-consuming part of this, but the authors make a big deal of leveraging Datalog optimzations to drive performance. Especially given they purposefully don't re-use the SMT context across SMT terms. Aren't the big SMT solvers already doing a bunch of optimization to allow incremental (push/pop) queries to be fast?
- mgreenbe 6y ago
  We do use incremental solving. check-sat-assuming is generally better than push/pop, though, because Datalog's bottom-up search isn't DFS. If you're interested, check out our ICLP 2020 extended abstract: https://cs.pomona.edu/~michael/papers/iclp2020_extabs.pdf https://cs.pomona.edu/~michael/papers/iclp2020_extabs.pdf. We should have more on this in not too long.
  - fovc 6y ago
    Super interesting, and cool technique. Do you have any insight into why CSA outperforms PP so often? I would have assumed the solvers were tuned for PP
    - mgreenbe 6y ago
      I think the solvers _are_ tuned for PP. But we're comparing CSA and PP on the queries that Formulog issues... which don't really match well with the DFS discipline that the PP stack aligns with. I think CSA beats PP in our experiments because CSA is more flexible about locality. Broadly---and I haven't looked at the memory usage to confirm this---I think CSA trades space (cache more old formulae, not just the prefix of some stack) for time (look, our answers are in the cache!).
mncharity 6y ago
Poplog was a 1980's integration of a Prolog, Common Lisp, C-like POP-11, and SML. Regrettably, it's academic authors had commercial dreams, which seemingly neutered the transformative impact I thought it might then have had.
mncharity 6y ago
Just to make it obvious: Paper is https://cs.pomona.edu/~michael/papers/formulog_sub2020.pdf https://cs.pomona.edu/~michael/papers/formulog_sub2020.pdf ; code is https://github.com/HarvardPL/formulog https://github.com/HarvardPL/formulog .

129 points by matt_d 6y ago

There's a reason why a lot of programming language papers use formal math notation, because it's a lot more concise to express the entire typing rules of your language in a dozen or so inference rules rather than a more convoluted implementation.[0] Formulog looks like it could potentially replace that math notation for something as rigorous yet executable. On the other hand, denotational semantics are usually straightforward enough to be implemented by reading off the math. As an example, it was quite easy for me to translate Scheme's semantics to code.[1] I hope it gets reimplemented in a functional language as well, Formulog's current implementation is in Java[2] which might not be ideal for reducing implementation bugs. [0] Contrast the code and math: https://www.andres-loeh.de/LambdaPi/LambdaPi.pdf https://www.andres-loeh.de/LambdaPi/LambdaPi.pdf [1] https://github.com/siraben/r5rs-denot https://github.com/siraben/r5rs-denot [2] https://github.com/HarvardPL/formulog https://github.com/HarvardPL/formulog

benrbray 6y ago
Any advice for learning to read the PL math notation? The PL papers I've seen normally take it for granted, so I don't even know what it's called to search for it! EDIT: Thank you all for the references :)
- siraben 6y ago
  If you're talking about the inference rules used to specify the type system of a programming language, one of Wikipedia's[0] references is[1] which from a quick skim seems adequate. The main takeaway is that the things above the line are the assumptions, and the things below the line is what you conclude. Γ is usually used for typing environments (a map from variables to their types), the turnstile ⊢ can be read as "from the context on the left, it entails the typing information on the right". As a quick example: Γ ⊢ e1 : Int Γ ⊢ e2 : Int ---------------------------- Γ ⊢ e1 + e2 : Int Which reads, if e1 has type Int in Γ, and e2 has type Int in Γ, then e1 + e2 also has type Int in Γ. These rules are really bidirectional which is what allows you to perform typechecking. If you have an expression (a + b) of type Int, you can reduce it into two subproblems, typechecking a expecting an Int, and similarly for b. [0] https://en.wikipedia.org/wiki/Type_rule https://en.wikipedia.org/wiki/Type_rule [1] https://www.cs.colorado.edu/~bec/courses/csci5535/reading/cardelli-typesystems.pdf https://www.cs.colorado.edu/~bec/courses/csci5535/reading/ca...
  - mgreenbe 6y ago
    See also: http://siek.blogspot.com/2012/07/crash-course-on-notation-in-programming.html http://siek.blogspot.com/2012/07/crash-course-on-notation-in...
    - chubot 6y ago
      (Nice to see your work shared here :) ) I went through the corresponding videos last year: https://www.youtube.com/watch?v=vU3caZPtT2I https://www.youtube.com/watch?v=vU3caZPtT2I https://www.youtube.com/watch?v=MhuK_aepu1Y https://www.youtube.com/watch?v=MhuK_aepu1Y It was a great refresher as someone who once liked math but hasn't done much of it in ~20 years :) I had seen the blog posts, but there was some "color" in the videos that helped. For example I didn't realize that the fonts sometimes matter! Honestly, I still don't really read the notation, as I haven't had a strong reason to, but I feel it would be useful at some point. ---- For others, I also recommend this 2017 talk by Guy Steele It's Time for a New Old Language https://www.youtube.com/watch?v=7HKbjYqqPPQ https://www.youtube.com/watch?v=7HKbjYqqPPQ Because even people in the field seem to have problems with the notation. He also was asked about this work a few days ago here and said he was still working on it in the background (being a "completionist"): https://www.youtube.com/watch?v=c_ZJECVlpog https://www.youtube.com/watch?v=c_ZJECVlpog ----- FWIW as you know, Oil is more static than shell, and that was largely motivated by tools and static analysis (and negatively motivated by false positives in ShellCheck https://news.ycombinator.com/item?id=22213155 https://news.ycombinator.com/item?id=22213155) I would like to go further in that direction, but getting the basic functionality and performance up to par has taken up essentially 100% of the time so far :-( My use of Zephyr ASDL was also partly motivated by some vague desire to get the AST into OCaml. However I haven't used OCaml in quite awhile and I get hung up on small things like writing a serializer and deserializer. I don't want to do it for every type/schema, so it requires some kind of reflection. And my understanding is that there are a bunch of packages that do this like sexplib, but I never got further than that. Formulog sounds very nice, so I wonder if there is some recommended way of bridging the gap? For example imagine you want to load enormous Clang AST or TypeScript ASTs into Formulog. The parsers alone are 10K-30K lines of code, i.e. it's essentially infeasible to reproduce those parsers in another language in a reasonable time. And even just duplicating the schema is a pretty big engineering issue, since there are so many node types! I could generate them from Zephyr ASDL, but other projects can't. I wonder if you have any thoughts on that? i.e. to make the work more accessible on codebases "in the wild" ----- Also FWIW I mentioned this "microgrammars" work a few days ago because I'm always looking for ways to make things less work in practice :) https://news.ycombinator.com/item?id=23978432 https://news.ycombinator.com/item?id=23978432 Doing anything with languages seems to be very "long winded" so I'm glad to see work in that direction!
- matt_d 6y ago
  I can recommend the references listed in "Background: Notation" section of Program Analysis Resources: https://gist.github.com/MattPD/00573ee14bf85ccac6bed3c0678ddbef#background-notation https://gist.github.com/MattPD/00573ee14bf85ccac6bed3c0678dd...
- gmfawcett 6y ago
  Also try searching for "sequent calculus" or "Gentzen proof calculus" which describe the underlying logical framework. You might enjoy this tutorial: http://logitext.mit.edu/logitext.fcgi/tutorial http://logitext.mit.edu/logitext.fcgi/tutorial
  - guerrilla 6y ago
    Dag Prawitz's book "Natural Deduction" isn't too hard to read .
- remexre 6y ago
  And if you're fine with something much longer than others have suggested, Types And Programming Languages [0] covers the notation, in addition to most of the other knowledge most PL papers take for granted. [0]: https://www.cis.upenn.edu/~bcpierce/tapl/ https://www.cis.upenn.edu/~bcpierce/tapl/

Ericson2314 6y ago

It is also integesting to see how typeclasses/traits and OCaml's (still upcoming?) "modular implicits" are related to logic programming. I commend the rustc team for taking this lineage seriously in developing Chalk[1] and using differential-dataflow for the next borrow checker. If they combine those into a differential-dataflow-powered Chalk it will be very formidable! We'll have to catch up Haskell at some point, sigh. [1]: https://github.com/rust-lang/chalk.git https://github.com/rust-lang/chalk.git [2]: https://github.com/TimelyDataflow/differential-dataflow https://github.com/TimelyDataflow/differential-dataflow

carterschonwald 6y ago

A really cool prject in that space is/was datafun. http://www.rntz.net/datafun/ http://www.rntz.net/datafun/ Roughly: the way facts work in Datalog and similar stuff have pretty strong monotonicity properties. So if you want to allow adding more predicates and computations to the system, you kinda wanna only allow monotonic functions! This has some pretty interesting surprises when it comes to how to model things like true or false!

mgreenbe 6y ago
Datafun is quite cool! Formulog and Datafun seem similar---both combine logic programming and pure functional programming---but they take wildly different approaches. Datafun is a foundational re-imagining of what a Datalog could look like: start with a higher-order programming language and give it a first-class notion of least fixed points. A type system for tracking monotonicity lets you roll your own Datalog. It's impressive that you can reconstruct semi-naive evaluation (morally: in each 'round' of evaluation, only apply rules matching new results) in their setting (https://dl.acm.org/doi/abs/10.1145/3371090 https://dl.acm.org/doi/abs/10.1145/3371090). Datafun is still a ways away from the performance and implementation maturity of existing Datalogs, though. Formulog's approach is to try to let Datalog be Datalog as much as possible. We end up with restrictions around higher-order functions and other FP features in order to keep things simple on the Datalog side---quite the opposite of Datafun's fancy type system. Our Formulog interpreter does pretty well with internment, parallel execution, and magic sets, but you could easily port our design to existing Datalog compilers and get even bigger speedups. It's not clear how to do that for Datafun... yet. (I suspect you could port our SMT interface to Datafun without too much of a problem, too.)

fovc 6y ago

I would have thought the SMT queries would be the most time-consuming part of this, but the authors make a big deal of leveraging Datalog optimzations to drive performance. Especially given they purposefully don't re-use the SMT context across SMT terms. Aren't the big SMT solvers already doing a bunch of optimization to allow incremental (push/pop) queries to be fast?

mgreenbe 6y ago
We do use incremental solving. check-sat-assuming is generally better than push/pop, though, because Datalog's bottom-up search isn't DFS. If you're interested, check out our ICLP 2020 extended abstract: https://cs.pomona.edu/~michael/papers/iclp2020_extabs.pdf https://cs.pomona.edu/~michael/papers/iclp2020_extabs.pdf. We should have more on this in not too long.
- fovc 6y ago
  Super interesting, and cool technique. Do you have any insight into why CSA outperforms PP so often? I would have assumed the solvers were tuned for PP
  - mgreenbe 6y ago
    I think the solvers _are_ tuned for PP. But we're comparing CSA and PP on the queries that Formulog issues... which don't really match well with the DFS discipline that the PP stack aligns with. I think CSA beats PP in our experiments because CSA is more flexible about locality. Broadly---and I haven't looked at the memory usage to confirm this---I think CSA trades space (cache more old formulae, not just the prefix of some stack) for time (look, our answers are in the cache!).

mncharity 6y ago

Poplog was a 1980's integration of a Prolog, Common Lisp, C-like POP-11, and SML. Regrettably, it's academic authors had commercial dreams, which seemingly neutered the transformative impact I thought it might then have had.

mncharity 6y ago

Just to make it obvious: Paper is https://cs.pomona.edu/~michael/papers/formulog_sub2020.pdf https://cs.pomona.edu/~michael/papers/formulog_sub2020.pdf ; code is https://github.com/HarvardPL/formulog https://github.com/HarvardPL/formulog .