From 205480d314afb43bbd31870d17d5c1cdaf773ef0 Mon Sep 17 00:00:00 2001 From: Leon Vatthauer Date: Fri, 9 Feb 2024 13:27:14 +0100 Subject: [PATCH] some prose, remove subtitle --- thesis/bib.bib | 2 +- thesis/main.tex | 10 ++-- thesis/src/01_preliminaries.tex | 26 +++++------ thesis/src/03_partiality-monads.tex | 72 +++++++++++++++++++---------- thesis/src/05_setoids.tex | 2 +- thesis/src/titlepage.tex | 8 ++-- 6 files changed, 73 insertions(+), 47 deletions(-) diff --git a/thesis/bib.bib b/thesis/bib.bib index e999f20..055cb6c 100644 --- a/thesis/bib.bib +++ b/thesis/bib.bib @@ -186,7 +186,7 @@ doi = {10.1016/S0304-3975(02)00728-4}, abstract = {Infinite trees form a free completely iterative theory over any given signature--this fact, proved by Elgot, Bloom and Tindell, turns out to be a special case of a much more general categorical result exhibited in the present paper. We prove that whenever an endofunctor H of a category has final coalgebras for all functors H(-) + X, then those coalgebras, TX, form a monad. This monad is completely iterative, i.e., every guarded system of recursive equations has a unique solution. And it is a free completely iterative monad on H. The special case of polynomial endofunctors of the category Set is the above mentioned theory, or monad, of infinite trees.This procedure can be generalized to monoidal categories satisfying a mild side condition: if, for an object H, the endofunctor H ⊗ _ + I has a final coalgebra, T, then T is a monoid. This specializes to the above case for the monoidal category of all endofunctors.}, journal = {Theor. Comput. Sci.}, - month = {may}, + month = {5}, pages = {1–45}, numpages = {45}, keywords = {coalgebra, completely iterative theory, monad, monoidal category, solution theorem} diff --git a/thesis/main.tex b/thesis/main.tex index 9e54e45..2bbfefe 100644 --- a/thesis/main.tex +++ b/thesis/main.tex @@ -18,6 +18,12 @@ \usepackage{fancyvrb} \usepackage{mathtools} \usepackage{amsmath} +\usepackage{mathpartir} +% mathpartir uses \atop, amsmath overrides it to throw a warning tho, so we override it back to the original! +\makeatletter +\let\atop\@@atop +\makeatother + \usepackage{tikz} \usetikzlibrary{cd, babel, quotes} \usepackage{quiver} @@ -79,7 +85,7 @@ \setlength{\parskip}{6pt} \setlength{\marginparsep}{0cm} -\title{Implementing Notions of Partiality and Delay in Agda} +\title{Implementing Categorical Notions of Partiality and Delay in Agda} \author{Leon Vatthauer} @@ -98,8 +104,6 @@ %\usepackage{fontspec} %\setmonofont{Noto Sans Mono} -\usepackage{mathpartir} - \newcommand{\obj}[1]{\ensuremath{\vert \mathcal{#1} \vert}} \begin{document} \pagestyle{plain} diff --git a/thesis/src/01_preliminaries.tex b/thesis/src/01_preliminaries.tex index 6d72f7c..be4e881 100644 --- a/thesis/src/01_preliminaries.tex +++ b/thesis/src/01_preliminaries.tex @@ -67,19 +67,19 @@ Categories with finite products (i.e. binary products and a terminal object) are \begin{proposition} The distribution morphisms can be viewed as natural transformations i.e. they satisfy the following diagrams: -% https://q.uiver.app/#q=WzAsOCxbMCwwLCJYIFxcdGltZXMgKFkgK1opIl0sWzIsMCwiQSBcXHRpbWVzIChCICsgQykiXSxbMCwxLCJYIFxcdGltZXMgWSArIFggXFx0aW1lcyBaIl0sWzIsMSwiQSBcXHRpbWVzIEIgKyBBIFxcdGltZXMgQyJdLFszLDAsIihZICsgWikgXFx0aW1lcyBYIl0sWzUsMCwiKEIgKyBDKSBcXHRpbWVzIEEiXSxbMywxLCJZIFxcdGltZXMgWCArIFogXFx0aW1lcyBYIl0sWzUsMSwiQiBcXHRpbWVzIEEgKyBDIFxcdGltZXMgQSJdLFswLDEsImYgXFx0aW1lcyAoZyArIGgpIl0sWzIsMywiZiBcXHRpbWVzIGcgKyBmIFxcdGltZXMgaCJdLFswLDIsImRzdGwiXSxbMSwzLCJkc3RsIl0sWzQsNSwiKGcgKyBoKSBcXHRpbWVzIGYiXSxbNCw2LCJkc3RyIiwyXSxbNSw3LCJkc3RyIl0sWzYsNywiZyBcXHRpbWVzIGYgKyBoIFxcdGltZXMgZiIsMl1d -\[\begin{tikzcd} - {X \times (Y +Z)} && {A \times (B + C)} & {(Y + Z) \times X} && {(B + C) \times A} \\ - {X \times Y + X \times Z} && {A \times B + A \times C} & {Y \times X + Z \times X} && {B \times A + C \times A} - \arrow["{f \times (g + h)}", from=1-1, to=1-3] - \arrow["{f \times g + f \times h}", from=2-1, to=2-3] - \arrow["dstl", from=1-1, to=2-1] - \arrow["dstl", from=1-3, to=2-3] - \arrow["{(g + h) \times f}", from=1-4, to=1-6] - \arrow["dstr"', from=1-4, to=2-4] - \arrow["dstr", from=1-6, to=2-6] - \arrow["{g \times f + h \times f}"', from=2-4, to=2-6] -\end{tikzcd}\] + % https://q.uiver.app/#q=WzAsOCxbMCwwLCJYIFxcdGltZXMgKFkgK1opIl0sWzIsMCwiQSBcXHRpbWVzIChCICsgQykiXSxbMCwxLCJYIFxcdGltZXMgWSArIFggXFx0aW1lcyBaIl0sWzIsMSwiQSBcXHRpbWVzIEIgKyBBIFxcdGltZXMgQyJdLFszLDAsIihZICsgWikgXFx0aW1lcyBYIl0sWzUsMCwiKEIgKyBDKSBcXHRpbWVzIEEiXSxbMywxLCJZIFxcdGltZXMgWCArIFogXFx0aW1lcyBYIl0sWzUsMSwiQiBcXHRpbWVzIEEgKyBDIFxcdGltZXMgQSJdLFswLDEsImYgXFx0aW1lcyAoZyArIGgpIl0sWzIsMywiZiBcXHRpbWVzIGcgKyBmIFxcdGltZXMgaCJdLFswLDIsImRzdGwiXSxbMSwzLCJkc3RsIl0sWzQsNSwiKGcgKyBoKSBcXHRpbWVzIGYiXSxbNCw2LCJkc3RyIiwyXSxbNSw3LCJkc3RyIl0sWzYsNywiZyBcXHRpbWVzIGYgKyBoIFxcdGltZXMgZiJdXQ== + \[\begin{tikzcd}[column sep=4ex] + {X \times (Y +Z)} && {A \times (B + C)} & {(Y + Z) \times X} && {(B + C) \times A} \\ + {X \times Y + X \times Z} && {A \times B + A \times C} & {Y \times X + Z \times X} && {B \times A + C \times A} + \arrow["{f \times (g + h)}", from=1-1, to=1-3] + \arrow["{f \times g + f \times h}", from=2-1, to=2-3] + \arrow["dstl", from=1-1, to=2-1] + \arrow["dstl", from=1-3, to=2-3] + \arrow["{(g + h) \times f}", from=1-4, to=1-6] + \arrow["dstr"', from=1-4, to=2-4] + \arrow["dstr", from=1-6, to=2-6] + \arrow["{g \times f + h \times f}", from=2-4, to=2-6] + \end{tikzcd}\] \end{proposition} \begin{proof} We will prove naturality of $dstl$, naturality for $dstr$ is then analogous. We use the fact that $dstl^{-1}$ is an iso and therefore also an epi. diff --git a/thesis/src/03_partiality-monads.tex b/thesis/src/03_partiality-monads.tex index 0a6ffc9..1154e4b 100644 --- a/thesis/src/03_partiality-monads.tex +++ b/thesis/src/03_partiality-monads.tex @@ -1,7 +1,7 @@ \chapter{Partiality Monads} Moggi's categorical semantics~\cite{moggi} give us a way to interpret an effectul programming language in a category. For this one needs a (strong) monad $T$ capturing the desired effects, then we can take the elements of $TA$ as denotations for programs of type $A$. The kleisli category of $T$ can be viewed as the category of programs, which gives us a way of composing programs (Kleisli composition). -For this thesis we will restrict ourselves to monads for modelling partiality, the goal of this section is to capture what it means to be a partiality monad and look at two common examples. +For this thesis we will restrict ourselves to monads for modelling partiality, the goal of this chapter is to capture what it means to be a partiality monad and look at two common examples. \section{Properties of Partiality Monads} We will now look at how to express the following non-controversial properties of partiality monads categorically: @@ -41,7 +41,6 @@ Lastly we also recall the following notion by Bucalo et al.~\cite{eqlm} which ca \begin{definition}[Equational Lifting Monad] \label{def:eqlm} A commutative monad $T$ is called an \textit{equational lifting monad} if the following diagram commutes: - % https://q.uiver.app/#q=WzAsMyxbMCwwLCJUWCJdLFsyLDAsIlRYIFxcdGltZXMgVFgiXSxbMiwyLCJUKFRYIFxcdGltZXMgWCkiXSxbMCwxLCJcXERlbHRhIl0sWzEsMiwiXFx0YXUiXSxbMCwyLCJUIFxcbGFuZ2xlIFxcZXRhICwgaWQgXFxyYW5nbGUiLDJdXQ== \[\begin{tikzcd} TX && {TX \times TX} \\ @@ -54,11 +53,11 @@ Lastly we also recall the following notion by Bucalo et al.~\cite{eqlm} which ca where $\Delta : X \rightarrow X \times X$ is the diagonal morphism. \end{definition} -\begin{theorem} +\begin{theorem}[no proof] Let $T$ be an equational lifting monad, then $\mathcal{C}^T$ is a restriction category~\cite{eqlm}. \end{theorem} -Definition~\ref{def:eqlm} combines all three properties stated above, so when studying partiality monads in this thesis, we ideally expect them to be equational lifting monads. For the rest of this chapter we will use these definitions to classify two common examples of monads that are used to model partiality. +Definition~\ref{def:eqlm} combines all three properties stated above, so when studying partiality monads in this thesis, we ideally expect them to be equational lifting monads. For the rest of this chapter we will use these definitions to compare two common examples of monads that are used to model partiality. \section{The Maybe Monad} The endofunctor $MX = X + 1$ extends to a monad by taking $\eta_X : X \rightarrow X + 1 = i_1$ and $\mu_X : (X + 1) + 1 \rightarrow X + 1 = [ id , i_2 ]$. The monad laws follow easily. This is generally known as the maybe monad and can be viewed as the prototypical example of an equational lifting monad: @@ -77,17 +76,36 @@ The endofunctor $MX = X + 1$ extends to a monad by taking $\eta_X : X \rightarro = \;&((id \times f) + !) \circ dstl\\ = \;&((id \times f) + id) \circ (id + !) \circ dstl \end{alignat*} + the other strength laws and commutativity can be proven by using simple properties of distributive categories, we added these proofs to the formalization for completeness. - and commutativity: - - and the equational lifting law: - + We are left to check the equational lifting law: + % https://q.uiver.app/#q=WzAsNCxbMCwwLCJYKzEiXSxbMywwLCIoWCsxKVxcdGltZXMoWCsxKSJdLFszLDIsIigoWCsxKVxcdGltZXMgWCkgKygoWCsxKVxcdGltZXMgMSkiXSxbMyw0LCIoKFgrMSlcXHRpbWVzIFgpKzEiXSxbMCwxLCJcXERlbHRhIl0sWzEsMiwiZHN0bCJdLFsyLDMsImlkK1xcOyEiXSxbMCwzLCJcXGxhbmdsZSBpXzEsaWRcXHJhbmdsZSArIFxcOyEiLDJdXQ== + \[\begin{tikzcd} + {X+1} &&& {(X+1)\times(X+1)} \\ + \\ + &&& {((X+1)\times X) +((X+1)\times 1)} \\ + \\ + &&& {((X+1)\times X)+1} + \arrow["\Delta", from=1-1, to=1-4] + \arrow["dstl", from=1-4, to=3-4] + \arrow["{id+\;!}", from=3-4, to=5-4] + \arrow["{\langle i_1,id\rangle + \;!}"', from=1-1, to=5-4] + \end{tikzcd}\] + By postcomposing $i_1$ and $i_2$ it suffices to show that: + \[i_1 \circ \langle i_1 , id \rangle = (id\;+\;!) \circ dstl \circ \langle i_1 , i_1 \rangle\] + and + \[i_2 \;\circ \;! = (id\;+\;!) \circ dstl \circ \langle i_2 , i_2 \rangle\] + which follow easily by the fact that + \[dstl \circ (id \times i_1) = i_1\] + and + \[dstl \circ (id \times i_2) = i_2\] \end{proof} +In a classical setting this monad is therefore sufficient for modelling partiality, but in general it won't be useful for modelling programming languages that have non-termination as a side effect, since one would need to know beforehand whether a program terminates or not. For the purpose of modelling possibly non-terminating computations another monad has been developed by Venanzio Capretta. \section{The Delay Monad} -Capretta's delay monad is a coinductive datatype whose inhabitants can be viewed as suspended computations. -It is defined by the two coinductive constructors $now$ and $later$, where $now$ is for lifting a value to a computation and $later$ intuitively delays a computation by one time unit: +Capretta's delay monad~\cite{delay} is a coinductive datatype whose inhabitants can be viewed as suspended computations. +It is usually defined by the two coinductive constructors $now$ and $later$, where $now$ is for lifting a value to a computation and $later$ intuitively delays a computation by one time unit: \[\mprset{fraction={===}} \inferrule {x : X} {now\; x : DX}\hskip 2cm @@ -132,7 +150,7 @@ Since $DX$ is defined as a final coalgebra, we can define morphisms via corecurs \end{equation*} \end{itemize} \end{corollary} -\begin{proof}\;\\ +\begin{proof} \begin{itemize} \item[\ref{D1}] Take $\eta = now$ then $out \circ now = i_1$ follows by definition of $now$. \item[\ref{D2}] We define $f^* = \;! \circ i_1$, where $!$ is the unique coalgebra-morphism in this diagram: @@ -256,18 +274,18 @@ Since $(DX, out)$ is a final coalgebra we get the following proof principle: \arrow["{[ (id + (id \times now)) \circ dstl \circ (id \times out) , i_2 ]}"', from=1-3, to=2-3] \end{tikzcd}\] \item[\ref{S4}] To show that $D\alpha \circ \tau = \tau \circ (id \times \tau) \circ \alpha$ we take the following coalgebra: - % https://q.uiver.app/#q=WzAsNixbMCwwLCIoWCBcXHRpbWVzIFkpIFxcdGltZXMgRFoiXSxbMCwyLCJEKFggXFx0aW1lcyBZIFxcdGltZXMgWikiXSxbMywyLCJYIFxcdGltZXMgWSBcXHRpbWVzIFogKyBEKFggXFx0aW1lcyBZIFxcdGltZXMgWikiXSxbMywxLCJYIFxcdGltZXMgWSAgXFx0aW1lcyBaICsgKFggXFx0aW1lcyBZKSBcXHRpbWVzIERaIl0sWzIsMCwiKFggXFx0aW1lcyBZKSBcXHRpbWVzIChaKyBEWikiXSxbMywwLCIoWFxcdGltZXMgWSkgXFx0aW1lcyBaICsgKFggXFx0aW1lcyBZKSBcXHRpbWVzIERaIl0sWzAsMSwiISIsMCx7InN0eWxlIjp7ImJvZHkiOnsibmFtZSI6ImRhc2hlZCJ9fX1dLFsxLDIsIm91dCJdLFszLDIsImlkICtcXDshIiwyXSxbMCw0LCJpZCBcXHRpbWVzIG91dCJdLFs0LDUsImRzdGwiXSxbNSwzLCJcXGxhbmdsZSBcXHBpXzEgXFxjaXJjIFxccGlfMSAsIFxcbGFuZ2xlIFxccGlfMiBcXGNpcmMgXFxwaV8xICwgXFxwaV8yIFxccmFuZ2xlIFxccmFuZ2xlICsgaWQiLDJdXQ== - \[\begin{tikzcd} - {(X \times Y) \times DZ} && {(X \times Y) \times (Z+ DZ)} & {(X\times Y) \times Z + (X \times Y) \times DZ} \\ - &&& {X \times Y \times Z + (X \times Y) \times DZ} \\ - {D(X \times Y \times Z)} &&& {X \times Y \times Z + D(X \times Y \times Z)} - \arrow["{!}", dashed, from=1-1, to=3-1] - \arrow["out", from=3-1, to=3-4] - \arrow["{id +\;!}"', from=2-4, to=3-4] - \arrow["{id \times out}", from=1-1, to=1-3] - \arrow["dstl", from=1-3, to=1-4] - \arrow["{\langle \pi_1 \circ \pi_1 , \langle \pi_2 \circ \pi_1 , \pi_2 \rangle \rangle + id}"', from=1-4, to=2-4] - \end{tikzcd}\] + % https://q.uiver.app/#q=WzAsNixbMCwwLCIoWCBcXHRpbWVzIFkpIFxcdGltZXMgRFoiXSxbMCwyLCJEKFggXFx0aW1lcyBZIFxcdGltZXMgWikiXSxbMiwyLCJYIFxcdGltZXMgWSBcXHRpbWVzIFogKyBEKFggXFx0aW1lcyBZIFxcdGltZXMgWikiXSxbMiwxLCJYIFxcdGltZXMgWSAgXFx0aW1lcyBaICsgKFggXFx0aW1lcyBZKSBcXHRpbWVzIERaIl0sWzEsMCwiKFggXFx0aW1lcyBZKSBcXHRpbWVzIChaKyBEWikiXSxbMiwwLCIoWFxcdGltZXMgWSkgXFx0aW1lcyBaICsgKFggXFx0aW1lcyBZKSBcXHRpbWVzIERaIl0sWzAsMSwiISIsMCx7InN0eWxlIjp7ImJvZHkiOnsibmFtZSI6ImRhc2hlZCJ9fX1dLFsxLDIsIm91dCJdLFszLDIsImlkICtcXDshIiwyXSxbMCw0LCJpZCBcXHRpbWVzIG91dCJdLFs0LDUsImRzdGwiXSxbNSwzLCJcXGxhbmdsZSBcXHBpXzEgXFxjaXJjIFxccGlfMSAsIFxcbGFuZ2xlIFxccGlfMiBcXGNpcmMgXFxwaV8xICwgXFxwaV8yIFxccmFuZ2xlIFxccmFuZ2xlICsgaWQiLDJdXQ== + \[\begin{tikzcd} + {(X \times Y) \times DZ} & {(X \times Y) \times (Z+ DZ)} & {(X\times Y) \times Z + (X \times Y) \times DZ} \\ + && {X \times Y \times Z + (X \times Y) \times DZ} \\ + {D(X \times Y \times Z)} && {X \times Y \times Z + D(X \times Y \times Z)} + \arrow["{!}", dashed, from=1-1, to=3-1] + \arrow["out", from=3-1, to=3-3] + \arrow["{id +\;!}"', from=2-3, to=3-3] + \arrow["{id \times out}", from=1-1, to=1-2] + \arrow["dstl", from=1-2, to=1-3] + \arrow["{\langle \pi_1 \circ \pi_1 , \langle \pi_2 \circ \pi_1 , \pi_2 \rangle \rangle + id}"', from=1-3, to=2-3] + \end{tikzcd}\] \end{itemize} \end{proof} @@ -314,7 +332,7 @@ To show that $\mathbf{D}$ is commutative we will use another proof principle pre \begin{proof} Using corollary~\ref{cor:solution} it suffices to show that both $\tau^* \circ \hat{\tau}$ and $\hat{\tau}^* \circ \tau$ are solutions of some guarded morphism $g$. - Let $w = (dstr + dstr) ∘ dstl ∘ (out \times out)$ and + Let $w = (dstr + dstr) \circ dstl \circ (out \times out)$ and \[g = out^{-1} \circ [ i_1 + D i_1 \circ \hat{\tau} , i_2 \circ [ D i_1 \circ \tau , later \circ now \circ i_2 ] ] \circ w\] $g$ is trivially guarded by $[ id + D i_1 \circ \hat{\tau} , i_2 \circ [ D i_1 \circ \tau , later \circ now \circ i_2 ] ] \circ w$. @@ -335,4 +353,8 @@ To show that $\mathbf{D}$ is commutative we will use another proof principle pre \arrow["dstl", from=1-3, to=1-5] \end{tikzcd}\] the last step holds generally for any $f : DX \times DY \rightarrow D(X \times Y)$. -\end{proof} \ No newline at end of file +\end{proof} + +We have now seen that $\mathbf{D}$ is strong and commutative, ideally we would want it to be an equational lifting monad, but this is not the case since besides modelling non-termination, the delay monad also captures the execution time. This is a result of the too intensional notion of equality that this monad comes with. + +In chapter~\ref{chp:setoids} we will see how to remedy this, by taking the quotient of the delay monad where execution time is ignored. This will then give us an equational lifting monad in the category of setoids, but Chapman et al.~\cite{quotienting} have found that this does not work generally without assuming some form of the axiom of countable choice (which crucially holds in the category of setoids). \ No newline at end of file diff --git a/thesis/src/05_setoids.tex b/thesis/src/05_setoids.tex index fe767df..fe22860 100644 --- a/thesis/src/05_setoids.tex +++ b/thesis/src/05_setoids.tex @@ -1 +1 @@ -\chapter{A Case Study on Setoids} \ No newline at end of file +\chapter{A Case Study on Setoids}\label{chp:setoids} \ No newline at end of file diff --git a/thesis/src/titlepage.tex b/thesis/src/titlepage.tex index 62e0063..a912ba2 100644 --- a/thesis/src/titlepage.tex +++ b/thesis/src/titlepage.tex @@ -20,10 +20,10 @@ Erlangen-Nürnberg% \makeatletter \@title \\[1cm] \makeatother -\large\bfseries -An exploration of \ldots % TODo -\\ and \ldots -\\[1cm] +% \large\bfseries +% An exploration of \ldots % TODo +% \\ and \ldots +% \\[1cm] \textbf{\large Bachelor Thesis in Computer Science} }\\[0.5\baselineskip] \rule{\textwidth}{1pt}\par