Rewriting modulo symmetric monoidal structure

DOI10.1145/2933575.2935316zbMATH Open1395.68162arXiv1602.06771OpenAlexW3103260150MaRDI QIDQ4635934FDOQ4635934

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

Publication date: 23 April 2018

Published in: Proceedings of the 31st Annual ACM/IEEE Symposium on Logic in Computer Science (Search for Journal in Brave)

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.

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

Recommendations

• String diagram rewrite theory II: Rewriting with symmetric monoidal structure
• String diagram rewrite theory. I: Rewriting with Frobenius structure
• Rewriting with Frobenius
• String diagram rewrite theory III: Confluence with and without Frobenius
• Open-graphs and monoidal theories

Mathematics Subject Classification ID

Hypergraphs (05C65) Grammars and rewriting systems (68Q42)

Cited In (33)

• Graphical Conjunctive Queries.
• Diagram rewriting and operads
• 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
• Title not available (Why is that?)
• Title not available (Why is that?)
• 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
• Interacting Hopf algebras
• Free gs-monoidal categories and free Markov categories
• Title not available (Why is that?)
• Confluence of graph rewriting with interfaces
• Quantomatic: a proof assistant for diagrammatic reasoning
• Title not available (Why is that?)
• A structural and nominal syntax for diagrams
• A finite presentation of CNOT-dihedral operators
• Bialgebraic foundations for the operational semantics of string diagrams
• Title not available (Why is that?)
• 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
• Pattern graph rewrite systems
• A practical type theory for symmetric monoidal categories
• String diagram rewrite theory III: Confluence with and without Frobenius

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)