leonv/bsc-leon-vatthauer
1
0
Fork 0
mirror of https://git8.cs.fau.de/theses/bsc-leon-vatthauer.git synced 2024-05-31 07:28:34 +02:00
Code Issues Projects Releases Packages Wiki Activity

change notation for freeobjects and coalgebras, work on partiality chapter

Browse source
This commit is contained in:
Leon Vatthauer 2024-02-24 13:12:32 +01:00
parent 65890dbffd
commit 5f479bf4f8
Signed by: leonv
SSH key fingerprint: SHA256:G4+ddwoZmhLPRB1agvXzZMXIzkVJ36dUYZXf5NxT+u8
9 changed files with 157 additions and 75 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
thesis/.vscode/ltex.dictionary.en-GB.txt vendored Normal file
View file

@ -0,0 +1,2 @@
Agda
Vatthauer

8
thesis/.vscode/ltex.dictionary.en-US.txt vendored
View file

@ -52,3 +52,11 @@ counit
epi
F-coalgebra
F-coalgebras
F-Coalgebras
terminality
coinductively
monos
epis
isos
Corecursion
subobject

2
thesis/.vscode/ltex.hiddenFalsePositives.en-GB.txt vendored Normal file
View file

@ -0,0 +1,2 @@
{"rule":"MORFOLOGIK_RULE_EN_GB","sentence":"^\\Q[agda] linenos=true, breaklines=true, encoding=utf8, fontsize=, frame=lines, autogobble\\E$"}
{"rule":"WHITESPACE_RULE","sentence":"^\\Q[4][]##4\\E$"}

6
thesis/.vscode/ltex.hiddenFalsePositives.en-US.txt vendored
View file

@ -1,3 +1,9 @@
{"rule":"POSSESSIVE_APOSTROPHE","sentence":"^\\QFurthermore, in mathematical textbooks equality between morphisms is usually taken for granted, i.e. there is some global notion of equality that is clear to everyone.\\E$"}
{"rule":"SENTENCE_WHITESPACE","sentence":"^\\QKleisli').\\E$"}
{"rule":"SENTENCE_WHITESPACE","sentence":"^\\QConstruction.\\E$"}
{"rule":"NO_SPACE_CLOSING_QUOTE","sentence":"^\\Q[inline]Change quotation marks ”\\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q”: Given a Kleisli triple \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q, we get a monad \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q where \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q is the object mapping of the Kleisli triple together with the functor action \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q, \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q is the morphism family of the Kleisli triple where naturality is easy to show and \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q is a natural transformation defined as \\E(?:Dummy|Ina|Jimmy-)[0-9]+$"}
{"rule":"IF_IS","sentence":"^\\QLet \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q and \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q be a setoid morphism, we define \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q point wise: \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q if \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q if \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q where \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q is defined corecursively by: \\E(?:Dummy|Ina|Jimmy-)[0-9]+$"}
{"rule":"ENGLISH_WORD_REPEAT_RULE","sentence":"^\\QThe following conditions hold: There exists a unit morphism \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q for any DX, satisfying \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q For any \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q there exists a unique morphism \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q satisfying: \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q There exists a unique morphism \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q satisfying: &&&& &&&& \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q We will make use of the fact that every \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q is a final coalgebra: [\\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q] This follows by definition of \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q.\\E$"}
{"rule":"ENGLISH_WORD_REPEAT_RULE","sentence":"^\\QWe call a morphism \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q guarded if there exists an \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q such that the following diagram commutes: &&& &&& \\E(?:Dummy|Ina|Jimmy-)[0-9]+$"}
{"rule":"ENGLISH_WORD_REPEAT_RULE","sentence":"^\\QIt suffices to show \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q, because then follows: \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q We prove this by coinduction using: [inline]Change name of morphism &&& &&& \\E(?:Dummy|Ina|Jimmy-)[0-9]+$"}
{"rule":"ENGLISH_WORD_REPEAT_RULE","sentence":"^\\Q[inline]Make this more explicit The first step in both equations can be proven by monicity of \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q and then using \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q and the dual diagram for \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q which is a direct consequence of \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q: &&&& &&&& \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q the last step holds generally for any \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q.\\E$"}

10
thesis/bib.bib
View file

@ -131,10 +131,12 @@
}
@online{nad-delay,
author = {Nils Anders Danielsson},
title = {The delay monad, defined coinductively},
url = {https://www.cse.chalmers.se/~nad/listings/delay-monad/Delay-monad.html},
urldate = {2024-15-02}
author = {Nils Anders Danielsson},
title = {The delay monad, defined coinductively},
url = {https://www.cse.chalmers.se/~nad/listings/delay-monad/Delay-monad.html},
urlday = {15},
urlmonth = {02},
urlyear = {2024}
}
@article{param-corec,

18
thesis/main.tex
View file

@ -1,8 +1,7 @@
\documentclass[a4paper,11pt,numbers=noenddot]{scrbook}
\usepackage[top=2cm,lmargin=1in,rmargin=1in,bottom=3cm,hmarginratio=1:1]{geometry}
% \usepackage[utf8]{inputenc}
\usepackage[ngerman, english]{babel}
\usepackage[ngerman, main=british]{babel}
\babeltags{german=ngerman}
\usepackage{minted}
\setminted[agda]{
@ -20,6 +19,7 @@
\usepackage{fancyvrb}
\usepackage{mathtools}
\usepackage{amsmath}
\usepackage{mathabx}
\usepackage{mathpartir}
% mathpartir uses \atop, amsmath overrides it to throw a warning tho, so we override it back to the original!
\makeatletter
@ -36,7 +36,7 @@
\usepackage{makeidx}
\usepackage{graphicx}
\usepackage{fvextra}
\usepackage[style=ieee, sorting=ynt]{biblatex} % advanced citations
\usepackage[style=ieee, sorting=ynt, language=british]{biblatex} % advanced citations, british to make dates DD-MM-YYYY
\usepackage[english=british]{csquotes} % biblatex recommended to load this
\usepackage{etoolbox,xpatch}
@ -62,8 +62,6 @@
\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}
@ -103,6 +101,7 @@
\usepackage{noto-mono}
\usepackage[colorinlistoftodos,prependcaption,textsize=tiny]{todonotes}
\usepackage{xargs}
\usepackage{xstring}
%\usepackage{fontspec}
%\setmonofont{Noto Sans Mono}
@ -118,6 +117,15 @@
% category of pre-Elgot monads on #1
\newcommand*{\preelgot}[1]{\ensuremath{\mathit{PreElgot}(#1)}}
\newcommand*{\setoids}{\ensuremath{\mathit{Setoids}}}
% free objects
\newcommand*{\freee}[1]{\ensuremath{#1^\bigstar}}
\newcommand*{\free}[1]{
\ensuremath{
\IfSubStr{#1}{\circ}{{\freee{(#1)}}}{\freee{#1}}
}
}
% terminal coalgebra
\newcommand*{\coalg}[1]{\ensuremath{\llbracket #1 \rrbracket}}
\begin{document}
\pagestyle{plain}

126
thesis/src/01_preliminaries.tex
View file

@ -112,8 +112,8 @@ Categories with finite products (i.e. binary products and a terminal object) are
A cartesian closed category is a cartesian category $\C$ that also has an exponential object $X^Y$ for any $X, Y \in \C$.
The internal logic of cartesian closed categories is the simply typed $\lambda$-calculus, which makes them a suitable target for interpreting programming languages. For the rest of this thesis we will work in an ambient distributive category that however does not have to be cartesian closed as to be more general.
\section{Functor Coalgebras}
Let $F : \C \rightarrow \C$ be an endofunctor. Recall that F-algebras are tuples $(X, \alpha : FX \rightarrow X)$ consisting of an object of $\C$ and a morphism out of the functor. Initial F-algebras have been studied extensively as a means of modelling inductive data types together with induction and recursion principles~\cite{inductive}. For this thesis we will be more interested in the dual concept namely terminal coalgebras let us formally introduce them now.
\section{F-Coalgebras}
Let $F : \C \rightarrow \C$ be an endofunctor. Recall that F-algebras are tuples $(X, \alpha : FX \rightarrow X)$ consisting of an object of $\C$ and a morphism out of the functor. Initial F-algebras have been studied extensively as a means of modelling inductive data types together with induction and recursion principles~\cite{inductive}. For this thesis we will be more interested in the dual concept namely terminal coalgebras; let us formally introduce them now.
\begin{definition}[F-Coalgebra]
A tuple $(X \in \obj{\C}, \alpha : X \rightarrow FX)$ is called a terminal F-coalgebra.
@ -150,18 +150,61 @@ Let $F : \C \rightarrow \C$ be an endofunctor. Recall that F-algebras are tuples
\end{alignat*}
\end{proof}
The terminal object of $Coalg(F)$ is sometimes called \textit{final F-coalgebra} and can now similarly to initial F-algebras be used for modelling the semantics of coinductive data types. Another special property arises:
The terminal object of $Coalg(F)$ is sometimes called \textit{final F-coalgebra} and can now similarly to initial F-algebras be used for modelling the semantics of coinductive data types where terminality of the coalgebra yields corecursion as a definitional principle and coinduction as a proof principle. Let us make the universal property of terminal F-coalgebras concrete:
\todo[inline]{Characterize final coalgebra first, introduce notation with double bracket}
\begin{definition}[Terminal F-Coalgebra]
An F-coalgebra $(T, t : T \rightarrow FT)$ is called a terminal F-coalgebra if for any other F-coalgebra $(X, \alpha : X \rightarrow FX)$ there exists a unique morphism $\coalg{\alpha} : X \rightarrow T$ satisfying:
\begin{theorem}[Lambek's Lemma]
% https://q.uiver.app/#q=WzAsNCxbMCwwLCJYIl0sWzIsMCwiRlgiXSxbMCwyLCJUIl0sWzIsMiwiRlQiXSxbMCwxLCJcXGFscGhhIl0sWzIsMywidCJdLFswLDIsIlxcbGxicmFja2V0IFxcYWxwaGEgXFxycmJyYWNrZXQiLDIseyJzdHlsZSI6eyJib2R5Ijp7Im5hbWUiOiJkYXNoZWQifX19XSxbMSwzLCJGXFxsbGJyYWNrZXQgXFxhbHBoYSBcXHJyYnJhY2tldCJdXQ==
\[\begin{tikzcd}[ampersand replacement=\&]
X \&\& FX \\
\\
T \&\& FT
\arrow["\alpha", from=1-1, to=1-3]
\arrow["t", from=3-1, to=3-3]
\arrow["{\coalg{\alpha}}"', dashed, from=1-1, to=3-1]
\arrow["{F\coalg{\alpha}}", from=1-3, to=3-3]
\end{tikzcd}\]
\end{definition}
\begin{lemma}[Lambek's Lemma]
Let $(T, t : T \rightarrow FT)$ be a terminal F-coalgebra. Then $t$ is an isomorphism.
\end{theorem}
\end{lemma}
\begin{proof}
\end{proof}
Note that $(FT, Ft : FT \rightarrow FFT)$ is also an F-coalgebra. This yields the unique morphism $\coalg{Ft} : FT \rightarrow T$ satisfying:
% https://q.uiver.app/#q=WzAsNCxbMCwwLCJGVCJdLFsyLDAsIkZGVCJdLFswLDIsIlQiXSxbMiwyLCJGVCJdLFswLDEsIkZ0Il0sWzIsMywidCJdLFswLDIsIlxcbGxicmFja2V0IEZ0IFxccnJicmFja2V0IiwyLHsic3R5bGUiOnsiYm9keSI6eyJuYW1lIjoiZGFzaGVkIn19fV0sWzEsMywiRlxcbGxicmFja2V0IEZ0IFxccnJicmFja2V0Il1d
\[\begin{tikzcd}[ampersand replacement=\&]
FT \&\& FFT \\
\\
T \&\& FT
\arrow["Ft", from=1-1, to=1-3]
\arrow["t", from=3-1, to=3-3]
\arrow["{\coalg{Ft}}"', dashed, from=1-1, to=3-1]
\arrow["{F\coalg{Ft}}", from=1-3, to=3-3]
\end{tikzcd}\]
\todo[inline]{Introduce (terminal) coalgebras, prove Lambek's lemma}
$\coalg{Ft}$ is inverse to $t$:
\begin{enumerate}
\item $\coalg{Ft} \circ t : (T, t) \rightarrow (T, t)$ is a morphism between F-coalgebras since
\begin{alignat*}{1}
&F(\coalg{Ft} \circ t) \circ t\\
=\;&F \coalg{Ft} \circ t \circ t\\
=\;&F \coalg{Ft} \circ Ft \circ t\\
=\;&t \circ \coalg{Ft} \circ t
\end{alignat*}
By uniqueness of the identity on $(T, t)$ we follow that $\coalg{Ft} \circ t = id$.
\item $t \circ \coalg{Ft} = id : (FT, Ft) \rightarrow (FT, Ft)$ follows by:
\begin{alignat*}{1}
&t \circ \coalg{Ft}\\
=\;&F\coalg{Ft} \circ Ft\\
=\;&F(\coalg{Ft} \circ t)\\
=\;&F(id)\\
=\;&id
\end{alignat*}
\end{enumerate}
\end{proof}
\section{Adjunctions and Free Objects}
\todo[inline]{Add text}
@ -184,17 +227,15 @@ The terminal object of $Coalg(F)$ is sometimes called \textit{final F-coalgebra}
Free objects are constructions capturing the essence of structures in a minimal way, we will rely on free structures in chapter~\ref{chp:iteration} to define a monad in a general setting. We recall the definition to establish some notation:
\todo[inline]{Change free object notation from llbracket to something else (llbracket is better for terminal coalg)}
\begin{definition}[Free Object]\label{def:free}
Let $\C, \D$ be categories and $U : \C \rightarrow \D$ be a forgetful functor (whose construction usually is obvious). A free object on some object $X \in \obj{\D}$ is an object $FX \in \obj{\C}$ together with a morphism $\eta : X \rightarrow UFX$ such that the following universal property holds for any $Y \in \obj{\C}$ and $f : X \rightarrow UY$:
% https://q.uiver.app/#q=WzAsMyxbMCwwLCJYIl0sWzEsMCwiVVkiXSxbMCwxLCJGWCJdLFswLDEsImYiXSxbMCwyLCJcXGV0YSIsMl0sWzIsMSwiXFxleGlzdHMhXFxsbGJyYWNrZXQgZiBcXHJyYnJhY2tldCIsMl1d
\[\begin{tikzcd}
X & UY \\
Let $\C, \D$ be categories and $U : \C \rightarrow \D$ be a forgetful functor (whose construction usually is obvious). A free object on some object $X \in \obj{\D}$ is an object $FX \in \obj{\C}$ together with a morphism $\eta : X \rightarrow UFX$ such that for any $Y \in \obj{\C}$ and $f : X \rightarrow UY$ there exists a unique morphism $\free{f} : FX \rightarrow UY$ satisfying:
% https://q.uiver.app/#q=WzAsMyxbMCwwLCJYIl0sWzEsMCwiVVkiXSxbMCwxLCJGWCJdLFswLDEsImYiXSxbMCwyLCJcXGV0YSIsMl0sWzIsMSwiXFxmcmVle2Z9IiwyLHsic3R5bGUiOnsiYm9keSI6eyJuYW1lIjoiZGFzaGVkIn19fV1d
\[\begin{tikzcd}[ampersand replacement=\&]
X \& UY \\
FX
\arrow["f", from=1-1, to=1-2]
\arrow["\eta"', from=1-1, to=2-1]
\arrow["{\exists!\llbracket f \rrbracket}"', from=2-1, to=1-2]
\arrow["{\free{f}}"', dashed, from=2-1, to=1-2]
\end{tikzcd}\]
\end{definition}
@ -204,62 +245,57 @@ Let $\C, \D$ be categories and $U : \C \rightarrow \D$ be a forgetful functor (w
\end{theorem}
\begin{proof}
First we define the free functor $F : \D \rightarrow \C$. $F$ maps objects of $\D$ to the corresponding $FX$ in $\C$ (where $FX$ is the underlying object in Definition~\ref{def:free}).
For any morphism $f : X \rightarrow Y$ in $\D$ we take $Ff = \llbracket\eta \circ f\rrbracket$.
For any morphism $f : X \rightarrow Y$ in $\D$ we take $Ff = \free{\eta \circ f}$.
This is a functor because:
\begin{enumerate}
\item The identity law:
\[Fid = \llbracket \eta \circ id \rrbracket = \llbracket \eta \rrbracket = id\]
follows by uniqueness of $\llbracket \eta \rrbracket$ since $id$ satisfies $id \circ \eta = \eta$.
\[Fid = \free{\eta \circ id} = \free{\eta} = id\]
follows by uniqueness of $\free{\eta}$ since $id$ satisfies $id \circ \eta = \eta$.
\item Let $f : X \rightarrow Y$ and $g : Y \rightarrow Z$. The compositional law:
\[F(g \circ f) = \llbracket \eta \circ g \circ f \rrbracket = \llbracket \eta \circ g \rrbracket \circ \llbracket \eta \circ f \rrbracket = Fg \circ Ff \]
follows by uniqueness of $\llbracket \eta \circ g \circ f \rrbracket$ since:
\[\llbracket \eta \circ g \rrbracket \circ \llbracket \eta \circ f \rrbracket \circ \eta = \llbracket \eta \circ g \rrbracket \circ \eta \circ f = \eta \circ g \circ f\]
\[F(g \circ f) = \free{\eta \circ g \circ f} = \free{\eta \circ g} \circ \free{\eta \circ f} = Fg \circ Ff \]
follows by uniqueness of $\free{\eta \circ g \circ f}$ since:
\[\free{\eta \circ g} \circ \free{\eta \circ f} \circ \eta = \free{\eta \circ g} \circ \eta \circ f = \eta \circ g \circ f\]
\end{enumerate}
We are left to show that $F$ is left adjoint to $U$. The free object $\eta$ extends to a family of morphisms $(\eta_X : X \rightarrow UFX)_{X \in \obj{D}}$ yielding the unit of the adjunction. For naturality of $\eta$ we need to check:
\[\eta \circ f = \llbracket \eta \circ f \rrbracket \circ \eta = UFf \circ \eta\]
\[\eta \circ f = \free{\eta \circ f}\circ \eta = UFf \circ \eta\]
which follows by the universal property of free objects.
As the counit take $\epsilon = \llbracket id \rrbracket : FU \rightarrow Id$. For naturality of $\epsilon$ we show:
\[\llbracket id \rrbracket \circ FU f = \llbracket Uf \rrbracket = f \circ \llbracket id \rrbracket\]
As the counit take $\epsilon = \free{id}: FU \rightarrow Id$. For naturality of $\epsilon$ we show:
\[\free{id}\circ FU f = \free{Uf}= f \circ \free{id }\]
where $f : X \rightarrow Y$.
Using uniqueness of $\llbracket Uf \rrbracket$ we are done by:
Using uniqueness of $\free{Uf }$ we are done by:
\begin{alignat*}{1}
&U (\llbracket id \rrbracket \circ FUf) \circ \eta\\
=\;&U \llbracket id \rrbracket \circ UFUf \circ \eta\\
=\;&U \llbracket id \rrbracket \circ \eta \circ Uf\\
&U (\free{id}\circ FUf) \circ \eta\\
=\;&U \free{id}\circ UFUf \circ \eta\\
=\;&U \free{id}\circ \eta \circ Uf\\
=\;&id \circ Uf\\
=\;&Uf
\end{alignat*}
% \[U (\llbracket id \rrbracket \circ FUf) \circ \eta = U \llbracket id \rrbracket \circ UFUf \circ \eta = U \llbracket id \rrbracket \circ \eta \circ Uf = id \circ Uf = Uf\]
and
\begin{alignat*}{1}
&U (f \circ \llbracket id \rrbracket) \circ \eta\\
=\;&Uf \circ U\llbracket id \rrbracket \circ \eta\\
&U (f \circ \free{id }) \circ \eta\\
=\;&Uf \circ U\free{id}\circ \eta\\
=\;&Uf \circ id\\
=\;&Uf
\end{alignat*}
% \[U (f \circ \llbracket id \rrbracket) \circ \eta = Uf \circ U\llbracket id \rrbracket \circ \eta = Uf \circ id = Uf \]
Let us finally check the triangle identities. The first one can be proven via:
\[\epsilon \circ F\eta = \llbracket id \rrbracket \circ \llbracket \eta \circ \eta \rrbracket = \llbracket \eta \rrbracket = id \]
where the only step missing is $\llbracket id \rrbracket \circ \llbracket \eta \circ \eta \rrbracket = \llbracket \eta \rrbracket$ which holds since:
\[\epsilon \circ F\eta = \free{id}\circ \free{\eta \circ \eta}= \free{\eta}= id \]
where the only step missing is $\free{id}\circ \free{\eta \circ \eta}= \free{\eta}$ which holds since:
\begin{alignat*}{1}
&\llbracket id \rrbracket \circ \llbracket \eta \circ \eta \rrbracket \circ \eta\\
=\;&\llbracket id \rrbracket \circ \eta \circ \eta\\
&\free{id}\circ \free{\eta \circ \eta}\circ \eta\\
=\;&\free{id}\circ \eta \circ \eta\\
=\;&id \circ \eta\\
=\;&\eta
\end{alignat*}
% \[\llbracket id \rrbracket \circ \llbracket \eta \circ \eta \rrbracket \circ \eta = \llbracket id \rrbracket \circ \eta \circ \eta = id \circ \eta = \eta\]
The second triangle identity is a direct consequence of the universal property of free objects:
\[U\epsilon \circ \eta = U \llbracket id \rrbracket \circ \eta = id\]
\[U\epsilon \circ \eta = U \free{id}\circ \eta = id\]
We have thereby proven that indeed $F \dashv U$.
\end{proof}
\section{Monads}
@ -338,10 +374,11 @@ Morphisms between monads are natural transformations that respect the monad oper
Monads on a category $\C$ together with monad morphisms form a category that we call $\monads{\C}$. The identity morphism is the identity natural transformation that trivially respects the monad operations and composition of morphisms is composition of natural transformations.
\end{definition}
\change[inline]{Change text}
For programmers a second equivalent definition is more useful:
\begin{definition}[Kleisli Triple]
A Kleisli triple on a category $\C$ is a triple $(F, \eta, (-)^*)$, where $F : \obj{C} \rightarrow \obj{C}$ is a mapping on objects, $(\eta_X : X \rightarrow FX)_{X\in\obj{C}}$ 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, where the following laws hold:
A Kleisli triple on a category $\C$ is a triple $(F, \eta, (-)^*)$, where $F : \obj{C} \rightarrow \obj{C}$ is a mapping on objects, $(\eta_X : X \rightarrow FX)_{X\in\obj{C}}$ 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, where the following laws hold:
\begin{alignat*}{2}
&\eta_X^* &&= id_{FX} \tag*{(K1)}\label{K1}\\
&\eta_X \circ f^* &&= f \tag*{(K2)}\label{K2}\\
@ -374,14 +411,13 @@ This results in the following:
\begin{proof}
The crux of this proof is defining the triples, the proofs of the corresponding laws (functoriality, naturality, monad and Kleisli triple laws) are left out.
\change[inline]{Change quotation marks}
'' $\Rightarrow$'':
``$\Rightarrow$'':
Given a Kleisli triple $(F, \eta, (-)^*)$,
we get a monad $(F, \eta, \mu)$ where $F$ is the object mapping of the Kleisli triple together with the functor action $F(f : X \rightarrow Y) = (\eta_Y \circ f)^*$,
$\eta$ is the morphism family of the Kleisli triple where naturality is easy to show and $\mu$ is a natural transformation defined as $\mu_X = id_{FX}^*$
'' $\Leftarrow$'': \\
``$\Leftarrow$'': \\
Given a monad $(F, \eta, \mu)$,
we get a Kleisli triple $(F, \eta, (-)^*)$ by restricting the functor $F$ on objects,
taking the underlying mapping of $\eta$ and defining $f^* = \mu_Y \circ Ff$ for any $f : X \rightarrow FY$.

54
thesis/src/03_partiality-monads.tex
View file

@ -1,5 +1,5 @@
\chapter{Partiality Monads}\label{chp:partiality}
Moggi's categorical semantics~\cite{moggi} give us a way to interpret an effectful 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).
Moggi's categorical semantics~\cite{moggi} give us a way to interpret an effectful 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 chapter is to capture what it means to be a partiality monad and look at two common examples.
@ -22,23 +22,40 @@ To ensure that programs are partial, we recall the following notion by Cockett a
\begin{definition}[Restriction Structure]
A restriction structure on a category $\mathcal{C}$ is a mapping $dom : \mathcal{C}(X, Y) \rightarrow \mathcal{C}(X , X)$ with the following properties:
\begin{alignat*}{1}
f \circ (\tdom f) &= f\tag*{(R1)}\\
(\tdom f) \circ (\tdom g) &= (\tdom g) \circ (\tdom f)\tag*{(R2)}\\
\tdom(g \circ (\tdom f)) &= (\tdom g) \circ (\tdom f)\tag*{(R3)}\\
(\tdom h) \circ f &= f \circ \tdom (h \circ f)\tag*{(R4)}
f \circ (\tdom f) &= f\tag*{(R1)}\label{R1}\\
(\tdom f) \circ (\tdom g) &= (\tdom g) \circ (\tdom f)\tag*{(R2)}\label{R2}\\
\tdom(g \circ (\tdom f)) &= (\tdom g) \circ (\tdom f)\tag*{(R3)}\label{R3}\\
(\tdom h) \circ f &= f \circ \tdom (h \circ f)\tag*{(R4)}\label{R4}
\end{alignat*}
for any $X, Y, Z \in \vert\mathcal{C}\vert, f : X \rightarrow Y, g : X \rightarrow Z, h: Y \rightarrow Z$.
\end{definition}
\todo[inline]{be more precise}
Intuitively $\tdom f$ captures the domain of definiteness of $f$.
\begin{lemma}
For any $f : X \rightarrow Y$ the restriction $\tdom f$ is idempotent.
\end{lemma}
\begin{proof}
This follows by \ref{R3} and \ref{R1}:
\[\tdom f \circ \tdom f = \tdom (f \circ \tdom f) = \tdom f\]
\end{proof}
The idempotent morphism $\tdom f : X \rightarrow X$ represents the domain of definiteness of $f : X \rightarrow Y$. In the category of partial functions this takes the following form:
\[
(\tdom f)(x) = \begin{cases}
x & \text{if } f(x) \text{ is defined}\\
\text{undefined} & \text{else}
\end{cases}
\]
That is, $\tdom f$ is only defined on values where $f$ is defined and for those values it behaves like the identity function.
\begin{definition}[Restriction Category]
Every category has a trivial restriction structure by taking $dom (f : X \rightarrow Y) = id_X$.
We call categories with a non-trivial restriction structure \textit{restriction categories}.
\end{definition}
A suitably defined partiality monad $T$ should then have the property that $\mathcal{C}^T$ is a restriction category.
For a suitable defined partiality monad $T$ the Kleisli category $\C^T$ should be a restriction category.
Lastly we also recall the following notion by Bucalo et al.~\cite{eqlm} which captures what it means for a monad to have no other side effect besides some sort of non-termination:
@ -57,12 +74,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}
\todo[inline]{proof?}
\begin{theorem}[no proof]
Let $T$ be an equational lifting monad, then $\mathcal{C}^T$ is a restriction category~\cite{eqlm}.
\begin{theorem}[\cite{eqlm}]
If $T$ is an equational lifting monad the Kleisli category $\mathcal{C}^T$ is a restriction category.
\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 compare 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 monads that are commonly used to model partiality.
\section{The Maybe Monad}
The endofunctor $MX = X + 1$ extends to a monad by taking $\eta_X = i_1 : X \rightarrow X + 1$ and $\mu_X = [ id , i_2 ] : (X + 1) + 1 \rightarrow X + 1$. 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:
@ -73,7 +89,7 @@ The endofunctor $MX = X + 1$ extends to a monad by taking $\eta_X = i_1 : X \rig
We define strength as:
\[ \tau_{X,Y} := X \times (Y + 1) \overset{dstl}{\longrightarrow} (X \times Y) + (X \times 1) \overset{id+!}{\longrightarrow} (X \times Y) + 1 \]
naturality of $\tau$ follows by naturality of dstl:
Naturality of $\tau$ follows by naturality of $dstl$:
\begin{alignat*}{1}
&(id + !) \circ dstl \circ (id \times (f + id))\\
@ -81,7 +97,8 @@ The endofunctor $MX = X + 1$ extends to a monad by taking $\eta_X = i_1 : X \rig
= \;&((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.
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.
We are left to check the equational lifting law:
% https://q.uiver.app/#q=WzAsNCxbMCwwLCJYKzEiXSxbMywwLCIoWCsxKVxcdGltZXMoWCsxKSJdLFszLDIsIigoWCsxKVxcdGltZXMgWCkgKygoWCsxKVxcdGltZXMgMSkiXSxbMyw0LCIoKFgrMSlcXHRpbWVzIFgpKzEiXSxbMCwxLCJcXERlbHRhIl0sWzEsMiwiZHN0bCJdLFsyLDMsImlkK1xcOyEiXSxbMCwzLCJcXGxhbmdsZSBpXzEsaWRcXHJhbmdsZSArIFxcOyEiLDJdXQ==
@ -100,20 +117,21 @@ The endofunctor $MX = X + 1$ extends to a monad by taking $\eta_X = i_1 : X \rig
\[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
which follow easily by the facts that
\[dstl \circ (id \times i_1) = i_1\]
and
\[dstl \circ (id \times i_2) = i_2\]
that are both proven by monicity of $dstl^{-1}$.
\end{proof}
In the setting of classical mathematics this monad is therefore sufficient for modelling partiality, but in general it will not be useful for modelling 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 Capretta~\cite{delay}.
\section{The Delay Monad}
\todo[inline]{Take introduction from setoids chapter and put it here!}
Capretta's delay monad~\cite{delay} is a coinductive datatype whose inhabitants can be viewed as suspended computations.
This monad 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:
\todo[inline]{Explain coinduction in introduction or here?}
\todo[inline]{Explain convention of double lines vs single lines}
\todo[inline]{Explain convention of double lines vs single lines ==> remove double lines here!!}
\[\mprset{fraction={===}}
\inferrule {x : X} {now\; x : DX}\hskip 2cm
@ -163,7 +181,7 @@ Since $DX$ is defined as a final coalgebra, we can define morphisms via corecurs
\begin{itemize}
\item[\ref{D1}] This follows by definition of $now$.
\item[\ref{D2}] We define $f^* = \;! \circ i_1$, where $!$ is the unique coalgebra morphism in this diagram:
\todo[inline]{Use other name than '!' for unique morphism}
\todo[inline]{Use other name than '!' for unique morphism => semantic brackets!}
% https://q.uiver.app/#q=WzAsNSxbMCwxLCJEWCArIERZIl0sWzcsMSwiWSArIChEWCArIERZKSJdLFswLDAsIkRYIl0sWzAsMiwiRFkiXSxbNywyLCJZICsgRFkiXSxbMCwxLCJbIFsgWyBpXzEgLCBpXzIgXFxjaXJjIGlfMiBdIFxcY2lyYyAob3V0IFxcY2lyYyBmKSAsIGlfMiBcXGNpcmMgaV8xIF0gXFxjaXJjIG91dCAsIChpZCArIGlfMikgXFxjaXJjIG91dCBdIl0sWzIsMCwiaV8xIl0sWzAsMywiISIsMCx7InN0eWxlIjp7ImJvZHkiOnsibmFtZSI6ImRhc2hlZCJ9fX1dLFszLDQsIm91dCJdLFsxLDQsImlkICsgISIsMCx7InN0eWxlIjp7ImJvZHkiOnsibmFtZSI6ImRhc2hlZCJ9fX1dXQ==
\[\begin{tikzcd}

6
thesis/src/05_setoids.tex
View file

@ -116,7 +116,7 @@ codata (A : Set) : Set where
This style is sometimes called \textit{positively coinductive} and is nowadays advised against in the manuals of both Agda and Coq\todo{cite}. Instead, one is advised to use coinductive records, we will heed this advice and use the following representation of the delay monad in Agda:\change{rephrase}
\todo[inline]{cite https://www.cse.chalmers.se/~nad/listings/delay-monad/Delay-monad.html somehow}
\todo[inline]{Cite https://www.cse.chalmers.se/~nad/listings/delay-monad/Delay-monad.html somehow}
\cite{nad-delay}
\begin{minted}{agda}
mutual
@ -150,7 +150,7 @@ We will now introduce two notions of equality on inhabitants of the delay type,
$(Delay\;A, \sim)$ is a setoid.
\end{lemma}
In $(Delay\;A, \sim)$ computations that evaluate to the same result but in a different amount of time are not equal. We will now quotient this type by weak bisimilarity, i.e. we will identify all computations that terminate with the same result. Let us first consider what it means for a computation to evaluate to some result:
In $(Delay\;A, \sim)$ computations that evaluate to the same result but in a different amount of time are not equal. We will now build the quotient of this type by weak bisimilarity, i.e. we will identify all computations that terminate with the same result. Let us first consider what it means for a computation to evaluate to some result:
\[
\inferrule*{eq : x =^A y}{now\; eq : now\;x \downarrow y} \hskip 1cm
@ -182,7 +182,7 @@ Now we can relate two computations \textit{iff} they evaluate to the same result
force (μ' x) = μ (force x)
\end{minted}
The monad laws have already been proven in~\cite{quotienting} and in our own formalization so we will not reiterate the proofs here.
The monad laws have already been proven in~\cite{quotienting} and in our own formalization, so we will not reiterate the proofs here.
\end{proof}
\begin{theorem}