# egg: Fast and Extensible Equality Saturation

**Authors:** Max Willsey, Chandrakana Nandi, Yisu Remy Wang, Oliver Flatt, Zachary Tatlock, Pavel Panchekha  
**arXiv:** [2004.03082](https://arxiv.org/abs/2004.03082)  
**Date:** 2020-04-07  
**Summary page:** https://www.summarizepaper.com/en/arxiv-id/2004.03082v3/

## Key points

- E-graphs were originally developed in the late 1970s for automated theorem provers and have been repurposed for state-of-the-art compiler optimizations and program synthesis through equality saturation.
- E-graphs lack specialization for equality saturation workloads, which often require additional transformations beyond simple syntactic rewrites.
- The researchers propose two key techniques tailored to equality saturation: rebuilding and integrating domain-specific analyses through e-class analyses.
- The proposed techniques are implemented in a new open-source library named egg, which offers practical speedups over existing techniques.
- Through case studies on three previously published applications of equality saturation, the authors demonstrate how egg's performance and flexibility enable cutting-edge results across diverse domains.

## Summary

, , , , 

In their paper titled "egg: Fast and Extensible Equality Saturation," Max Willsey, Chandrakana Nandi, Yisu Remy Wang, Oliver Flatt, Zachary Tatlock, and Pavel Panchekha introduce techniques to enhance the efficiency and extensibility of e-graphs for equality saturation. E-graphs were originally developed in the late 1970s for automated theorem provers but have since been repurposed for state-of-the-art compiler optimizations and program synthesis through equality saturation. The authors highlight that while e-graphs have proven useful in these newer applications, they lack specialization for equality saturation workloads. These workloads often require additional transformations beyond simple syntactic rewrites, necessitating ad-hoc extensions to e-graph functionality. To address this gap, the researchers propose two key techniques tailored to equality saturation. The first technique, called rebuilding, leverages an amortized invariant restoration approach to capitalize on the distinct characteristics of equality saturation workloads. This method offers practical speedups over existing techniques. The second technique involves integrating domain-specific analyses into e-graphs through a mechanism known as e-class analyses. By incorporating these analyses directly into the e-graph structure, the need for ad hoc manipulation is reduced. The proposed techniques are implemented in a new open-source library named egg. Through case studies on three previously published applications of equality saturation, the authors demonstrate how egg's performance and flexibility enable cutting-edge results across diverse domains. In addition to their contributions, the authors discuss related work in term rewriting systems commonly used for equational reasoning in program optimization tasks. They emphasize that while term rewriting systems apply semantics-preserving rewrites or axioms to input expressions symbolically, they may not always be as effective or efficient as specialized techniques like those introduced in their work. Overall, "egg: Fast and Extensible Equality Saturation" presents novel approaches to enhancing e-graph capabilities specifically for equality saturation workloads. The research opens up new possibilities for more efficient and effective program optimization and synthesis processes across various domains.