Monoidal Context Theory, PhD Thesis
- Document (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.