Bonchi, Filippo;
Gadducci, Fabio;
Kissinger, Aleks;
Sobocinski, Pawel;
Zanasi, Fabio;
(2022)
String Diagram Rewrite Theory I: Rewriting with Frobenius Structure.
Journal of the ACM
, 69
(2)
, Article 14. 10.1145/3502719.
Preview |
Text
Zanasi_String Diagram Rewrite Theory I. Rewriting with Frobenius Structure_submitted.pdf - Accepted Version Download (1MB) | Preview |
Abstract
String diagrams are a powerful and intuitive graphical syntax, originating in theoretical physics and later formalised in the context of symmetric monoidal categories. In recent 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 several of these proposals, transformations of systems are modelled as rewrite rules of diagrams. These developments require a mathematical foundation for string diagram rewriting: whereas rewrite theory for terms is well-understood, the two-dimensional nature of string diagrams poses quite a few additional challenges. This work systematises and expands a series of recent conference papers, laying down such a foundation. As a first step, we focus on the case of rewrite systems for string diagrammatic theories that feature a Frobenius algebra. This common structure provides a more permissive notion of composition than the usual one available in monoidal categories, and has found many applications in areas such as concurrency, quantum theory, and electrical circuits. Notably, this structure provides an exact correspondence between the syntactic notion of string diagrams modulo Frobenius structure and the combinatorial structure of hypergraphs. Our work introduces a combinatorial interpretation of string diagram rewriting modulo Frobenius structures in terms of double-pushout hypergraph rewriting. We prove this interpretation to be sound and complete and we also show that the approach can be generalised to 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.
| Type: | Article |
|---|---|
| Title: | String Diagram Rewrite Theory I: Rewriting with Frobenius Structure |
| Open access status: | An open access version is available from UCL Discovery |
| DOI: | 10.1145/3502719 |
| Publisher version: | https://doi.org/10.1145/3502719 |
| Language: | English |
| Additional information: | This version is the author accepted manuscript. For information on re-use, please refer to the publisher’s terms and conditions. |
| Keywords: | double-pushout rewriting, category theory, Frobenius algebra, String diagram |
| UCL classification: | UCL > Provost and Vice Provost Offices > UCL BEAMS > Faculty of Engineering Science UCL > Provost and Vice Provost Offices > UCL BEAMS > Faculty of Engineering Science > Dept of Computer Science UCL > Provost and Vice Provost Offices > UCL BEAMS UCL |
| URI: | https://discovery.ucl.ac.uk/id/eprint/10147745 |
Archive Staff Only
 |
View Item |
