{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,3,19]],"date-time":"2026-03-19T06:24:36Z","timestamp":1773901476459,"version":"3.50.1"},"reference-count":49,"publisher":"Cambridge University Press (CUP)","issue":"7","license":[{"start":{"date-parts":[[2022,6,13]],"date-time":"2022-06-13T00:00:00Z","timestamp":1655078400000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/creativecommons.org\/licenses\/by-nc-sa\/4.0\/"}],"content-domain":{"domain":["cambridge.org"],"crossmark-restriction":true},"short-container-title":["Math. Struct. Comp. Sci."],"published-print":{"date-parts":[[2022,8]]},"abstract":"<jats:title>Abstract<\/jats:title><jats:p>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, <jats:italic>is<\/jats:italic> 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.<\/jats:p>","DOI":"10.1017\/s0960129522000123","type":"journal-article","created":{"date-parts":[[2022,6,13]],"date-time":"2022-06-13T19:35:27Z","timestamp":1655148927000},"page":"829-869","update-policy":"https:\/\/doi.org\/10.1017\/policypage","source":"Crossref","is-referenced-by-count":8,"title":["String diagram rewrite theory III: Confluence with and without Frobenius"],"prefix":"10.1017","volume":"32","author":[{"given":"Filippo","family":"Bonchi","sequence":"first","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0003-0690-3051","authenticated-orcid":false,"given":"Fabio","family":"Gadducci","sequence":"additional","affiliation":[]},{"given":"Aleks","family":"Kissinger","sequence":"additional","affiliation":[]},{"given":"Pawe\u0142","family":"Soboci\u0144ski","sequence":"additional","affiliation":[]},{"given":"Fabio","family":"Zanasi","sequence":"additional","affiliation":[]}],"member":"56","published-online":{"date-parts":[[2022,6,13]]},"reference":[{"key":"S0960129522000123_ref43","doi-asserted-by":"publisher","DOI":"10.1016\/j.ic.2013.03.007"},{"key":"S0960129522000123_ref9","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-44584-6_30"},{"key":"S0960129522000123_ref3","doi-asserted-by":"publisher","DOI":"10.1007\/BF00271645"},{"key":"S0960129522000123_ref48","unstructured":"Soboci\u0144ski, P. (2004). Deriving Process Congruences from Reaction Rules. PhD thesis, BRICS, University of Aarhus."},{"key":"S0960129522000123_ref16","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.2012.35"},{"key":"S0960129522000123_ref39","doi-asserted-by":"publisher","DOI":"10.1090\/S0002-9904-1965-11234-4"},{"key":"S0960129522000123_ref4","doi-asserted-by":"publisher","DOI":"10.1145\/2933575.2935316"},{"key":"S0960129522000123_ref34","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-21401-6_22"},{"key":"S0960129522000123_ref44","unstructured":"Plump, D. (1993). Hypergraph rewriting: Critical pairs and undecidability of confluence. In: Sleep, M. R., Plasmeijer, M. J. and van Eekele, M. C. J. D. (eds.) Term Graph Rewriting: Theory and Practice. Wiley, 201\u2013213."},{"key":"S0960129522000123_ref23","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-07854-1_188"},{"key":"S0960129522000123_ref13","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-23217-6_21"},{"key":"S0960129522000123_ref25","doi-asserted-by":"publisher","DOI":"10.1145\/2933575.2934556"},{"key":"S0960129522000123_ref28","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-38164-5_5"},{"key":"S0960129522000123_ref47","first-page":"289","article-title":"A survey of graphical languages for monoidal categories","volume":"13","author":"Selinger","year":"2011","journal-title":"Springer Lecture Notes in Physics"},{"key":"S0960129522000123_ref32","doi-asserted-by":"publisher","DOI":"10.1017\/S0305004100074338"},{"key":"S0960129522000123_ref18","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-75396-6_1"},{"key":"S0960129522000123_ref27","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-64299-4_36"},{"key":"S0960129522000123_ref1","first-page":"836","article-title":"Categories in control","volume":"30","author":"Baez","year":"2015","journal-title":"Theory and Application of Categories"},{"key":"S0960129522000123_ref15","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-70583-3_25"},{"key":"S0960129522000123_ref21","doi-asserted-by":"crossref","unstructured":"Ehrig, H. , Habel, A. , Padberg, J. and Prange, U. (2004). Adhesive high-level replacement categories and systems. In: Ehrig, H., Engels, G., Parisi-Presicce, F. and Rozenberg, G. (eds.) ICGT 2004, vol. 2987. LNCS. Springer, 144\u2013160, 2004.","DOI":"10.1007\/978-3-540-30203-2_12"},{"key":"S0960129522000123_ref24","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-38164-5_4"},{"key":"S0960129522000123_ref35","volume-title":"Computational Problems in Abstract Algebra","author":"Knuth","year":"1970"},{"key":"S0960129522000123_ref45","unstructured":"Plump, D. (2010). Checking graph-transformation systems for confluence. In: Drewes, F., Habel, A., Hoffmann, B. and Plump, D. (eds.), Manipulation of Graphs, Algebras and Pictures, vol. 26. ECEASST. EASST."},{"key":"S0960129522000123_ref6","unstructured":"Bonchi, F. , Gadducci, F. , Kissinger, A. , Soboci\u0144ski, P. and Zanasi, F. (2020). String diagram rewrite theory II: Rewriting with symmetric monoidal structure. Preprint available at arXiv:2104.14686."},{"key":"S0960129522000123_ref8","doi-asserted-by":"publisher","DOI":"10.1016\/j.ic.2008.10.005"},{"key":"S0960129522000123_ref5","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-54434-1_6"},{"key":"S0960129522000123_ref49","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-07734-5_9"},{"key":"S0960129522000123_ref7","doi-asserted-by":"publisher","DOI":"10.1145\/3502719"},{"key":"S0960129522000123_ref38","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-51372-6_7"},{"key":"S0960129522000123_ref31","doi-asserted-by":"publisher","DOI":"10.1016\/j.entcs.2007.02.019"},{"key":"S0960129522000123_ref37","doi-asserted-by":"publisher","DOI":"10.1016\/S0022-4049(03)00069-0"},{"key":"S0960129522000123_ref42","doi-asserted-by":"publisher","DOI":"10.1007\/BFb0022525"},{"key":"S0960129522000123_ref10","doi-asserted-by":"publisher","DOI":"10.1145\/2676726.2676993"},{"key":"S0960129522000123_ref40","unstructured":"Mimram, S. (2010). Computing critical pairs in 2-dimensional rewriting systems. In: Lynch, C. (ed.) RTA 2010, vol. 6. LIPIcs. Schloss Dagstuhl - Leibniz-Zentrum f\u00fcr Informatik, 227\u2013242."},{"key":"S0960129522000123_ref20","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-15928-2_22"},{"key":"S0960129522000123_ref33","doi-asserted-by":"publisher","DOI":"10.1016\/0890-5401(90)90023-B"},{"key":"S0960129522000123_ref14","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-51372-6_2"},{"key":"S0960129522000123_ref46","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.2005.40"},{"key":"S0960129522000123_ref36","doi-asserted-by":"publisher","DOI":"10.1051\/ita:2005028"},{"key":"S0960129522000123_ref41","doi-asserted-by":"publisher","DOI":"10.2168\/LMCS-10(2:1)2014"},{"key":"S0960129522000123_ref19","doi-asserted-by":"crossref","unstructured":"Ehrig, H. (1978). Introduction to the algebraic theory of graph grammars (A survey). In: Claus, V., Ehrig, H. and Rozenberg, G. (eds.) Graph-Grammars and Their Application to Computer Science and Biology, vol. 73. LNCS. Springer, 1\u201369.","DOI":"10.1007\/BFb0025714"},{"key":"S0960129522000123_ref17","doi-asserted-by":"crossref","unstructured":"Corradini, A. (2016). On the definition of parallel independence in the algebraic approaches to graph transformation. In: Milazzo, P., Varr\u00f3, D. and Wimmer, M. (eds.) STAF 2016, vol. 9946. LNCS. Springer.","DOI":"10.1007\/978-3-319-50230-4_8"},{"key":"S0960129522000123_ref26","doi-asserted-by":"publisher","DOI":"10.1017\/S096012950700610X"},{"key":"S0960129522000123_ref12","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2006.07.005"},{"key":"S0960129522000123_ref30","unstructured":"Huet, G. and Lankford, D. (1978). On the uniform halting problem for term rewriting systems. Technical Report 283, IRIA."},{"key":"S0960129522000123_ref2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-22993-0_8"},{"key":"S0960129522000123_ref22","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-24727-2_12"},{"key":"S0960129522000123_ref11","unstructured":"Sander Bruggink, H. J. , Cauderlier, R. , H\u00fclsbusch, M. and K\u00f6nig, B. (2011). Conditional reactive systems. In: Chakraborty, S. and Kumar, A. (eds.) FSTTCS 2011, vol. 13. LIPIcs. Schloss Dagstuhl - Leibniz-Zentrum f\u00fcr Informatik, 191\u2013203."},{"key":"S0960129522000123_ref29","doi-asserted-by":"publisher","DOI":"10.1017\/S0960129501003425"}],"container-title":["Mathematical Structures in Computer Science"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/www.cambridge.org\/core\/services\/aop-cambridge-core\/content\/view\/S0960129522000123","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,2,22]],"date-time":"2023-02-22T08:15:50Z","timestamp":1677053750000},"score":1,"resource":{"primary":{"URL":"https:\/\/www.cambridge.org\/core\/product\/identifier\/S0960129522000123\/type\/journal_article"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2022,6,13]]},"references-count":49,"journal-issue":{"issue":"7","published-print":{"date-parts":[[2022,8]]}},"alternative-id":["S0960129522000123"],"URL":"https:\/\/doi.org\/10.1017\/s0960129522000123","relation":{},"ISSN":["0960-1295","1469-8072"],"issn-type":[{"value":"0960-1295","type":"print"},{"value":"1469-8072","type":"electronic"}],"subject":[],"published":{"date-parts":[[2022,6,13]]},"assertion":[{"value":"\u00a9 The Author(s), 2022. Published by Cambridge University Press","name":"copyright","label":"Copyright","group":{"name":"copyright_and_licensing","label":"Copyright and Licensing"}},{"value":"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\/), which permits non-commercial re-use, distribution, and reproduction in any medium, provided the same Creative Commons licence is used to distribute the re-used or adapted article and the original article is properly cited. The written permission of Cambridge University Press must be obtained prior to any commercial use.","name":"license","label":"License","group":{"name":"copyright_and_licensing","label":"Copyright and Licensing"}},{"value":"This content has been made available to all.","name":"free","label":"Free to read"}]}}