Bialgebraic Semantics for String Diagrams

TL;DR

This paper applies bialgebraic semantics to string diagrams, providing a compositional and well-behaved operational semantics that unify different interpretations and synchronization mechanisms across disciplines.

Contribution

It introduces a bialgebraic framework for the semantics of string diagrams, enabling compositional analysis and linking different process interpretations.

Findings

Bialgebraic semantics for string diagrams are well-behaved and compositional.

The approach unifies different synchronization mechanisms in process theories.

Provides semantics for models like signal flow graphs and Petri nets.

Abstract

Turi and Plotkin's bialgebraic semantics is an abstract approach to specifying the operational semantics of a system, by means of a distributive law between its syntax (encoded as a monad) and its dynamics (an endofunctor). This setup is instrumental in showing that a semantic specification (a coalgebra) satisfies desirable properties: in particular, that it is compositional. In this work, we use the bialgebraic approach to derive well-behaved structural operational semantics of string diagrams, a graphical syntax that is increasingly used in the study of interacting systems across different disciplines. Our analysis relies on representing the two-dimensional operations underlying string diagrams in various categories as a monad, and their bialgebraic semantics in terms of a distributive law over that monad. As a proof of concept, we provide bialgebraic compositional semantics for a versatile string diagrammatic language which has been used to model both signal flow graphs (control theory) and Petri nets (concurrency theory). Moreover, our approach reveals a correspondence between two different interpretations of the Frobenius equations on string diagrams and two synchronisation mechanisms for processes, \`a la Hoare and \`a la Milner.