String diagram rewrite theory II: Rewriting with symmetric monoidal structure

DOI10.1017/S0960129522000317zbMATH Open1506.68042arXiv2104.14686OpenAlexW3157210582MaRDI QIDQ5058366FDOQ5058366

Fabio Zanasi, Filippo Bonchi, Paweł Sobociński, Fabio Gadducci, Aleks Kissinger

Publication date: 20 December 2022

Published in: Mathematical Structures in Computer Science (Search for Journal in Brave)

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.

Full work available at URL: https://arxiv.org/abs/2104.14686

zbMATH Keywords

symmetric monoidal categorystring diagramdouble-pushout rewriting

Mathematics Subject Classification ID

Grammars and rewriting systems (68Q42) Monoidal categories, symmetric monoidal categories (18M05) String diagrams and graphical calculi (18M30)

Cites Work

• Title not available (Why is that?)
• Title not available (Why is that?)
• Title not available (Why is that?)
• Title not available (Why is that?)
• Title not available (Why is that?)
• Title not available (Why is that?)
• Title not available (Why is that?)
• Title not available (Why is that?)
• An Algorithm for Subgraph Isomorphism
• The geometry of tensor calculus. I
• Algebraic operations and generic effects
• The category theoretic understanding of universal algebra: Lawvere theories and monads
• A Survey of Graphical Languages for Monoidal Categories
• Interacting quantum observables: categorical algebra and diagrammatics
• Notions of computation and monads
• Computational effects and operations: an overview
• Traced monoidal categories
• Category Theoretic Understandings of Universal Algebra and its Dual: Monads and Lawvere Theories, Comonads and What?
• Categorical algebra
• Rewriting modulo symmetric monoidal structure
• \(H^\ast\)-algebras and nonunital Frobenius algebras: first steps in infinite-dimensional categorical quantum mechanics
• Foundations of Software Science and Computation Structures
• Coalgebras and cartesian categories
• Termination orders for three-dimensional rewriting
• Adhesive and quasiadhesive categories
• Higher-dimensional word problems with applications to equational logic
• Towards an algebraic theory of Boolean circuits.
• Categories in Control
• Refinement for signal flow graphs
• Semantics for Algebraic Operations
• Synthesising CCS bisimulation using graph rewriting
• Graph rewriting for the π-calculus
• Gabriel–Ulmer duality and Lawvere theories enriched over a general base
• Algebra and Coalgebra in Computer Science
• The Frobenius anatomy of word meanings I: subject and object relative pronouns
• The calculus of signal flow diagrams. I: Linear relations on streams.
• The algebra of partial equivalence relations
• Countable Lawvere theories and computational effects
• Foundations of Software Science and Computation Structures
• Open-graphs and monoidal theories
• A functorial semantics for multi-algebras and partial algebras, with applications to syntax.
• Picturing Quantum Processes
• Diagrammatic Semantics for Digital Circuits.
• Confluence of Graph Rewriting with Interfaces
• Quantomatic: A Proof Assistant for Diagrammatic Reasoning
• Causal inference by string diagram surgery
• Towards 3-Dimensional Rewriting Theory
• A combinatorial-topological shape category for polygraphs
• Categorified cyclic operads
• An enriched view on the extended finitary monad--Lawvere theory correspondence
• Globular: an online proof assistant for higher-dimensional rewriting
• Rewriting with Frobenius
• String Diagram Rewrite Theory I: Rewriting with Frobenius Structure

Cited In (5)

• An axiomatic approach to differentiation of polynomial circuits
• String Diagram Rewrite Theory I: Rewriting with Frobenius Structure
• 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

Uses Software

• Quantomatic
• Globular

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)