This thesis provides an in-depth study of the properties of pseudo-distributive laws, and as one of its applications, 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 Flore et al, and that for linear contexts by Tanaka. The main mathematical result of the thesis is the proof that, given a pseudo-monad <i>S</i> on a 2-category C, the 2-category of pseudo-distributive laws of <i>S</i> over pseudo-endofunctors on C and that of liftings of pseudo-endofunctors on C to the 2-category of the pseudo-algebras of <i>S </i>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 pseudo-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 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 <i>S </i>on <i>Cat, </i>and presheaf categories are given as the cocompletion (partial) pseudo-monad <i>T </i>on <i>Cat, </i>therefore our analysis of pseudo-distributive laws is applied to the combination of a pseudo-monad for contexts with the cocompletion pseudo-monad <i>T. </i>The existence of such pseudo-distributive laws leads to a natural monoidal structure that models substitution. This follows from the second main mathematical result of the thesis, the framework for such monoidal structures, which is given in terms of pseudo-strengths of pseudo-monads on <i>Cat </i>and the monoidal structures induced by them. We first prove that a pseudo-distributive law of <i>S </i>over <i>T </i>renders the composite <i>TS </i>to be again a pseudo-monad, from which it follows that the category <i>TS1 </i>has a monoidal structure, which, in our examples, models the substitution.
| Identifer | oai:union.ndltd.org:bl.uk/oai:ethos.bl.uk:662722 |
| Date | January 2004 |
| Creators | Tanaka, Miki |
| Publisher | University of Edinburgh |
| Source Sets | Ethos UK |
| Detected Language | English |
| Type | Electronic Thesis or Dissertation |
| Source | http://hdl.handle.net/1842/14520 |
Page generated in 0.0026 seconds