Rewriting modulo symmetric monoidal structure
From MaRDI portal
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
(38)- Petri nets are dioids: a new algebraic foundation for non-deterministic net theory
- Bialgebraic foundations for the operational semantics of string diagrams
- Diagram rewriting and operads
- Equational reasoning with context-free families of string diagrams
- Confluence of graph rewriting with interfaces
- Interacting Hopf algebras
- A structural and nominal syntax for diagrams
- A finite presentation of CNOT-dihedral operators
- Towards large-scale functional verification of universal quantum circuits
- Quantomatic: a proof assistant for diagrammatic reasoning
- Properties of co-operations: diagrammatic proofs
- Open-graphs and monoidal theories
- Pattern graph rewrite systems
- A practical type theory for symmetric monoidal categories
- Encoding !-tensors as !-graphs with neighbourhood orders
- A framework for rewriting families of string diagrams
- Wiring diagrams as normal forms for computing in symmetric monoidal categories
- Reverse derivative ascent: a categorical approach to learning Boolean circuits
- String diagram rewrite theory II: Rewriting with symmetric monoidal structure
- String diagram rewrite theory. I: Rewriting with Frobenius structure
- Graphical Conjunctive Queries.
- Rewriting with Frobenius
- The axiom of choice in cartesian bicategories
- Nominal string diagrams
- CARTOGRAPHER: a tool for string diagrammatic reasoning (tool paper)
- Bialgebraic semantics for string diagrams
- String diagram rewrite theory III: Confluence with and without Frobenius
- Completeness of Nominal PROPs
- Free gs-monoidal categories and free Markov categories
- A Category of Surface-Embedded Graphs
- Data Structures for Topologically Sound Higher-Dimensional Diagram Rewriting
- The cost of compositionality: a high-performance implementation of string diagram composition
- Rewriting for monoidal closed categories
- Derivatives on graphs for the positive calculus of relations with transitive closure
- Logic programming with multiplicative structures
- String diagrams with factorized densities
- Rewriting for symmetric monoidal categories with commutative (co)monoid structure
- A complete diagrammatic calculus for automata simulation
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)
