一句话：提出 rebuilding 与 e-class analyses 两项技术，使 e-graph 在等式饱和场景下兼具高性能与可扩展性，并实现开源库 egg。
e-graph 能高效表示多个表达式间的同余关系，近年被等式饱和技术重新用于实现先进的改写驱动编译器优化与程序合成。然而 e-graph 并未针对这一新用途特化：等式饱和工作负载具有独特特征，且常需临时性扩展以支持超越纯语法改写的变换。本文贡献两项技术使 e-graph 快速且可扩展。其一是称为 rebuilding 的摊销式不变式恢复技术，利用等式饱和工作负载的特点，在实践中相较现有方法获得渐近加速；其二是称为 e-class analyses 的通用机制，将领域特定分析集成进 e-graph，减少临时性手工操作。作者将这些技术实现在开源库 egg 中，并在三个已发表的等式饱和应用案例上开展研究，表明 egg 的性能与灵活性可在多个领域取得当前最优结果。
An e-graph efficiently represents a congruence relation over many expressions. Although they were originally developed in the late 1970s for use in automated theorem provers, a more recent technique known as equality saturation repurposes e-graphs to implement state-of-the-art, rewrite-driven compiler optimizations and program synthesizers. However, e-graphs remain unspecialized for this newer use case. Equality saturation workloads exhibit distinct characteristics and often require ad-hoc e-graph extensions to incorporate transformations beyond purely syntactic rewrites. This work contributes two techniques that make e-graphs fast and extensible, specializing them to equality saturation. A new amortized invariant restoration technique called rebuilding takes advantage of equality saturation's distinct workload, providing asymptotic speedups over current techniques in practice. A general mechanism called e-class analyses integrates domain-specific analyses into the e-graph, reducing the need for ad hoc manipulation. We implemented these techniques in a new open-source library called egg. Our case studies on three previously published applications of equality saturation highlight how egg's performance and flexibility enable state-of-the-art results across diverse domains.
@article{paperbot1142,
title = {egg: Fast and extensible equality saturation},
author = {Max Willsey and Chandrakana Nandi and Yisu Remy Wang and Oliver Flatt and Zachary Tatlock and Pavel Panchekha},
journal = {Proceedings of the ACM on Programming Languages},
volume = {5},
number = {POPL},
year = {2021},
doi = {10.1145/3434304}
}