George Kaye: Diagrammatic Semantics with Symmetric Traced Monoidal Categories

Abstract

String diagrams are becoming the established mathematical language of diagrammatic reasoning, with the mantra of ‘only connectivity matters’: equal terms are represented as isomorphic (or isotopic) diagrams. Unfortunately, when adding more structure to categories in the form of additional axioms, this mantra is lost: we must now consider diagrams up to rewriting. To perform these rewrites, we are required to move from topological to combinatorial languages: this has been studied recently using framed point graphs and hypergraphs. However, these approaches have been rooted in the setting of compact closed categories, which have a flexible notion of causality where any two ports can join provided the types match. Conversely, systems with a strict notion of input-output connectivity (such as digital circuits) require a different kind of categorical setting, namely that of a symmetric traced monoidal category (STMC). While one can construct a trace from a compact closed setting, this can lead to degenerate terms in certain settings, such as when we have finite products.

We therefore introduce a variant of hypergraphs that we call ‘interfaced linear hypergraphs’, designed specifically for STMCs. This language is sound and complete – any morphism in the STMC can be interpreted as a well-formed interfaced linear hypergraph up to isomorphism, and any interfaced linear hypergraph is the representation of a unique morphism, up to the equational theory of the category. We can then express the axioms of our monoidal theory as graph rewrite rules – we show how we can use our graphical language to apply the framework of double pushout (DPO) rewriting to act as a graph rewriting diagrammatic semantics.

Slides: https://www.georgejkaye.com/pages/talks/2021-03-04-huawei.pdf

Video: https://youtu.be/UbTke5d2-Xs

Full paper: https://arxiv.org/abs/2010.06319