String diagram rewrite theory II: rewriting with symmetric monoidal structure
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 <i>string diagrams</i>, topological enti...
| Main Authors: | , , , , |
|---|---|
| Format: | Journal article |
| Language: | English |
| Published: |
Cambridge University Press
2022
|
| _version_ | 1797110962875006976 |
|---|---|
| author | Bonchi, F Gadducci, F Kissinger, A Sobocinski, P Zanasi, F |
| author_facet | Bonchi, F Gadducci, F Kissinger, A Sobocinski, P Zanasi, F |
| author_sort | Bonchi, F |
| collection | OXFORD |
| description | 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 <i>string diagrams</i>, topological entities that can be intuitively thought of 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 <i>rewriting rules</i>. 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 <i>Frobenius algebra</i> 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 <i>convex</i>) is identified. As proof of concept, we use our approach to show termination of two SMTs of interest: Frobenius semi-algebras and bialgebras. |
| first_indexed | 2024-03-07T08:02:00Z |
| format | Journal article |
| id | oxford-uuid:5bf7e2ad-4107-488f-b883-0cf5e14964f1 |
| institution | University of Oxford |
| language | English |
| last_indexed | 2024-03-07T08:02:00Z |
| publishDate | 2022 |
| publisher | Cambridge University Press |
| record_format | dspace |
| spelling | oxford-uuid:5bf7e2ad-4107-488f-b883-0cf5e14964f12023-10-09T13:49:44ZString diagram rewrite theory II: rewriting with symmetric monoidal structureJournal articlehttp://purl.org/coar/resource_type/c_dcae04bcuuid:5bf7e2ad-4107-488f-b883-0cf5e14964f1EnglishSymplectic ElementsCambridge University Press2022Bonchi, FGadducci, FKissinger, ASobocinski, PZanasi, FSymmetric 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 <i>string diagrams</i>, topological entities that can be intuitively thought of 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 <i>rewriting rules</i>. 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 <i>Frobenius algebra</i> 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 <i>convex</i>) is identified. As proof of concept, we use our approach to show termination of two SMTs of interest: Frobenius semi-algebras and bialgebras. |
| spellingShingle | Bonchi, F Gadducci, F Kissinger, A Sobocinski, P Zanasi, F String diagram rewrite theory II: rewriting with symmetric monoidal structure |
| title | String diagram rewrite theory II: rewriting with symmetric monoidal structure |
| title_full | String diagram rewrite theory II: rewriting with symmetric monoidal structure |
| title_fullStr | String diagram rewrite theory II: rewriting with symmetric monoidal structure |
| title_full_unstemmed | String diagram rewrite theory II: rewriting with symmetric monoidal structure |
| title_short | String diagram rewrite theory II: rewriting with symmetric monoidal structure |
| title_sort | string diagram rewrite theory ii rewriting with symmetric monoidal structure |
| work_keys_str_mv | AT bonchif stringdiagramrewritetheoryiirewritingwithsymmetricmonoidalstructure AT gadduccif stringdiagramrewritetheoryiirewritingwithsymmetricmonoidalstructure AT kissingera stringdiagramrewritetheoryiirewritingwithsymmetricmonoidalstructure AT sobocinskip stringdiagramrewritetheoryiirewritingwithsymmetricmonoidalstructure AT zanasif stringdiagramrewritetheoryiirewritingwithsymmetricmonoidalstructure |