Egg: E-Graphs Good

If, like me, you have never heard of e-graphs, this takes you straight to an introduction:<p><a href="https:&#x2F;&#x2F;docs.rs&#x2F;egg&#x2F;0.6.0&#x2F;egg&#x2F;tutorials&#x2F;_01_background&#x2F;index.html" rel="nofollow">https:&#x2F;&#x2F;docs.rs&#x2F;egg&#x2F;0.6.0&#x2F;egg&#x2F;tutorials&#x2F;_01_background&#x2F;index...</a>

Glad to see this getting play on here. Egg presents a very compelling algorithm and library for equational reasoning over syntax trees that I&#x27;ve been pretty fascinated with over the past couple months.<p>These e-graph data structures are in the heart of SMT solvers but giving easier access to end users and specializing the algorithm to the different needs of optimizing rewrites really changes the game.<p>There&#x27;s some cool applications linked on the site that I recommend people check out. A kind of neat thing about it being in rust is that you can compile to WASM to throw stuff on the web. I had a little demo of using egg to rewrite some category theory on my blog here <a href="https:&#x2F;&#x2F;www.philipzucker.com&#x2F;rust-category&#x2F;" rel="nofollow">https:&#x2F;&#x2F;www.philipzucker.com&#x2F;rust-category&#x2F;</a>

So theory is not my strongest suit, maybe someone can clarify some things for me here. It seems like these equalities that we&#x27;re looking for are things like the identity laws, but also extended by mathematical operations like bitshift being faster than division by 2.<p>Do these equalities carry all the way into general programming, to the point where we could for example say a short loop is equivalent to an unrolled loop, and thus suggest that optimization? Would we have to come up with an exhaustive list of equivalences, or is the list actually short and well known like they are in logic (Identity Laws)?<p>Will we at some point basically plug Egg into LLVM and have it find new optimization passes?

I love this paper. Beyond including an interesting contribution, they give a fantastic introduction to the underlying ideas and algorithm that forms the background. Even if you only have time for the first few pages, it&#x27;s a worthwhile read.

ooh this is serendipitous, I&#x27;m going to need to do some deep research into term rewriting soon.<p>mentally, I&#x27;m modelling term rewriting as a state space search where each edge transition is a single possible rewrite. As always with state space search, the goal is to find the global optimum.<p>It&#x27;s funny how many problems come back to search heuristics.