String Diagram Rewrite Theory I: Rewriting with Frobenius Structure
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.