Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Equivalence Hypergraphs: DPO Rewriting for Monoidal E-Graphs

Aleksei Tiurin, Chris Barrett, Dan R. Ghica, Nick Hu

TL;DR

Equivalence Hypergraphs provides a semantic bridge from e-graphs used in equality saturation to monoidal string-diagram theories by enriching hom-sets with semilattice joins. It develops e-hypergraphs as a combinatorial, DPOI-friendly representation of morphisms in semilattice-enriched symmetric monoidal categories (SMCs) and PROPs, absorbing SMC equations into isomorphisms and treating enrichment equations via rewriting. The paper proves soundness and completeness of this representation with respect to the $ extbf{SLat}$-enriched category semantics, enabling systematic rewriting of equivalence classes through EDPOI rules. This framework generalizes e-graphs from Cartesian to monoidal theories, enabling principled, semantics-preserving rewrites across a broad class of algebraic and monoidal systems for program optimisation and beyond.

Abstract

The technique of \emph{equality saturation}, which equips graphs with an equivalence relation, has proven effective for program optimisation. We give a categorical semantics to these structures, called \emph{e-graphs}, in terms of Cartesian categories enriched over the category of semilattices. This approach generalises to monoidal categories, which opens the door to new applications of e-graph techniques, from algebraic to monoidal theories. Finally, we present a sound and complete combinatorial representation of morphisms in such a category, based on a generalisation of hypergraphs which we call \emph{e-hypergraphs}. They have the usual advantage that many of their structural equations are absorbed into a general notion of isomorphism. This new principled approach to e-graphs enables double-pushout (DPO) rewriting for these structures, which constitutes the main contribution of this paper.

Equivalence Hypergraphs: DPO Rewriting for Monoidal E-Graphs

TL;DR

Equivalence Hypergraphs provides a semantic bridge from e-graphs used in equality saturation to monoidal string-diagram theories by enriching hom-sets with semilattice joins. It develops e-hypergraphs as a combinatorial, DPOI-friendly representation of morphisms in semilattice-enriched symmetric monoidal categories (SMCs) and PROPs, absorbing SMC equations into isomorphisms and treating enrichment equations via rewriting. The paper proves soundness and completeness of this representation with respect to the -enriched category semantics, enabling systematic rewriting of equivalence classes through EDPOI rules. This framework generalizes e-graphs from Cartesian to monoidal theories, enabling principled, semantics-preserving rewrites across a broad class of algebraic and monoidal systems for program optimisation and beyond.

Abstract

The technique of \emph{equality saturation}, which equips graphs with an equivalence relation, has proven effective for program optimisation. We give a categorical semantics to these structures, called \emph{e-graphs}, in terms of Cartesian categories enriched over the category of semilattices. This approach generalises to monoidal categories, which opens the door to new applications of e-graph techniques, from algebraic to monoidal theories. Finally, we present a sound and complete combinatorial representation of morphisms in such a category, based on a generalisation of hypergraphs which we call \emph{e-hypergraphs}. They have the usual advantage that many of their structural equations are absorbed into a general notion of isomorphism. This new principled approach to e-graphs enables double-pushout (DPO) rewriting for these structures, which constitutes the main contribution of this paper.
Paper Structure (20 sections, 25 theorems, 71 equations, 10 figures)

This paper contains 20 sections, 25 theorems, 71 equations, 10 figures.

Table of Contents

  1. Introduction
  2. E-graphs
  3. Semilattice Enriched Categories
  4. Combinatorial Representation of Enriched String Diagrams
  5. Soundness and Completeness
  6. Related Work
  7. Categorical Semantics of E-Graphs
  8. Symmetric Monoidal Theories and PROPs.
  9. Free Semilattice Enrichment: Formal Joins
  10. String Diagram Rewrite Theory
  11. Hypergraphs
  12. DPOI-Rewriting for Hypergraphs with Interfaces
  13. E-Hypergraphs
  14. DPOI-Rewriting for E-Hypergraphs
  15. Soundness and Completeness
  16. ...and 5 more sections

Key Result

Proposition 2.9

(A specialized case of Proposition 6.4.3 Borceux_1994. See also Appendix sec:appendix:slat) There is a 2-adjunction that is induced by a usual free-forgetful adjunction

Figures (10)

  • Figure 1: Example translation of acyclic e-graphs into string diagrams for semilattice-enriched Cartesian categories.
  • Figure 2: String diagrams for semilattice-enriched symmetric monoidal categories.
  • Figure 3: E-graph e-class translation to string diagram.
  • Figure 4: Equations for a semilattice-enriched symmetric monoidal category
  • Figure 5: DPO and DPOI squares
  • ...and 5 more figures

Theorems & Definitions (86)

  • Definition 2.1: Monoidal signature
  • Definition 2.2: Products and permutations category
  • Definition 2.3: Symmetric Monoidal Theory (Definition 2.1 bonchi_string_2022-1)
  • Definition 2.4
  • Example 2.5
  • Definition 2.6: Semilattice-enriched category
  • Definition 2.7: $\mathbf{SLat}$-functor
  • Definition 2.8: $\mathbf{SLat}$-SMC
  • Proposition 2.9
  • Definition 2.10
  • ...and 76 more