EGGs are adhesive!
Roberto Biondo, Davide Castelnovo, Fabio Gadducci
TL;DR
The paper develops a comprehensive adhesive-categorical foundation for EGGs (E-graphs), formalizing hypergraphs, term graphs, and their extensions with equivalence relations within $ ext{M}$-adhesive categories. It shows that hypergraphs, term graphs, and their equivalence-extended variants are adhesive (or quasi-adhesive) under suitable classes of monos, enabling rewriting via double-pushout (DPO) steps, possibly with negative application conditions. By introducing e-hypergraphs and labelled e-hypergraphs, the authors build up to EGGs as term graphs with equivalence closed under operator application, providing a rigorous framework for equality saturation-based program optimization. The adhesive formulation yields precise modeling of concurrency and parallelism in updates and supports confluence/termination analyses. The work also outlines future directions, including extending to DPO rewriting, hierarchical EGGS, and comparisons with alternative formalisms such as Ghica’s approach.
Abstract
The use of rewriting-based visual formalisms is on the rise. In the formal methods community, this is due also to the introduction of adhesive categories, where most properties of classical approaches to graph transformation, such as those on parallelism and confluence, can be rephrased and proved in a general and uniform way.E-graphs (EGGs) are a formalism for program optimisation via an efficient implementation of equality saturation. In short, EGGs can be defined as (acyclic) term graphs with an additional notion of equivalence on nodes that is closed under the operators of the signature. Instead of replacing the components of a program, the optimisation step is performed by adding new components and linking them to the existing ones via an equivalence relation, until an optimal program is reached. This work describes EGGs via adhesive categories. Besides the benefits in itself of a formal presentation, which renders the properties of the data structure precise, the description of the addition of equivalent program components using standard graph transformation tools offers the advantages of the adhesive framework in modelling, for example, concurrent updates.