String diagram rewrite theory II: Rewriting with symmetric monoidal structure
From MaRDI portal
Publication:5058366
Abstract: Symmetric monoidal theories (SMTs) generalise algebraic theories in a way that make them suitable to express resource-sensitive systems, in which variables cannot be copied or discarded at will. In SMTs, traditional tree-like terms are replaced by string diagrams, topological entities that can be intuitively thoughts as diagrams of wires and boxes. Recently, string diagrams have become increasingly popular as a graphical syntax to reason about computational models across diverse fields, including programming language semantics, circuit theory, quantum mechanics, linguistics, and control theory. In applications, it is often convenient to implement the equations appearing in SMTs as rewriting rules. This poses the challenge of extending the traditional theory of term rewriting, which has been developed for algebraic theories, to string diagrams. In this paper, we develop a mathematical theory of string diagram rewriting for SMTs. Our approach exploits the correspondence between string diagram rewriting and double pushout (DPO) rewriting of certain graphs, introduced in the first paper of this series. Such a correspondence is only sound when the SMT includes a Frobenius algebra structure. In the present work, we show how an analogous correspondence may be established for arbitrary SMTs, once an appropriate notion of DPO rewriting (which we call convex) is identified. As proof of concept, we use our approach to show termination of two SMTs of interest: Frobenius semi-algebras and bialgebras.
Recommendations
Cites work
- scientific article; zbMATH DE number 1705158 (Why is no real title available?)
- scientific article; zbMATH DE number 2125662 (Why is no real title available?)
- scientific article; zbMATH DE number 1189283 (Why is no real title available?)
- scientific article; zbMATH DE number 19499 (Why is no real title available?)
- scientific article; zbMATH DE number 1482700 (Why is no real title available?)
- scientific article; zbMATH DE number 1373521 (Why is no real title available?)
- scientific article; zbMATH DE number 2087441 (Why is no real title available?)
- scientific article; zbMATH DE number 1889386 (Why is no real title available?)
- A combinatorial-topological shape category for polygraphs
- A functorial semantics for multi-algebras and partial algebras, with applications to syntax.
- A survey of graphical languages for monoidal categories
- Adhesive and quasiadhesive categories
- Algebra and Coalgebra in Computer Science
- Algebraic operations and generic effects
- An Algorithm for Subgraph Isomorphism
- An enriched view on the extended finitary monad-Lawvere theory correspondence
- Categorical algebra
- Categories in control
- Categorified cyclic operads
- Category theoretic understandings of universal algebra and its dual: monads and Lawvere theories, comonads and what?
- Causal inference by string diagram surgery
- Coalgebras and cartesian categories
- Computational effects and operations: an overview
- Confluence of graph rewriting with interfaces
- Countable Lawvere theories and computational effects
- Diagrammatic Semantics for Digital Circuits.
- Foundations of Software Science and Computation Structures
- Foundations of Software Science and Computation Structures
- Gabriel–Ulmer duality and Lawvere theories enriched over a general base
- Graph rewriting for the π-calculus
- Higher-dimensional word problems with applications to equational logic
- Interacting quantum observables: categorical algebra and diagrammatics
- Notions of computation and monads
- Open-graphs and monoidal theories
- Picturing quantum processes. A first course in quantum theory and diagrammatic reasoning
- Quantomatic: a proof assistant for diagrammatic reasoning
- Refinement for signal flow graphs
- Rewriting modulo symmetric monoidal structure
- Rewriting with Frobenius
- Semantics for algebraic operations
- String diagram rewrite theory. I: Rewriting with Frobenius structure
- Synthesising CCS bisimulation using graph rewriting
- Termination orders for three-dimensional rewriting
- The Frobenius anatomy of word meanings. I: Subject and object relative pronouns
- The algebra of partial equivalence relations
- The calculus of signal flow diagrams. I: Linear relations on streams.
- The category theoretic understanding of universal algebra: Lawvere theories and monads
- The geometry of tensor calculus. I
- Towards 3-dimensional rewriting theory
- Towards an algebraic theory of Boolean circuits.
- Traced monoidal categories
- \(H^\ast\)-algebras and nonunital Frobenius algebras: first steps in infinite-dimensional categorical quantum mechanics
- \textsf{Globular}: an online proof assistant for higher-dimensional rewriting
Cited in
(11)- Pattern graph rewrite systems
- Equational reasoning with context-free families of string diagrams
- Rewriting for monoidal closed categories
- A categorical approach to synthetic chemistry
- Truth diagrams for some non-classical and modal logics
- String diagram rewrite theory III: Confluence with and without Frobenius
- Rewriting modulo symmetric monoidal structure
- Quantomatic: a proof assistant for diagrammatic reasoning
- An axiomatic approach to differentiation of polynomial circuits
- String diagram rewrite theory. I: Rewriting with Frobenius structure
- Open-graphs and monoidal theories
This page was built for publication: String diagram rewrite theory II: Rewriting with symmetric monoidal structure
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q5058366)
