Rewriting modulo symmetric monoidal structure — Filippo Bonchi, Fabio Gadducci, Aleks Kissinger, Pawel Sobocinski & Fabio Zanasi (2016; LICS 2016). arXiv:1602.06771 (v2, PDF).
Shows that rewriting string diagrams — morphisms of free symmetric monoidal categories — can be done by double-pushout rewriting of hypergraphs. With Frobenius structure the correspondence is exact; without it one must restrict to convex matches and convex DPO steps. Establishes hypergraph rewriting as a sound and complete implementation of equational reasoning in symmetric monoidal theories.
Sources: the paper, arXiv:1602.06771v2, checked against the arXiv listing. Index: Papers.
Key definitions and results
- Definition 3.1: hypergraphs
- Definition 3.2, Theorem 3.3: Frobenius termgraphs
- Definition 4.1: DPO rewriting with discrete interfaces
- Theorems 4.4, 4.6: DPO rewriting of termgraphs coincides with rewriting in
- Proposition 4.7: the category of hypergraphs is adhesive
- Definitions 5.4–5.5, Theorem 5.6: convex matches and convex DPO for plain symmetric monoidal theories