I think you'll be (very!) interested in e-graphs: https://en.wikipedia.org/wiki/E-graph https://en.wikipedia.org/wiki/E-graph Google fodder: "Equality Satura

I think you'll be (very!) interested in e-graphs: https://en.wikipedia.org/wiki/E-graph https://en.wikipedia.org/wiki/E-graph Google fodder: "Equality Saturation: A New Approach to Optimization" "Denali: A Goal-directed Superoptimizer" "Z3: An Efficient SMT Solver" "Efficient E-matching for SMT Solvers" "egg: Fast and Extensible Equality Saturation" "Rewrite Rule Inference Using Equality Saturation"