E-graphs are good. They are a powerful, general-purpose mechanism for representing sets of programs and reasoning about those sets of programs via equational rules. My colleagues at the University of Washington who work on the Egg library have been developing a "cookbook" of techniques for common subexpression elimination, synthesis, constant folding, and binding in e-graphs. This post is a new take on represent binding in an e-graph. The problem of binding The basic problem is that. Suppose ...
