Equivalence Hypergraphs: DPO Rewriting for Monoidal E-Graphs
Fuente:
arXiv
Gespeichert in:
| Hauptverfasser: | , , , |
|---|---|
| Format: | Preprint |
| Veröffentlicht: |
2024
|
| Schlagworte: | |
| Online-Zugang: | |
| Tags: |
Tag hinzufügen
Keine Tags, Fügen Sie den ersten Tag hinzu!
|
| _version_ | 1866913848279171072 |
|---|---|
| author | Tiurin, Aleksei Barrett, Chris Ghica, Dan R. Hu, Nick |
| author_facet | Tiurin, Aleksei Barrett, Chris Ghica, Dan R. Hu, Nick |
| contents | 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. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2406_15882 |
| institution | arXiv |
| publishDate | 2024 |
| record_format | arxiv |
| spellingShingle | Equivalence Hypergraphs: DPO Rewriting for Monoidal E-Graphs Tiurin, Aleksei Barrett, Chris Ghica, Dan R. Hu, Nick Logic in Computer Science Category Theory 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. |
| title | Equivalence Hypergraphs: DPO Rewriting for Monoidal E-Graphs |
| topic | Logic in Computer Science Category Theory |
| url | https://arxiv.org/abs/2406.15882 |