How to prove equations using diagrams, part 1 – Evan’s Blog
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.