E-Graphs With Bindings
Fuente:
arXiv
Gespeichert in:
| Hauptverfasser: | , , |
|---|---|
| Format: | Preprint |
| Veröffentlicht: |
2025
|
| Schlagworte: | |
| Online-Zugang: | |
| Tags: |
Tag hinzufügen
Keine Tags, Fügen Sie den ersten Tag hinzu!
|
| _version_ | 1866913816104665088 |
|---|---|
| author | Tiurin, Aleksei Ghica, Dan R. Hu, Nick |
| author_facet | Tiurin, Aleksei Ghica, Dan R. Hu, Nick |
| contents | 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. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2505_00807 |
| institution | arXiv |
| publishDate | 2025 |
| record_format | arxiv |
| spellingShingle | E-Graphs With Bindings Tiurin, Aleksei Ghica, Dan R. Hu, Nick Logic in Computer Science Category Theory 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. |
| title | E-Graphs With Bindings |
| topic | Logic in Computer Science Category Theory |
| url | https://arxiv.org/abs/2505.00807 |