diff --git a/thesis/bib.bib b/thesis/bib.bib index dde4d9e..7a694fc 100644 --- a/thesis/bib.bib +++ b/thesis/bib.bib @@ -39,6 +39,28 @@ journal = {Logical Methods in Computer Science} } +@inproceedings{Lane1971, + title = {Categories for the Working Mathematician}, + author = {Saunders Mac Lane}, + year = {1971}, + url = {https://api.semanticscholar.org/CorpusID:122892655} +} + + @article{moggi, + title = {Notions of computation and monads}, + journal = {Information and Computation}, + volume = {93}, + number = {1}, + pages = {55-92}, + year = {1991}, + note = {Selections from 1989 IEEE Symposium on Logic in Computer Science}, + issn = {0890-5401}, + doi = {https://doi.org/10.1016/0890-5401(91)90052-4}, + url = {https://www.sciencedirect.com/science/article/pii/0890540191900524}, + author = {Eugenio Moggi}, + abstract = {The λ-calculus is considered a useful mathematical tool in the study of programming languages, since programs can be identified with λ-terms. However, if one goes further and uses βη-conversion to prove equivalence of programs, then a gross simplification is introduced (programs are identified with total functions from values to values) that may jeopardise the applicability of theoretical results. In this paper we introduce calculi, based on a categorical semantics for computations, that provide a correct basis for proving equivalence of programs for a wide range of notions of computation.} +} + @inproceedings{uni-elgot2021, doi = {10.4230/LIPICS.ICALP.2021.131}, url = {https://drops.dagstuhl.de/opus/volltexte/2021/14200/}, @@ -49,4 +71,4 @@ publisher = {Schloss Dagstuhl - Leibniz-Zentrum für Informatik}, year = {2021}, copyright = {Creative Commons Attribution 4.0 International license} -} +} \ No newline at end of file diff --git a/thesis/main.tex b/thesis/main.tex index 6a5387d..42b51f7 100644 --- a/thesis/main.tex +++ b/thesis/main.tex @@ -34,6 +34,8 @@ \chaptermark{#1}% \addcontentsline{toc}{chapter}{#1}} +\newcommand\C{\mathcal{C}} + \declaretheorem[name=Definition,style=definition,numberwithin=chapter]{definition} \declaretheorem[name=Example,style=definition,sibling=definition]{example} \declaretheorem[style=definition,numbered=no]{exercise} diff --git a/thesis/src/01_preliminaries.tex b/thesis/src/01_preliminaries.tex index 0c2fc92..db596ea 100644 --- a/thesis/src/01_preliminaries.tex +++ b/thesis/src/01_preliminaries.tex @@ -1,4 +1,37 @@ \chapter{Preliminaries} +We assume familiarity with basic concepts of category theory that should be taught in any introductory course, or can be looked up in~\cite{Lane1971}. In particular we will need the notions of category, functor, functor algebra, natural transformation, product and coproduct. + +In the rest of this section we will look at other categorical notions that are either less well-known, or crucial for this thesis and therefore require special attention. + \section{Stable Natural Numbers Object} + \section{Extensive and Distributive Categories} -\section{Strong and Commutative Monads} \ No newline at end of file + +\section{Monads} +Monads are widely known among programmers as a way of modelling effects in pure languages. Categorically a Monad is a monoid in the category of endofunctors of a category, or in more accessible terms: + +\begin{definition}[Monad~\cite{Lane1971}] + A monad on a category $\C$ is a triple $(F, \eta, \mu)$, where $F : \C \rightarrow \C$ is an endofunctor and $\eta : Id \rightarrow F, \mu : F^2 \rightarrow F$ are natural transformations, satisfying the following laws: + \begin{enumerate} + % TODO add quantifiers + \item $\mu_X \circ \mu_{FX} = \mu_X \circ F\mu_X$ + \item $\mu_X \circ \eta_{FX} = id_{FX}$ + \item $\mu_X \circ F\eta_X = id_{FX}$ + \end{enumerate} +\end{definition} + +For programmers a second equivalent definition is more useful: + +\begin{definition}[Kleisli triple~\cite{moggi}] + A kleisli triple on a category $\C$ is a triple $(F, \eta, _*)$, where $F : \vert \C \vert \rightarrow \vert \C \vert$ is a mapping on objects, $(\eta_X : X \rightarrow FX)_{X\in\vert\C\vert}$ is a family of morphisms and for every morphism $f : X \rightarrow FY$ there exists a morphism $f^* : FX \rightarrow FY$ called the kleisli lifting. With the following laws: + \begin{enumerate} + % TODO add quantifiers + \item $\eta_X^* = id_{FX}$ + \item $\eta_X \circ f^* = f$ + \item $f^* \circ g* = (f \circ g^*)^*$ + \end{enumerate} +\end{definition} + +% todo change moggi citation to manes, once I got the original +\begin{theorem}[\cite{moggi}] The notions of Kleisli triple and monad are equivalent. +\end{theorem} \ No newline at end of file