Search

# Monoidal Context Theory, PhD Thesis

Last updated Unknown

• Thesis: pdf.
• Supervisor: Pawel Sobocinski.
• Opponents: Guy McCusker and Paul-André Melliès.

Preface
Understanding intelligent systems may be both our greatest achievement or our end, intelligent systems pose an existential risk. Current mathematics is not up for the task of describing complex systems, we resort to impenetrable piles of linear algebra. However, old mathematics does not need to be our strategy, we can advance conceptual understanding. This work is about finding the right languages for process description; it relies on the intuitive description of processes via string diagrams.

The main idea of this thesis is to use monoidal multicategories to study the algebra of monoidal categories, in the same way that multicategories and Lawvere theories are used to study 1-dimensional algebra. Monoidal multicategories are half-representable duoidal categories, and so, we use much of the theory of normalization of duoidal categories. The main unit of a decomposition in a monoidal category is a monoidal context, or a monoidal optic; and we provide for them a universal property: monoidal optics are the free produoidal normalization of the cofree produoidal on a monoidal category.

Chapter 1: Process Theories.
Short exposition on monoidal categories and string diagrams. We talk about the missing string diagrams adjunction and how string diagrams still construct free monoidal categories by reducing an adjunction (precisely, a Quasi 2-adjunction). We comment quickly on string diagrams for bicategories.

As a source of examples, we pick cartesian monoidal categories, but also study what happens when cartesianity fails: partial and stochastic theories. Our running example will be the Kleisli category of the subdistribution monad.

Chapter 2: Context Theory
Our formulation of decomposition is based on two ingredients: profunctors and multicategories. The point of coend calculus is that it gives a canonical notion of connecting processes, that of dinaturality. In fact, this brings us to consider malleable multicategories, a coherent version of multicategories that coincides with promonoidal categories – the category of malleable multicategories is equivalent to the category of promonoidal categories.

The fundamental result we will generalize is the splice-contour adjunction: the contour of a multicategory is left adjoint to the spliced arrows, which form a malleable multicategory.

Chapter 3: Monoidal Context Theory
Duoidal categories have a rich theory, although be careful with duoidal coherence. Garner and Lopez Franco described the normalization of a duoidal category, but only duoidal categories with coequalizers preserved by the parallel tensor can be normalized. Instead, we use the normalization of a produoidal: this one always exists and it induces an idempotent monad. The normalization of the produoidal category of monoidal spliced arrows is the produoidal category of monoidal optics; a non-symmetric version describes the produoidal algebra of monoidal contexts.

Chapter 4: Monoidal Message Passing
Message theories are an axiomatization of basic message passing. We characterize message theories in terms of physical monoidal multicategories. Shuffles form the free physical monoidal multicategory. The free polarized physical monoidal multicategory over some generators is given by polar shuffles. Polar shuffles can be used for deadlock-free message-passing.

Sessions form a message theory, and any message theory induces a symmetric monoidal category.