Bonchi, Filippo;
Gadducci, Fabio;
Kissinger, Aleks;
Sobocinski, Pawel;
Zanasi, Fabio;
(2022)
String diagram rewrite theory III: Confluence with and without Frobenius.
Mathematical Structures in Computer Science
10.1017/S0960129522000123.
(In press).
Preview |
Text
string-diagram-rewrite-theory-iii-confluence-with-and-without-frobenius.pdf - Published Version Download (3MB) | Preview |
Abstract
In this paper, we address the problem of proving confluence for string diagram rewriting, which was previously shown to be characterised combinatorially as double-pushout rewriting with interfaces (DPOI) on (labelled) hypergraphs. For standard DPO rewriting without interfaces, confluence for terminating rewriting systems is, in general, undecidable. Nevertheless, we show here that confluence for DPOI, and hence string diagram rewriting, is decidable. We apply this result to give effective procedures for deciding local confluence of symmetric monoidal theories with and without Frobenius structure by critical pair analysis. For the latter, we introduce the new notion of path joinability for critical pairs, which enables finitely many joins of a critical pair to be lifted to an arbitrary context in spite of the strong non-local constraints placed on rewriting in a generic symmetric monoidal theory.
| Type: | Article |
|---|---|
| Title: | String diagram rewrite theory III: Confluence with and without Frobenius |
| Open access status: | An open access version is available from UCL Discovery |
| DOI: | 10.1017/S0960129522000123 |
| Publisher version: | https://doi.org/10.1017/S0960129522000123 |
| Language: | English |
| Additional information: | © The Author(s), 2022. Published by Cambridge University Press. This is an Open Access article, distributed under the terms of the Creative Commons Attribution-NonCommercial-ShareAlike licence (http://creativecommons.org/licenses/by-nc-sa/4.0/). |
| Keywords: | String diagram, symmetric monoidal category, double-pushout rewriting, confluence |
| 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/10151067 |
Archive Staff Only
 |
View Item |
