egglog

The recent work on relational, datalog-inspired egraphs in PLDI this year ("Unifying Datalog and Equality Saturation") is actually interesting because it can solve cases like the y/x*x -> y identity example, by the power of an interval analysis on x (among other things.) Sort of like adding a postulate to a rewrite term and then proving it. But instead it's by adding relations between terms in the graph. See section 6.2 of the paper. https://github.com/egraphs-good/egglog https://arxiv.org/pdf/2304.04332.pdf

A more direct link to a list of applications of egraphs is 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 with a wasm compiled web demo with examples here 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 http://www.philipzucker.com/egglog/

Close, but the link is on Page 13, and it points here: https://github.com/mwillsey/egg-smol Unfortunately the naming is all a bit confusing, isn't it....