The Produoidal Algebra of Process Decomposition

TL;DR

This paper introduces a new algebraic framework called the normal produoidal category of monoidal contexts, which models incomplete processes and aids in analyzing multi-party interaction protocols across various process theories.

Contribution

It defines the normal produoidal category of monoidal contexts, characterizes them via universal properties, and connects symmetric monoidal contexts with monoidal lenses for protocol analysis.

Findings

Monoidal contexts represent incomplete processes with missing parts.

Symmetric monoidal contexts are equivalent to monoidal lenses.

The framework applies to multi-party interaction protocols.

Abstract

We introduce the normal produoidal category of monoidal contexts over an arbitrary monoidal category. In the same sense that a monoidal morphism represents a process, a monoidal context represents an incomplete process: a piece of a decomposition, possibly containing missing parts. We characterize monoidal contexts in terms of universal properties. In particular, symmetric monoidal contexts coincide with monoidal lenses, endowing them with a novel universal property. We apply this algebraic structure to the analysis of multi-party interaction protocols in arbitrary theories of processes.