String Diagram Rewrite Theory I: Rewriting with Frobenius Structure
Preprint
Abstract
String diagrams are a powerful and intuitive graphical syntax, originated in the study of symmetric monoidal categories. In the last few years, they have found application in the modelling of various computational structures, in fields as diverse as Computer Science, Physics, Control Theory, Linguistics, and Biology. In many such proposals, the transformations of the described systems are modelled as rewrite rules of diagrams. These developments demand a mathematical foundation for string diagram rewriting: whereas rewrite theory for terms is well-understood, the two-dimensional nature of string diagrams poses additional challenges. This work systematises and expands a series of recent conference papers laying down such foundation. As first step, we focus on the case of rewrite systems for string diagrammatic theories which feature a Frobenius algebra. This situation ubiquitously appear in various approaches: for instance, in the algebraic semantics of linear dynamical systems, Frobenius structures model the wiring of circuits; in categorical quantum mechanics, they model interacting quantum observables. Our work introduces a combinatorial interpretation of string diagram rewriting modulo Frobenius structures, in terms of double-pushout hypergraph rewriting. Furthermore, we prove this interpretation to be sound and complete. In the last part, we also see that the approach can be generalised to model rewriting modulo multiple Frobenius structures. As a proof of concept, we show how to derive from these results a termination strategy for Interacting Bialgebras, an important rewrite theory in the study of quantum circuits and signal flow graphs.Keywords
All Related Versions
This publication has 23 references indexed in Scilit:
- The Calculus of Signal Flow Diagrams I: Linear relations on streamsInformation and Computation, 2017
- Interacting Hopf algebrasJournal of Pure and Applied Algebra, 2017
- Quantomatic: A Proof Assistant for Diagrammatic Reasoning2015
- A Categorical Semantics of Signal Flow Graphs2014
- Interacting Bialgebras Are Frobenius2014
- Synthesising CCS bisimulation using graph rewritingInformation and Computation, 2009
- Deriving Bisimulation Congruences in the DPO Approach to Graph Rewriting2004
- An inductive view of graph transformationLecture Notes in Computer Science, 1998
- Higher-dimensional word problems with applications to equational logicTheoretical Computer Science, 1993
- Completion for rewriting modulo a congruenceTheoretical Computer Science, 1989