*Abstract:*

This thesis provides an in-depth study of the
properties of pseudo-distributive laws motivated by the search for
a unified framework to model substitution and variable binding for
various different types of contexts; in particular, the
construction presented in this thesis for modelling substitution
unifies that for cartesian contexts as in the work by Fiore *et
al* and that for linear contexts by Tanaka.

The main mathematical result of the thesis is
the proof that, given a pseudo-monad *S* on a 2-category
*C*, the 2-category of pseudo-distributive laws of *S*
over pseudo-endofunctors on *C* and that of liftings of
pseudo-endofunctors on *C* to the 2-category of the
pseudo-algebras of *S* are equivalent. The proof for the
non-pseudo case, *i.e.*, a version for ordinary categories and
monads, is given in detail as a prelude to the proof of the
pseudo-case, followed by some investigation into the relation
between distributive laws and Kleisli categories. Our analysis of
distributive laws is then extended to pseudo-distributivity over
pseudo-endofunctors and over pseudo-natural transformations and
modifications. The natural bimonoidal structures on the 2-category
of pseudo-distributive laws and that of (pseudo)-liftings are also
investigated as part of the proof of the equivalence.

Fiore *et al* and Tanaka take the free
cocartesian category on 1 and the free symmetric monoidal category
on 1 respectively as a category of contexts and then consider its
presheaf category to construct abstract models for binding and
substitution. In this thesis a model for substitution that unifies
these two and other variations is constructed by using the presheaf
category on a small category with structure that models contexts.
Such structures for contexts are given as pseudo-monads *S* on
*Cat*, and presheaf categories are given as the free
cocompletion (partial) pseudo-monad *T* on *Cat*,
therefore our analysis of pseudo-distributive laws is applied to
the combination of a pseudo-monad for contexts with the
cocompletion pseudo-monad *T*. The existence of such
pseudo-distributive laws leads to a natural monoidal structure that
is used to model substitution. We prove that a pseudo-distributive
law of *S* over *T* results in the composite *TS*
again being a pseudo-monad, from which it follows that the category
*TS*1 has a monoidal structure, which, in our examples, models
substitution.

This is a 167-page thesis.

This report is available in the following formats:

Previous | Index