An e-graph, short for “equality graph,” is a data structure that maintains a congruence relation on expression trees: an equivalence relation stable under forming new expressions. First devised by Nelson and Oppen in 1980 (Nelson 1980; Nelson and Oppen 1980), e-graphs received a surge of new attention when Willsey et al demonstrated, via their software package egg, that e-graphs combined with equality saturation can be a fast, powerful, and adaptable tool for equational reasoning (Willsey et al. 2021). In my own work on CatColab, I’ve begun using egg’s successor, egglog (Zhang et al. 2023), to reason about finitely presented categories.
Standard presentations, beginning with Nelson’s PhD thesis (Nelson 1980), emphasize the data structures and algorithms needed to implement e-graphs, such as the union-find data structure. It’s crucial that work in computer algebra ultimately touch the ground in this way. Still, I can’t help but wonder what, abstracted from the implementation details, is really going on with e-graphs. The diagrammatic and visual nature of e-graphs, so apparent in the interactive egglog demo, will suggest to any category theorist that categorical ideas may be implicitly at work.
