hegg

One can have obvious but repetitive optimizations with symbolic programming [1]. [1] https://arxiv.org/abs/1012.1802 Strange that AlphaEvolve authors do not compare their work to what is achievable by equality saturation. An implementation of equality saturation can take interesting integrals with very simple rules [2]. [2] https://github.com/alt-romes/hegg/blob/master/test/Sym.hs#L3...

Great to see this! Funnily, I was just now working on a problem to which I'm trying to apply e-graphs (using my -- shameless plug -- haskell e-graphs/eqsat library[1]) [1] https://github.com/alt-romes/hegg

Equality graphs (e-graphs) for theorem proving and equality saturation and other equality-related things. They're awesome data structures that efficiently maintain a congruence relation over many expressions > At a high level, e-graphs extend union-find to compactly represent equivalence classes of expressions while maintaining a key invariant: the equivalence relation is closed under congruence. e.g. If I were to represent "f(x)" and "f(y)" in the e-graph, and then said "x == y" (merged "x" and "y" in the e-graph), then the e-graph, by congruence, would be able to tell me that "f(x) == f(y)" e.g. If I were to represent "a*(2/2)", in the e-graph, then say "2/2 == 1", and "x*1 == x", by congruence the e-graph would know "a*(2/2) == a" ! The most recent description of e-graphs with an added insight on implementation is https://arxiv.org/pdf