Structure and Semantics

TL;DR

This thesis introduces proto-theories as a unifying framework for algebraic theories, generalizes semantics via aritations, and explores a topological extension to achieve desirable categorical properties.

Contribution

It defines proto-theories and aritations, establishing a general semantics framework that encompasses classical algebraic theories and extends monads with better categorical properties.

Findings

Proto-theories unify various algebraic notions.

Semantics functor has an adjoint, enabling structure-semantics correspondence.

Topological proto-theories improve the properties of the semantics functor.

Abstract

There are many category-theoretic notions of algebraic theory, including Lawvere theories, monads, PROPs and operads. The first central notion of this thesis is a common generalisation of these, which we call a proto-theory. In order to define models of a proto-theory in a category, we need a way of relating the arities of the proto-theory with the objects of the category. This leads to our second central notion, that of an interpretation of arities, or aritation for short. We show that every aritation gives rise to a semantics functor sending proto-theories to models. In fact this functor always has an adjoint, giving a structure-semantics adjunction. Furthermore, we show that the semantics of proto-theories generalises the classical semantics of many existing notions of algebraic theory. Another aim of this thesis is to find a convenient category of monads in the following sense. Every right adjoint gives rise to a monad on its codomain, and more generally so does any functor that admits a codensity monad. However, not all functors have codensity monads. This means that the semantics functor for monads on a category, viewed as a functor into the category of all functors into the base category, does not have a left adjoint. We seek a generalisation of monads with a semantics functor that does have a left adjoint. This can be accomplished with proto-theories, but at a cost. The classical semantics functor for monads is full and faithful; this is a kind of completeness theorem, and is highly desirable in a notion of algebraic theory. However, the semantics functor for general proto-theories is not full and faithful. Thus we seek a generalisation of monads and their semantics for which the semantics functor is both full and faithful and has a left adjoint. We show that such a generalisation is given, for suitable base categories, by a certain kind of topological proto-theory.