4 ms·

Better Together: Unifying Datalog and Equality Saturation

101 points by luu 4y ago

YeGoblynQueenne 4y ago
I always want to see more on HN about programming languages and logic programming, but I'd like some context here, on the notability of the work that is presented in the linked article. It sounds cool. What are the current applications, uses?
- sakras 4y ago
  UW’s PL group has been focusing lately on this notion of E-Graphs and a technique called Equality Saturation. An E-Graph is a structure that efficiently represents equivalent rewrites of a program (exponentially many rewrites in polynomial space iiuc). Equality saturation is the process of generating an e-graph that represents all possible rewrites by inserting rewrites until the e-graph doesn’t change (is saturated). After the graph is created, you can use some heuristic to pick a good rewrite. This paper applies E-graphs to augment Datalog's reasoning/constraint solving.
- hobofan 4y ago
  This is the advancement of egg[0]. Egg (and the e-graph theory behind it) has recently been put into use in some databases (e.g. cube[1]) and compilers (e.g. cranelift[2]). It lends itself well to the use-case of optimizing query planers and compilers, as it at the core avoids the optimization pass ordering problem (where an earlier optimization pass may destroy information that could be useful for a later one). [0]: https://github.com/egraphs-good/egg https://github.com/egraphs-good/egg [1]: https://github.com/cube-js/cube https://github.com/cube-js/cube [2]: https://github.com/bytecodealliance/rfcs/blob/main/accepted/cranelift-egraph.md https://github.com/bytecodealliance/rfcs/blob/main/accepted/...
  - philzook 4y ago
    A more direct link to a list of applications of egraphs is https://egraphs-good.github.io/ https://egraphs-good.github.io/ Largely optimizing rewrites in compilers/synthesizers/query optimizer and theorem proving applications. The egglog repo is here https://github.com/mwillsey/egg-smol https://github.com/mwillsey/egg-smol with a wasm compiled web demo with examples here https://www.mwillsey.com/egg-smol/ https://www.mwillsey.com/egg-smol/ It is still in pre-release, so there are no guarantees of stability and not necessarily ready for people to pile in. This system is related to ones Yihong Zhang and I gave separate talks on at last year EGRAPHS 2022 workshop https://effect.systems/doc/pldi-2022-egraphs/abstract.pdf https://effect.systems/doc/pldi-2022-egraphs/abstract.pdf http://www.philipzucker.com/egglog/ http://www.philipzucker.com/egglog/
    - YeGoblynQueenne 4y ago
      Thanks both for all the links!
    - thaliaarchi 4y ago
      How does egglog compare to bddbddb, a Datalog engine powered by BDDs? They use BDDs in Datalog to solve previously unsolved problems like context-sensitive pointer analysis for large programs and show that analyses implemented with it are faster than hand-tuned implementations and use dramatically fewer lines of code. https://people.csail.mit.edu/mcarbin/papers/aplas05.pdf https://people.csail.mit.edu/mcarbin/papers/aplas05.pdf
  - cfallin 4y ago
    A small correction re: Cranelift -- I had originally prototyped with egg, but we're currently using a variant of egraphs I invented called "acyclic egraphs" after working through performance and productionization issues, with our own implementation. Egg is great for what it is; a production compiler is just a really particular and demanding environment. I'll be giving a talk about it at EGRAPHS 2023 (in the meantime there are details in the RFC you linked). E-graphs are cool! :-)
  - felixyz 4y ago
    Related to equality-constrained tree automata[1], which (as far as I understand) can "pick" an implementation/realization out of a huge latent space of possibilities. [1]: https://www.jameskoppel.com/publication/ecta/ https://www.jameskoppel.com/publication/ecta/
crazyedgar 4y ago
I believe this is the code for their work, which I believe the authors didn't put in the paper: https://github.com/philzook58/egglog https://github.com/philzook58/egglog
- aseipp 4y ago
  Close, but the link is on Page 13, and it points here: https://github.com/mwillsey/egg-smol https://github.com/mwillsey/egg-smol Unfortunately the naming is all a bit confusing, isn't it....
- philzook 4y ago
  That is a previous defunct prototype wildly superseded by the current implementation. I still have a soft spot for the syntax though
hinoki 4y ago
The same people had the presentation at POPL that’s a good introduction to equality saturation. https://youtu.be/6cJMI9z2TeU https://youtu.be/6cJMI9z2TeU
deleted 4y ago
[deleted]
bottom999mottob 4y ago
This looks very intriguing! Couldn't you use this for stuff like graph convolution networks or even optimizing TypeScript live reloading? I'm just trying to think of potential applications. This sounds cool!
- ar-nelson 4y ago
  I'm just imagining a type system based on this. I've had ideas about a Datalog-based type system before, but it was never really practical; this could be the breakthrough that would make it practical!
  - philzook 4y ago
    You might find these also interesting - Higher-Order, Data-Parallel Structured Deduction https://arxiv.org/pdf/2211.11573.pdf https://arxiv.org/pdf/2211.11573.pdf - Functional Programming with Datalog https://drops.dagstuhl.de/opus/volltexte/2022/16235/pdf/LIPIcs-ECOOP-2022-7.pdf https://drops.dagstuhl.de/opus/volltexte/2022/16235/pdf/LIPI... - A Systematic Approach to Deriving Incremental Type Checkers https://www.pl.informatik.uni-mainz.de/files/2020/10/incremental-typing-foundations.pdf https://www.pl.informatik.uni-mainz.de/files/2020/10/increme...

101 points by luu 4y ago

I always want to see more on HN about programming languages and logic programming, but I'd like some context here, on the notability of the work that is presented in the linked article. It sounds cool. What are the current applications, uses?

sakras 4y ago
UW’s PL group has been focusing lately on this notion of E-Graphs and a technique called Equality Saturation. An E-Graph is a structure that efficiently represents equivalent rewrites of a program (exponentially many rewrites in polynomial space iiuc). Equality saturation is the process of generating an e-graph that represents all possible rewrites by inserting rewrites until the e-graph doesn’t change (is saturated). After the graph is created, you can use some heuristic to pick a good rewrite. This paper applies E-graphs to augment Datalog's reasoning/constraint solving.
hobofan 4y ago
This is the advancement of egg[0]. Egg (and the e-graph theory behind it) has recently been put into use in some databases (e.g. cube[1]) and compilers (e.g. cranelift[2]). It lends itself well to the use-case of optimizing query planers and compilers, as it at the core avoids the optimization pass ordering problem (where an earlier optimization pass may destroy information that could be useful for a later one). [0]: https://github.com/egraphs-good/egg https://github.com/egraphs-good/egg [1]: https://github.com/cube-js/cube https://github.com/cube-js/cube [2]: https://github.com/bytecodealliance/rfcs/blob/main/accepted/cranelift-egraph.md https://github.com/bytecodealliance/rfcs/blob/main/accepted/...
- philzook 4y ago
  A more direct link to a list of applications of egraphs is https://egraphs-good.github.io/ https://egraphs-good.github.io/ Largely optimizing rewrites in compilers/synthesizers/query optimizer and theorem proving applications. The egglog repo is here https://github.com/mwillsey/egg-smol https://github.com/mwillsey/egg-smol with a wasm compiled web demo with examples here https://www.mwillsey.com/egg-smol/ https://www.mwillsey.com/egg-smol/ It is still in pre-release, so there are no guarantees of stability and not necessarily ready for people to pile in. This system is related to ones Yihong Zhang and I gave separate talks on at last year EGRAPHS 2022 workshop https://effect.systems/doc/pldi-2022-egraphs/abstract.pdf https://effect.systems/doc/pldi-2022-egraphs/abstract.pdf http://www.philipzucker.com/egglog/ http://www.philipzucker.com/egglog/
  - YeGoblynQueenne 4y ago
    Thanks both for all the links!
  - thaliaarchi 4y ago
    How does egglog compare to bddbddb, a Datalog engine powered by BDDs? They use BDDs in Datalog to solve previously unsolved problems like context-sensitive pointer analysis for large programs and show that analyses implemented with it are faster than hand-tuned implementations and use dramatically fewer lines of code. https://people.csail.mit.edu/mcarbin/papers/aplas05.pdf https://people.csail.mit.edu/mcarbin/papers/aplas05.pdf
- cfallin 4y ago
  A small correction re: Cranelift -- I had originally prototyped with egg, but we're currently using a variant of egraphs I invented called "acyclic egraphs" after working through performance and productionization issues, with our own implementation. Egg is great for what it is; a production compiler is just a really particular and demanding environment. I'll be giving a talk about it at EGRAPHS 2023 (in the meantime there are details in the RFC you linked). E-graphs are cool! :-)
- felixyz 4y ago
  Related to equality-constrained tree automata[1], which (as far as I understand) can "pick" an implementation/realization out of a huge latent space of possibilities. [1]: https://www.jameskoppel.com/publication/ecta/ https://www.jameskoppel.com/publication/ecta/

crazyedgar 4y ago

I believe this is the code for their work, which I believe the authors didn't put in the paper: https://github.com/philzook58/egglog https://github.com/philzook58/egglog

aseipp 4y ago
Close, but the link is on Page 13, and it points here: https://github.com/mwillsey/egg-smol https://github.com/mwillsey/egg-smol Unfortunately the naming is all a bit confusing, isn't it....
philzook 4y ago
That is a previous defunct prototype wildly superseded by the current implementation. I still have a soft spot for the syntax though

hinoki 4y ago

The same people had the presentation at POPL that’s a good introduction to equality saturation. https://youtu.be/6cJMI9z2TeU https://youtu.be/6cJMI9z2TeU

deleted 4y ago

[deleted]

bottom999mottob 4y ago

This looks very intriguing! Couldn't you use this for stuff like graph convolution networks or even optimizing TypeScript live reloading? I'm just trying to think of potential applications. This sounds cool!

ar-nelson 4y ago
I'm just imagining a type system based on this. I've had ideas about a Datalog-based type system before, but it was never really practical; this could be the breakthrough that would make it practical!
- philzook 4y ago
  You might find these also interesting - Higher-Order, Data-Parallel Structured Deduction https://arxiv.org/pdf/2211.11573.pdf https://arxiv.org/pdf/2211.11573.pdf - Functional Programming with Datalog https://drops.dagstuhl.de/opus/volltexte/2022/16235/pdf/LIPIcs-ECOOP-2022-7.pdf https://drops.dagstuhl.de/opus/volltexte/2022/16235/pdf/LIPI... - A Systematic Approach to Deriving Incremental Type Checkers https://www.pl.informatik.uni-mainz.de/files/2020/10/incremental-typing-foundations.pdf https://www.pl.informatik.uni-mainz.de/files/2020/10/increme...