String Diagram Rewrite Theory I: Rewriting with Frobenius Structure
- 10 March 2022
- journal article
- research article
- Published by Association for Computing Machinery (ACM) in Journal of the ACM
- Vol. 69 (2), 1-58
- https://doi.org/10.1145/3502719
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.Keywords
Funding Information
- Italian MIUR PRIN (2017FTXR7S)
- EPSRC (EP/V002376/1)
- Estonian IT Academy research (2014-2020.4.05.19-0001)
- Estonian Research Council (PRG1210)
This publication has 44 references indexed in Scilit:
- Open Graphs and Computational ReasoningElectronic Proceedings in Theoretical Computer Science, 2010
- Graph rewriting for the π-calculusMathematical Structures in Computer Science, 2007
- The Category Theoretic Understanding of Universal Algebra: Lawvere Theories and MonadsElectronic Notes in Theoretical Computer Science, 2007
- Adhesive and quasiadhesive categoriesRAIRO - Theoretical Informatics and Applications, 2005
- Traced monoidal categoriesMathematical Proceedings of the Cambridge Philosophical Society, 1996
- The geometry of tensor calculus, IAdvances in Mathematics, 1991
- Completion for rewriting modulo a congruenceTheoretical Computer Science, 1989
- Complete Sets of Reductions for Some Equational TheoriesJournal of the ACM, 1981
- Confluent Reductions: Abstract Properties and Applications to Term Rewriting SystemsJournal of the ACM, 1980
- Categorical algebraBulletin of the American Mathematical Society, 1965