Huawei Edinburgh PL Tech Talk - Diagrammatic Semantics with Symmetric Traced Monoidal Categories

Talk date: 04/03/2021
Venue: Huawei Edinburgh Programming Languages Group Tech Talk
Link: https://blogs.ed.ac.uk/he-lab/categor...

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.