Rewriting Modulo Symmetric Monoidal Structure

Abstract

String diagrams are an elegant, convenient and powerful syntax for arrows of symmetric monoidal categories. In recent years, they have been used as compositional descriptions of computational systems from various fields, including quantum foundations, linear algebra, control theory, automata theory, concurrency theory, and even linguistics. All of these applications rely on diagrammatic reasoning, which is to string diagrams as equational reasoning is to ordinary terms.

If we are to take string diagrams out of research papers and into practical applications, we need understand how to implement diagrammatic reasoning. This is the focus of my talk.

There is a tight correspondence between symmetric monoidal categories where every object has a coherent special Frobenius algebra structure and categories of cospans of hypergraphs. This correspondence, therefore, takes us from a topological understanding of string diagrams to a combinatorial data-structure-like description. Moreover, diagrammatic reasoning translates via this correspondence exactly to DPO rewriting with interfaces.

The obvious follow-up question is: how much of this correspondence survives if we drop the assumption about Frobenius structure? Can we use this correspondence to implement diagrammatic reasoning on vanilla symmetric monoidal categories? The answer is yes, but we need to restrict the kinds of cospans we consider: the underlying hypergraph has to be acyclic and satisfy an additional condition called monogamy. Moreover, we must restrict the DPO rewriting mechanism to a variant that we call convex DPO rewriting. The good news is that none of these modifications come with a significant algorithmic cost.

The material in this talk is joint work with Filippo Bonchi, Fabio Gadducci, Aleks Kissinger and Fabio Zanasi, and has been published in a series of papers:

  • “Rewriting modulo symmetric monoidal structure”, Proceedings of LiCS 2016 - “Confluence of Graph Rewriting with Interfaces”, Proceedings of ESOP 2017 - “Rewriting with Frobenius”, Proceedings of LiCS 2018

Date
Friday, April 23, 2021 15:00 Europe/Paris
Event
GReTA seminar


Paweł Sobociński
Paweł Sobociński
Professor of Trustworthy Software Technologies

I am Professor of Trustworthy Software Technologies at Taltech. The position is a research measure of the IT Academy programme, funded by the Estonian State and the European Social Fund. I lead the Laboratory for Compositional Systems and Methods.
My research can be understood as the study of how to connect open systems (of various kinds: programs, networks, computing devices, circuits, …) in a way that the description of the connections–i.e. the language that we describe subsystems and how to compose them—is compatible with the behaviour of the system. Therefore, what can be observed of the global system is entirely derivable from the observations made of the component subsystems. This is because each composition operation in the language we use for describing systems gives rise to an analogous operation on the behaviours. This property is known as compositionality.
I focus on compositional modelling of systems, developing the underlying mathematics (usually category theory), and applying it to real-life problems such as verification. I work on graph transformation, Petri nets, process algebras, dynamical and cyberphysical systems, as well as mainstream concurrent programming. Since 2015, I write the Graphical Linear Algebra blog about rediscovering linear algebra in a compositional way, with string diagrams.