Monoidal Context Theory

TL;DR

The work develops a universal category-theoretic framework for monoidal context and message passing by characterizing monoidal lenses as a normalization of a cofree produoidal structure on monoidal spliced arrows. It builds a layered hierarchy—duoidal and normal duoidal categories, promonoidal/malleable multicategories, and the splice-contour adjunction—to model contexts, incomplete processes, and global effects, culminating in a producing/decomposing (produoidal) view of monoidal categories. Central results include a universal characterization of monoidal contexts as a normalization (Theorem) and an adjunction between sessions and processes that captures multi-party message passing. The framework unifies symmetric monoidal do-notation, premonoidal reasoning with runtime, and a minimalistic notion of message theory, enabling robust reasoning about distributed, effectful, and probabilistic processes across classical and quantum settings. This provides a foundational, compositional toolkit for analyzing process decomposition, context wiring, and communication protocols in a broad spectrum of computational models.

Abstract

We universally characterize the produoidal category of monoidal lenses over a monoidal category. In the same way that each category induces a cofree promonoidal category of spliced arrows, each monoidal category induces a cofree produoidal category of monoidal spliced arrows; monoidal lenses are the free normalization of the cofree produoidal category of monoidal spliced arrows. We apply the characterization of symmetric monoidal lenses to the analysis of multi-party message-passing protocols. We introduce a minimalistic axiomatization of message passing -- message theories -- and we construct combinatorially the free message theory over a set. Symmetric monoidal lenses are the derivations of the free message theory over a symmetric monoidal category.

Figures (111)

• Figure 1: String-diagrammatic correctness proof for the One-time pad protocol (\ref{['prop:correctness']}, broadbent22:crypto).
• Figure 2: A depiction of monoidal lenses, or incomplete processes.
• Figure 3: Type-theoretic presentation of a message theory.
• Figure 4: One-time pad protocol, split in four actors, mixed with a shuffle.
• Figure 5: Chapter dependencies.

Theorems & Definitions (305)

• Definition 1.1.1
• Remark 1.1.2: Process theories
• Definition 1.1.3
• Definition 1.1.4
• Remark 1.1.5
• Proposition 1.1.6
• proof
• Definition 1.1.7
• Definition 1.1.8
• Definition 1.1.9