Equational reasoning with context-free families of string diagrams

TL;DR

This paper introduces B-ESG grammars, a new class of context-free grammars for defining and reasoning about entire families of string diagrams and their rewrite rules, enabling mechanised equational reasoning.

Contribution

It defines B-ESG grammars for representing families of string graphs and their rewrite rules, and proves decidability of key problems, facilitating automated reasoning at the grammar level.

Findings

Decidability of language-membership for B-ESG grammars

Decidability of match-enumeration problems

Algorithm for rewriting string graphs using B-ESG patterns

Abstract

String diagrams provide an intuitive language for expressing networks of interacting processes graphically. A discrete representation of string diagrams, called string graphs, allows for mechanised equational reasoning by double-pushout rewriting. However, one often wishes to express not just single equations, but entire families of equations between diagrams of arbitrary size. To do this we define a class of context-free grammars, called B-ESG grammars, that are suitable for defining entire families of string graphs, and crucially, of string graph rewrite rules. We show that the language-membership and match-enumeration problems are decidable for these grammars, and hence that there is an algorithm for rewriting string graphs according to B-ESG rewrite patterns. We also show that it is possible to reason at the level of grammars by providing a simple method for transforming a grammar by string graph rewriting, and showing admissibility of the induced B-ESG rewrite pattern.