Representing languages with bound variables in e-graphs is not straightforward. Using plain names results in reduced sharing, as multiple terms that are equivalent up to renaming are represented redundantly in the e-graph. De-Bruijn indices suffer from the same problem. Furthermore, rewriting can trigger the need to rename variables (or shift indices), such as when performing 𝛽-reduction, which can dramatically increase the size of the e-graph.

In this work, we present a novel approach to representing bound variables in e-graphs by making them a built-in feature of the data structure. In our slotted e-graph, e-classes are parameterized by slots abstracting over all free variables. Referring to an e-class now requires instantiating it by assigning a name from the user’s context to each slot. Renaming variables corresponds simply to different instantiations of an e-class.

Representing variables and 𝛽-reduction efficiently is an important topic in many applications of equality saturation, and we hope that this talk will spark interest with the audience of the EGRAPHS workshop