Equivalence Hypergraphs: E-Graphs for Monoidal Theories
summary
Presents a categorical construction that generalises e-graphs to arbitrary monoidal theories by representing string diagrams as combinatorial Equivalence Hypergraphs, absorbing all monoidal laws so diagrams are already “saturated.” Claims soundness and completeness for representing enriched symmetric monoidal theories, shows how traditional e-graphs appear as a special case for Cartesian monoidal theories, and demonstrates concrete translations: hierarchal boxes for e-classes, non‑destructive rewrite steps that preserve sharing, and a single diagrammatic beta‑reduction rule for lambda binding using string diagrams and e-graphs as special case.
AI-written summary · about
chapters (18)
- 0:00Introduction
- 1:32Algebraic to monoidal theories
- 4:04Monoidal theories applications
- 6:54Symmetric monoidal theories
- 9:06E-graph challenges
- 10:49String diagrams solution
- 13:20String diagrams benefits
- 16:14Formalizing E-hypergraphs
- 19:28Enriched diagrams semantics
- 22:03Rewriting with E-hypergraphs
- 23:09E-graphs special case
- 25:16Translating E-classes
- 27:26E-class evolution example
- 28:31Non-destructive rewriting
- 31:05Binding with diagrams
- 32:35Lambda calculus example
- 34:24Future work
- 35:52Open questions
related talks
35mOmelets Need Onions: E-graphs Modulo Theories via Bottom Up E-Matching
27mFunctorial Semantics for Partial Theories
28mModular Models of Monoids with Operations
30mDisplayed Monoidal Categories for the Semantics of Linear Logic
56mCategory Theory Through Functional Programming (part 2/3)
25mLifting E-Graphs: A Function Isn’t a Constant
23mVersioned E-Graphs
20mSlotted E-Graphs: First-Class Support for (Bound) Variables in E-Graphs