E-Graphs With Bindings

TL;DR

This work addresses the lack of native binding support in traditional e-graphs by embedding e-graphs into closed semilattice-enriched symmetric monoidal categories and representing morphisms as string diagrams. It introduces a combinatorial model using hierarchical e-hypergraphs and develops a DPOI rewriting framework that is sound and complete with respect to rewriting closed $\Sigma^{+}$-terms modulo the monoidal laws, absorbing binding and equivalence structure into composition. The key contributions include a categorical semantics for binding-enabled e-graphs, a hypergraph-based representation that accommodates binding through hierarchical boxes, and an EDPOI rewriting strategy that faithfully implements equational reasoning for the monoidal setting. This framework enables robust equality-saturation techniques for languages with binding (notably $\lambda$-calculus) and offers a principled path toward more scalable optimization and reasoning in compilers and formal methods.

Abstract

Equality saturation, a technique for program optimisation and reasoning, has gained attention due to the resurgence of equality graphs (e-graphs). E-graphs represent equivalence classes of terms under rewrite rules, enabling simultaneous rewriting across a family of terms. However, they struggle in domains like $λ$-calculus that involve variable binding, due to a lack of native support for bindings. Building on recent work interpreting e-graphs categorically as morphisms in semilattice-enriched symmetric monoidal categories, we extend this framework to closed symmetric monoidal categories to handle bindings. We provide a concrete combinatorial representation using hierarchical hypergraphs and introduce a corresponding double-pushout (DPO) rewriting mechanism. Finally, we establish the equivalence of term rewriting and DPO rewriting, with the key property that the combinatorial representation absorbs the equations of the symmetric monoidal category.

Figures (11)

• Figure 1: String-diagrammatic representation of $\lambda f . f ((\lambda x . f x) 2)$.
• Figure 2: E-graph example (top) and its equivalent string diagram representation (bottom) \citeghica2024equivalencehypergraphsegraphsmonoidal
• Figure 3: String diagrams for closed semilattice-enriched symmetric monoidal categories.
• Figure 4: DPO and DPOI squares
• Figure 5: Cospan of e-hypergraphs example

Theorems & Definitions (53)

• Definition 2.1
• Definition 2.2
• Definition 2.3
• Definition 2.4
• Definition 2.5
• Definition 2.6
• Definition 2.7
• Definition 2.8
• Definition 2.9: Semilattice-enriched category Borceux_1994
• Definition 2.10: $\mathbf{SLat}$-functor