Rewriting modulo symmetric monoidal structure
From MaRDI portal
Publication:4635934
Abstract: 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.
Recommendations
Cited in
(33)- Pattern graph rewrite systems
- A practical type theory for symmetric monoidal categories
- String diagram rewrite theory III: Confluence with and without Frobenius
- Diagram rewriting and operads
- Graphical Conjunctive Queries.
- Towards large-scale functional verification of universal quantum circuits
- Equational reasoning with context-free families of string diagrams
- A Category of Surface-Embedded Graphs
- Data Structures for Topologically Sound Higher-Dimensional Diagram Rewriting
- scientific article; zbMATH DE number 7649945 (Why is no real title available?)
- scientific article; zbMATH DE number 7450015 (Why is no real title available?)
- Interacting Hopf algebras
- Rewriting with Frobenius
- Properties of co-operations: diagrammatic proofs
- Open-graphs and monoidal theories
- Completeness of Nominal PROPs
- The cost of compositionality: a high-performance implementation of string diagram composition
- Free gs-monoidal categories and free Markov categories
- scientific article; zbMATH DE number 7649903 (Why is no real title available?)
- Confluence of graph rewriting with interfaces
- Quantomatic: a proof assistant for diagrammatic reasoning
- scientific article; zbMATH DE number 7649901 (Why is no real title available?)
- A structural and nominal syntax for diagrams
- A finite presentation of CNOT-dihedral operators
- Bialgebraic foundations for the operational semantics of string diagrams
- scientific article; zbMATH DE number 7649898 (Why is no real title available?)
- String diagram rewrite theory. I: Rewriting with Frobenius structure
- String diagram rewrite theory II: Rewriting with symmetric monoidal structure
- Reverse derivative ascent: a categorical approach to learning Boolean circuits
- Wiring diagrams as normal forms for computing in symmetric monoidal categories
- Encoding !-tensors as !-graphs with neighbourhood orders
- Petri nets are dioids: a new algebraic foundation for non-deterministic net theory
- Rewriting for monoidal closed categories
This page was built for publication: Rewriting modulo symmetric monoidal structure
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q4635934)
