Rewriting modulo symmetric monoidal structure
Not on the map. Why?
Abstract (arXiv)
String diagrams are a powerful and intuitive graphical syntax for terms of symmetric monoidal categories (SMCs). They find many applications in computer science and are becoming increasingly relevant in other fields such as physics and control theory. An important role in many such approaches is played by equational theories of diagrams, typically oriented and applied as rewrite rules. This paper lays a comprehensive foundation of this form of rewriting. We interpret diagrams combinatorially as typed hypergraphs and establish the precise correspondence between diagram rewriting modulo the laws of SMCs on the one hand and double pushout (DPO) rewriting of hypergraphs, subject to a soundness condition called convexity, on the other. This result rests on a more general characterisation theorem in which we show that typed hypergraph DPO rewriting amounts to diagram rewriting modulo the laws of SMCs with a chosen special Frobenius structure. We illustrate our approach with a proof of termination for the theory of non-commutative bimonoids.
Key facts. Cited by 4 papers in the map (data through 14 Oct 2026). First posted on arXiv 22 Feb 2016.
Builds on
No reference list yet.
Built on by
Citing papers per year: 2021: 2; 2022: 1; 2023: 1.
4 papers.
- 2023String Diagrams with Factorized Densities4 May 2023
- 2022The d-separation criterion in Categorical Probability12 Jul 2022
- 2021Functorial String Diagrams for Reverse-Mode Automatic Differentiation28 Jul 2021
- 2021Reverse Derivative Ascent: A Categorical Approach to Learning Boolean Circuits26 Jan 2021