一句话：提出槽位 E-Graph，将绑定变量作为内建一等特性，使仅变量名不同的项共享表示，避免 E-Graph 膨胀。
Equality saturation 以 e-graph 高效唯一表示等价子项，但将 e-graph 扩展到含（绑定）变量的语言时，无论用名字还是 de Bruijn 索引表示变量，仅变量名不同的子项都会被分开表示，破坏共享，导致 e-graph 膨胀、性能下降和表达力受限。本文提出 slotted e-graph，将绑定变量作为数据结构的内建一等特性，用 slots 参数化表示等价项的 e-class 以抽象其自由变量；e-node 引用 e-class 时需将上下文变量关联到该 e-class 的 slots。评估通过编译器优化与定理证明两个案例研究，表明对有绑定变量的语言执行 equality saturation 被大幅简化，并能解决使用 de Bruijn 索引 e-graph 无法处理的实用问题。
Equality saturation has gained significant interest as a powerful optimization and reasoning technique. At its heart is the e-graph data structure, that space-efficiently represents equal sub-terms uniquely. An important open problem in this context is extending this efficient representation to languages featuring (bound) variables. Independent of how we represent variables in e-graphs, either as names or nameless (using de Bruijn indices), sharing is broken as sub-terms that differ only in the names of their variables are represented separately. This results in aggressive e-graph growth, bad performance, as well as reduced expressiveness. In this paper, we present a novel approach to representing bound variables in e-graphs by making them a first-class built-in feature of the data structure. Our slotted e-graph represents terms that differ only by (bound or free) variable names uniquely. To do so, e-classes that represent equivalent terms via e-nodes are parameterized by slots , abstracting over free variables of the represented terms. Referring to an e-class from an e-node now requires relating the variables from its context to the slots of the e-class. Our evaluation of slotted e-graph uses two case studies from compiler optimization and theorem proving to show that performing equality saturation for languages with bound variables is greatly simplified and that we can solve practically relevant problems that cannot be solved with e-graphs using de Bruijn indices.
@article{paperbot3096,
title = {Slotted E-Graphs: First-Class Support for (Bound) Variables in E-Graphs},
author = {Rudi Schneider and Marcus Rossel and Amir Shaikhha and Andrés Goens and Thomas Kœhler and Michel Steuwer},
journal = {Proceedings of the ACM on Programming Languages},
volume = {9},
number = {PLDI},
year = {2025},
doi = {10.1145/3729326}
}