String Diagram Rewrite Theory III: Confluence with and without Frobenius

TL;DR

This paper proves that confluence in string diagram rewriting with interfaces is decidable, providing effective methods for local confluence analysis in symmetric monoidal theories, including those with Frobenius structures.

Contribution

It establishes decidability of confluence for DPOI rewriting in string diagrams and introduces path joinability for analyzing critical pairs with non-local constraints.

Findings

Confluence for DPOI rewriting is decidable.

Effective procedures for local confluence analysis are developed.

Path joinability enables handling non-local constraints in symmetric monoidal theories.

Abstract

In this paper we address the problem of proving confluence for string diagram rewriting, which was previously shown to be characterised combinatorically as double-pushout rewriting with interfaces (DPOI) on (labelled) hypergraphs. For standard DPO rewriting without interfaces, confluence for terminating rewrite 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.