Yes, perhaps. This is not written as a general introduction to e-graphs. They are a data structure that compactly holds many equivalent versions of terms / syntax trees. Egraphs are a solution to phase ordering issues for greedy rewrites. They are also just a useful fabric for optimization tasks. They are being used in many compiler projects
https://github.com/philzook58/awesome-egraphs . Mostly research compilers, but cranelift and luminal are not for example.
Many applications are naturally expressed using bound variables (lambdas, summation expressions, einstein indices, integrals, loops) but the basic e-graph doesn't really support the concept. One can instead model using combinators (SKI combinators, relation algebra, categorical combinators, other) but this tends to be not entirely natural and tends to explodes in the search space of different ways to encode the same concept using combinators.
Lifting e-graphs are a variant of sorts of slotted e-graphs, which are techniques to supports binders in egraphs. It's more subtle to do so than one might think. Lambda microegg also adds a surface syntax to play around more easily.
Many applications are naturally expressed using bound variables (lambdas, summation expressions, einstein indices, integrals, loops) but the basic e-graph doesn't really support the concept. One can instead model using combinators (SKI combinators, relation algebra, categorical combinators, other) but this tends to be not entirely natural and tends to explodes in the search space of different ways to encode the same concept using combinators.
Lifting e-graphs are a variant of sorts of slotted e-graphs, which are techniques to supports binders in egraphs. It's more subtle to do so than one might think. Lambda microegg also adds a surface syntax to play around more easily.