What do e-graphs and regexes have in common? More than you might think!
Check out the post I wrote with @altan0 on the egg discussion board: github.com/egraphs-good/e….
The key idea is that e-graphs are minimal DFTAs, but what does that mean? 🧵
Check out the post I wrote with @altan0 on the egg discussion board: github.com/egraphs-good/e….
The key idea is that e-graphs are minimal DFTAs, but what does that mean? 🧵
An e-graph is a data structure for efficiently storing lots of equivalent expressions, and that's really useful for all sorts of PL problems in compilers, optimization, and synthesis. Read @mwillsey's SIGPLAN post for more! blog.sigplan.org/2021/04/06/equ…
DFTAs come from theoretical computer science. A DFTA is a deterministic finite tree automaton. DFTAs work like their simpler cousins DFAs except that instead of recognizing words, DFTAs recognize trees. (Also they are really fun to draw! Here's one for simple boolean expressions)
Here's how a DFTA recognizes an expression. Starting from the leaves you bubble up DFTA states to the root using the rules in the hypergraph. (Thanks to @xwangsd for this example!) Many more details in the post!
If you stare at the DFTA hypergraph, you might notice that every label has exactly one red edge. We can simplify the drawing by "pushing" every label into its target state. And hey, that looks a lot like an e-graph...
Well almost. We haven't discussed congruence closure, which is important for e-graphs. Thanks to the Myhill-Nerode theorem, a *minimal* DFTA (i.e. one with a minimal number of states) respects congruence _exactly_ like an e-graph! states = e-classes, transitions = e-nodes. QED
Glossing over lots of details here so be sure to check out the post if you want to know more! github.com/egraphs-good/e…
• • •
Missing some Tweet in this thread? You can try to
force a refresh
