Equivalence Hypergraphs: DPO Rewriting for Monoidal E-Graphs

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

doi:10.1109/LICS65433.2025.00023

Equivalence Hypergraphs: DPO Rewriting for Monoidal E-Graphs

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

Computer Science

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution

5 Downloads (Pure)

Abstract

The technique of equality saturation, which equips graphs with an equivalence relation, has proven effective for program optimisation. We give a categorical semantics to these structures, called 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 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.

Original language	English
Title of host publication	2025 40th Annual ACM/IEEE Symposium on Logic in Computer Science (LICS)
Publisher	IEEE
Pages	209-222
Number of pages	14
ISBN (Electronic)	9798331579012
ISBN (Print)	9798331579005 (PoD)
DOIs	https://doi.org/10.1109/LICS65433.2025.00023
Publication status	Published - 9 Oct 2025
Event	2025 40th Annual ACM/IEEE Symposium on Logic in Computer Science (LICS) - Singapore, Singapore Duration: 23 Jun 2025 → 26 Jun 2025

Publication series

Name	Annual Symposium on Logic in Computer Science
Publisher	IEEE
ISSN (Print)	1043-6871
ISSN (Electronic)	2575-5528

Conference

Conference	2025 40th Annual ACM/IEEE Symposium on Logic in Computer Science (LICS)
Period	23/06/25 → 26/06/25

Keywords

Computer science
Translation
Semantics
Mathematical models
Logic
Category Theory
String Diagrams
monoidal categories
Optimization
equality saturation

Access to Document

10.1109/LICS65433.2025.00023Licence: None: All rights reserved

TiurinA2025Equivalence_AAMAccepted author manuscript, 524 KBLicence: Creative Commons: Attribution (CC BY)

1 Finished
1 Active

Semantics-Directed Compiler Construction: From Formal Semantics to Certified Compilers
Ghica, D. (Principal Investigator)
Engineering & Physical Science Research Council
1/05/24 → 31/03/27
Project: Research Councils
Nominal String Diagrams
Ghica, D. (Principal Investigator)
Engineering & Physical Science Research Council
1/12/20 → 31/05/24
Project: Research Councils

Cite this

@inproceedings{8e0fa428e7fb4d5abf613b2ad9dcbaea,

title = "Equivalence Hypergraphs: DPO Rewriting for Monoidal E-Graphs",

abstract = "The technique of equality saturation, which equips graphs with an equivalence relation, has proven effective for program optimisation. We give a categorical semantics to these structures, called 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 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.",

keywords = "Computer science, Translation, Semantics, Mathematical models, Logic, Category Theory, String Diagrams, monoidal categories, Optimization, equality saturation",

author = "Aleksei Tiurin and Chris Barrett and Ghica, \{Dan R.\} and Nick Hu",

year = "2025",

month = oct,

day = "9",

doi = "10.1109/LICS65433.2025.00023",

language = "English",

isbn = "9798331579005 (PoD)",

series = "Annual Symposium on Logic in Computer Science",

publisher = "IEEE",

pages = "209--222",

booktitle = "2025 40th Annual ACM/IEEE Symposium on Logic in Computer Science (LICS)",

note = "2025 40th Annual ACM/IEEE Symposium on Logic in Computer Science (LICS) ; Conference date: 23-06-2025 Through 26-06-2025",

}

Tiurin, A, Barrett, C, Ghica, DR & Hu, N 2025, Equivalence Hypergraphs: DPO Rewriting for Monoidal E-Graphs. in 2025 40th Annual ACM/IEEE Symposium on Logic in Computer Science (LICS)., 11186301, Annual Symposium on Logic in Computer Science, IEEE, pp. 209-222, 2025 40th Annual ACM/IEEE Symposium on Logic in Computer Science (LICS), 23/06/25. https://doi.org/10.1109/LICS65433.2025.00023

TY - GEN

T1 - Equivalence Hypergraphs

T2 - 2025 40th Annual ACM/IEEE Symposium on Logic in Computer Science (LICS)

AU - Tiurin, Aleksei

AU - Barrett, Chris

AU - Ghica, Dan R.

AU - Hu, Nick

PY - 2025/10/9

Y1 - 2025/10/9

N2 - The technique of equality saturation, which equips graphs with an equivalence relation, has proven effective for program optimisation. We give a categorical semantics to these structures, called 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 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.

AB - The technique of equality saturation, which equips graphs with an equivalence relation, has proven effective for program optimisation. We give a categorical semantics to these structures, called 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 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.

KW - Computer science

KW - Translation

KW - Semantics

KW - Mathematical models

KW - Logic

KW - Category Theory

KW - String Diagrams

KW - monoidal categories

KW - Optimization

KW - equality saturation

U2 - 10.1109/LICS65433.2025.00023

DO - 10.1109/LICS65433.2025.00023

M3 - Conference contribution

SN - 9798331579005 (PoD)

T3 - Annual Symposium on Logic in Computer Science

SP - 209

EP - 222

BT - 2025 40th Annual ACM/IEEE Symposium on Logic in Computer Science (LICS)

PB - IEEE

Y2 - 23 June 2025 through 26 June 2025

ER -

Equivalence Hypergraphs: DPO Rewriting for Monoidal E-Graphs

Abstract

Publication series

Conference

Keywords

Access to Document

Fingerprint

Projects

Semantics-Directed Compiler Construction: From Formal Semantics to Certified Compilers

Nominal String Diagrams

Cite this