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

Work on TODOs

Browse source
This commit is contained in:
Leon Vatthauer 2024-03-13 13:26:38 +01:00
parent 50c98dc642
commit fe0dcc44a8
Signed by: leonv
SSH key fingerprint: SHA256:G4+ddwoZmhLPRB1agvXzZMXIzkVJ36dUYZXf5NxT+u8
12 changed files with 257 additions and 197 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -1,2 +1,4 @@
Agda
Vatthauer
Moggi
Capretta

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

@ -68,3 +68,6 @@ Set₀
Set₁
bisimilar
copatterns
epimorphisms
monomorphisms
expressivity

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

@ -2,3 +2,4 @@
{"rule":"WHITESPACE_RULE","sentence":"^\\Q[4][]##4\\E$"}
{"rule":"MORFOLOGIK_RULE_EN_GB","sentence":"^\\Q[ignoreall,show=definition]\\E$"}
{"rule":"COMMA_PARENTHESIS_WHITESPACE","sentence":"^\\Q[ignoreall,show=definition]\\E$"}
{"rule":"MORFOLOGIK_RULE_EN_GB","sentence":"^\\Q[1]Coalgs(#1)\\E$"}

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

@ -32,3 +32,10 @@
{"rule":"UPPERCASE_SENTENCE_START","sentence":"^\\Qlaw:compositionality Compositionality: \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q for \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q law:stutter Stutter: \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q for \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q law:diamond Diamond: \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q for \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q: First, note that \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q can equivalently be reformulated as \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q since \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q Using \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q, we are left to show that \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q.\\E$"}
{"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]+$"}
{"rule":"IF_IS","sentence":"^\\Q\\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q if \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q if \\E(?:Dummy|Ina|Jimmy-)[0-9]+$"}
{"rule":"ENGLISH_WORD_REPEAT_RULE","sentence":"^\\QA (unguarded) Elgot Algebra \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q consists of: An object A for every \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q an iteration \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q, satisfying: law:fixpoint Fixpoint: \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q for \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q law:uniformity Uniformity: \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q for \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q law:folding Folding: \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q for \\E(?:Dummy|Ina|Jimmy-)[0-9]+$"}
{"rule":"ENGLISH_WORD_REPEAT_RULE","sentence":"^\\Qlaw:compositionality Compositionality: \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q for any \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q, law:stutter Stutter: \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q for any \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q, law:diamond Diamond: \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q for any \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q.\\E$"}
{"rule":"ENGLISH_WORD_REPEAT_RULE","sentence":"^\\QA (unguarded) Elgot Algebra \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q consists of: An object \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q, and for every \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q an iteration \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q, satisfying: law:fixpoint Fixpoint: \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q for any \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q, law:uniformity Uniformity: \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q implies \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q for any \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q, law:folding Folding: \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q for any \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q.\\E$"}
{"rule":"ENGLISH_WORD_REPEAT_RULE","sentence":"^\\QA (unguarded) Elgot Algebra \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q consists of: An object \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q, and for every \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q an iteration \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q, satisfying the following axioms: law:fixpoint Fixpoint: \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q for any \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q, law:uniformity Uniformity: \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q implies \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q for any \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q, law:folding Folding: \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q for any \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q.\\E$"}
{"rule":"MORFOLOGIK_RULE_EN_US","sentence":"^\\QGiven a functor \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q, a (H-)guarded Elgot algebra consists of: An object \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q, a H-algebra structure \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q, and for every \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q an iteration \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q, satisfying the following axioms: law:guardedfixpoint Fixpoint: \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q for any \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q, law:guardeduniformity Uniformity: \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q implies \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q for any \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q, law:guardedcompositionality Compositionality: \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q for any \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q.\\E$"}
{"rule":"UPPERCASE_SENTENCE_START","sentence":"^\\Qlaw:compositionality Compositionality: \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q for any \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q, law:stutter Stutter: \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q for any \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q, law:diamond Diamond: \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q for any \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q.\\E$"}
{"rule":"MORFOLOGIK_RULE_EN_US","sentence":"^\\QAn Elgot monad consists of A monad \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q, for every \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q an iteration \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q satisfying: Fixpoint: \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q for any \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q, Uniformity: \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q implies \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q for any \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q, Naturality: \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q for any \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q, Codiagonal: \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q for any \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q.\\E$"}

128
thesis/bib.bib
View file

@ -5,41 +5,6 @@
version = {2.6.5}
}
@manual{agda-man,
title = {Agda User Manual},
author = {The Agda Team},
year = {2024},
month = {03},
day = {06},
version = {2.6.4.3},
url = {https://agda.readthedocs.io/en/v2.6.4.3/}
}
@manual{coq-man,
title = {The Coq Reference Manual},
author = {The Coq Development Team},
year = {2024},
month = {03},
day = {01},
version = {8.19.1},
url = {https://coq.inria.fr/doc/V8.19.0/refman/}
}
@article{setoids,
title = {Category theoretic structure of setoids},
journal = {Theoretical Computer Science},
volume = {546},
pages = {145-163},
year = {2014},
note = {Models of Interaction: Essays in Honour of Glynn Winskel},
issn = {0304-3975},
doi = {https://doi.org/10.1016/j.tcs.2014.03.006},
url = {https://www.sciencedirect.com/science/article/pii/S0304397514001819},
author = {Yoshiki Kinoshita and John Power},
keywords = {Setoid, Proof assistant, Proof irrelevance, Cartesian closed category, Coproduct, -category, -inserter, -category, -coinserter},
abstract = {A setoid is a set together with a constructive representation of an equivalence relation on it. Here, we give category theoretic support to the notion. We first define a category Setoid and prove it is Cartesian closed with coproducts. We then enrich it in the Cartesian closed category Equiv of sets and classical equivalence relations, extend the above results, and prove that Setoid as an Equiv-enriched category has a relaxed form of equalisers. We then recall the definition of E-category, generalising that of Equiv-enriched category, and show that Setoid as an E-category has a relaxed form of coequalisers. In doing all this, we carefully compare our category theoretic constructs with Agda code for type-theoretic constructs on setoids.}
}
@inproceedings{agda-categories,
author = {Hu, Jason Z. S. and Carette, Jacques},
title = {Formalizing Category Theory in Agda},
@ -58,6 +23,16 @@
series = {CPP 2021}
}
@manual{agda-man,
title = {Agda User Manual},
author = {The Agda Team},
year = {2024},
month = {03},
day = {06},
version = {2.6.4.3},
url = {https://agda.readthedocs.io/en/v2.6.4.3/}
}
@software{agda-stdlib,
author = {{The Agda Community}},
month = dec,
@ -78,6 +53,16 @@
booktitle = {Lecture Notes in Computer Science}
}
@manual{coq-man,
title = {The Coq Reference Manual},
author = {The Coq Development Team},
year = {2024},
month = {03},
day = {01},
version = {8.19.1},
url = {https://coq.inria.fr/doc/V8.19.0/refman/}
}
@article{delay,
author = {Venanzio Capretta},
title = {General Recursion via Coinductive Types},
@ -142,6 +127,24 @@
keywords = {premonoidal categories, categories, partiality and partial categories, abstract Kleish, commutative strong monads}
}
@inproceedings{goncharov2017unifying,
title = {Unifying guarded and unguarded iteration},
author = {Goncharov, Sergey and Schr{\"o}der, Lutz and Rauch, Christoph and Pir{\'o}g, Maciej},
booktitle = {Foundations of Software Science and Computation Structures: 20th International Conference, FOSSACS 2017, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2017, Uppsala, Sweden, April 22-29, 2017, Proceedings 20},
pages = {517--533},
year = {2017},
organization = {Springer}
}
@article{goncharov2018unguarded,
title = {Unguarded recursion on coinductive resumptions},
author = {Goncharov, Sergey and Schr{\"o}der, Lutz and Rauch, Christoph and Jakob, Julian},
journal = {Logical Methods in Computer Science},
volume = {14},
year = {2018},
publisher = {Episciences. org}
}
@book{inductive,
title = {Categorical programming with inductive and coinductive types},
author = {Vene, Varmo},
@ -149,6 +152,17 @@
publisher = {Citeseer}
}
@article{kozencoinduction,
title = {Practical coinduction},
author = {Kozen, Dexter and Silva, Alexandra},
journal = {Mathematical Structures in Computer Science},
volume = {27},
number = {7},
pages = {1132--1152},
year = {2017},
publisher = {Cambridge University Press}
}
@article{lambek,
title = {A fixpoint theorem for complete categories},
author = {Lambek, Joachim},
@ -166,6 +180,15 @@
url = {https://api.semanticscholar.org/CorpusID:122892655}
}
@article{manes,
title = {Algebraic Theories in a Category},
author = {Manes, Ernest G},
journal = {Algebraic Theories},
pages = {161--279},
year = {1976},
publisher = {Springer}
}
@article{moggi,
author = {Moggi, Eugenio},
title = {Notions of Computation and Monads},
@ -242,6 +265,21 @@
numpages = {37}
}
@article{setoids,
title = {Category theoretic structure of setoids},
journal = {Theoretical Computer Science},
volume = {546},
pages = {145-163},
year = {2014},
note = {Models of Interaction: Essays in Honour of Glynn Winskel},
issn = {0304-3975},
doi = {https://doi.org/10.1016/j.tcs.2014.03.006},
url = {https://www.sciencedirect.com/science/article/pii/S0304397514001819},
author = {Yoshiki Kinoshita and John Power},
keywords = {Setoid, Proof assistant, Proof irrelevance, Cartesian closed category, Coproduct, -category, -inserter, -category, -coinserter},
abstract = {A setoid is a set together with a constructive representation of an equivalence relation on it. Here, we give category theoretic support to the notion. We first define a category Setoid and prove it is Cartesian closed with coproducts. We then enrich it in the Cartesian closed category Equiv of sets and classical equivalence relations, extend the above results, and prove that Setoid as an Equiv-enriched category has a relaxed form of equalisers. We then recall the definition of E-category, generalising that of Equiv-enriched category, and show that Setoid as an E-category has a relaxed form of coequalisers. In doing all this, we carefully compare our category theoretic constructs with Agda code for type-theoretic constructs on setoids.}
}
@article{setoids,
author = {Barthe, Gilles and Capretta, Venanzio and Pons, Olivier},
title = {Setoids in type theory},
@ -310,23 +348,3 @@
biburl = {https://dblp.org/rec/journals/corr/GoncharovSR14.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@article{manes,
title = {Algebraic Theories in a Category},
author = {Manes, Ernest G},
journal = {Algebraic Theories},
pages = {161--279},
year = {1976},
publisher = {Springer}
}
@article{kozencoinduction,
title = {Practical coinduction},
author = {Kozen, Dexter and Silva, Alexandra},
journal = {Mathematical Structures in Computer Science},
volume = {27},
number = {7},
pages = {1132--1152},
year = {2017},
publisher = {Cambridge University Press}
}

29
thesis/main.tex
View file

@ -24,7 +24,7 @@
\usepackage{mathpartir}
% packages for draft version
\usepackage{lineno}
\usepackage[colorinlistoftodos,prependcaption,textsize=tiny,obeyDraft]{todonotes}
\usepackage[colorinlistoftodos,prependcaption,textsize=tiny]{todonotes}
\usepackage{ifdraft}
% mathpartir uses \atop, amsmath overrides it to throw a warning tho, so we override it back to the original!
@ -57,6 +57,9 @@
%\usepackage[justific=raggedright,totoc]{idxlayout}
\usepackage[type=CC, modifier=by-sa,version=4.0]{doclicense}
% autoref for minted listings
\providecommand*{\listingautorefname}{Listing}
\addto\extrasenglish{
\renewcommand{\chapterautorefname}{Section}
\renewcommand{\sectionautorefname}{Section}
@ -105,16 +108,11 @@
\usepackage[scale=.8]{noto-mono}
% \usepackage{noto}
% TODO Need different mono font, noto-mono has weird font sizing...
\usepackage{unicode-math}
% \setmainfont{STIX-Regular}
% \setmathfont{STIX Two Math Regular}
\usepackage{mathrsfs}
\usepackage{xargs}
\usepackage{xstring}
\usepackage{accents} % provides \accentset
\newcommand*{\dbtilde}[1]{\tilde{\raisebox{0pt}[0.85\height]{\(\tilde{#1}\)}}}
@ -130,6 +128,7 @@
% category of elgot algebras on #1
\newcommand*{\elgotalgs}[1]{\ensuremath{\mathit{ElgotAlgs}(#1)}}
% category of monads on #1
\newcommand*{\coalgs}[1]{\ensuremath{\mathit{Coalgs}(#1)}}
\newcommand*{\monads}[1]{\ensuremath{\mathit{Monads}(#1)}}
\newcommand*{\strongmonads}[1]{\ensuremath{\mathit{StrongMonads}(#1)}}
% category of pre-Elgot monads on #1
@ -203,11 +202,16 @@
\phantom{Erlangen, \today{}} \theauthor{}
\end{german}
\chapter*{Licensing}
\doclicenseThis{}
% \chapter*{Licensing}
% \doclicenseThis{}
\chapter*{Abstract}
\todo[inline]{abstract}
Moggi famously showed how to use category theory (specifically monads) to model the semantics of effectful computations.
In this thesis we want to specifically examine how to model possibly non-terminating computations, which requires a monad supporting some form of partiality.
For that we will consider categorical properties that a monad that models partiality should satisfy and then compare concrete monads in view of these properties.
Capretta's delay monad is a typical example for a partiality monad, but it comes with a too intensional notion of built-in equality.
Since fixing this seems to be impossible without additional axioms, we will look at a novel approach to defining a partiality monad that works in a general setting by making use of previous research on iteration theories and drawing on the inherent connection between partiality and iteration. Lastly, we will see that in the category of setoids this partiality monad instantiates to a quotient of the delay monad.
\tableofcontents
@ -229,7 +233,6 @@
\ifdraft{\linenumbers}
% \include{src/examples}
\include{src/00_introduction}
\include{src/01_preliminaries}
\include{src/02_agda-categories}
@ -238,18 +241,12 @@
\include{src/05_setoids}
\include{src/10_conclusion}
\todo[inline]{Symbolverzeichnis, siehe: https://www.namsu.de/Extra/pakete/Listofsymbols.pdf}
\todo[inline]{Add fullstop behind every proof}
\todo[inline]{ (Re-) move list of definitions}
\appendix
% \include{src/A1_contributions}
\medskip
\printbibliography[heading=bibintoc]{}
% https://tex.stackexchange.com/questions/74857/toc-like-list-of-definitions-using-theorem-environments
% \renewcommand*{\listtheoremname}{List of Definitions}
% \listoftheorems[ignoreall,show={definition}]
\end{document}

5
thesis/src/00_introduction.tex
View file

@ -2,9 +2,4 @@
\section{Motivation}
\info[inline]{Use introductory example from talk}
\section{Type Theory}
\unsure[inline]{Talk about (co)induction?} % chktex 36
\todo[inline]{Give overview of thesis}

136
thesis/src/01_preliminaries.tex
View file

@ -1,6 +1,6 @@
\chapter{Preliminaries}
We assume familiarity with basic categorical notions, in particular: categories, functors, functor algebras and natural transformations, as well as special objects like (co)products, terminal and initial objects and special morphisms like isos, epis and monos. % chktex 36
We assume familiarity with basic categorical notions, in particular: categories, functors, functor algebras and natural transformations, as well as special objects like (co)products, terminal and initial objects and special classes of morphisms like isomorphisms (isos), epimorphisms (epis) and monomorphisms (monos). % chktex 36
In this chapter we will introduce notation that will be used throughout the thesis and also introduce some notions that are crucial to this thesis in more detail.
We write \(\obj{C}\) for the objects of a category \( \C \), \(id_X\) for the identity morphism on \(X\), \((-) \circ (-)\) for the composition of morphisms and \(\C(X,Y)\) for the set of morphisms between \(X\) and \(Y\).
We will also sometimes omit indices of the identity and of natural transformations in favor of readability.
@ -34,10 +34,10 @@ We will furthermore overload this notation and write \(f \times g := \langle f \
We write \(1\) for the terminal object together with the unique morphism \(! : A \rightarrow 1\) and \(0\) for the initial object with the unique morphism \(¡ : A \rightarrow 0\).
Categories with finite products (i.e.\ binary products and a terminal object) are also called Cartesian and categories with finite coproducts (i.e.\ binary coproducts and an initial object) are called cocartesian.
Categories with finite products (i.e.\ binary products and a terminal object) are also called Cartesian and categories with finite coproducts (i.e.\ binary coproducts and an initial object) are called coCartesian.
\begin{definition}[Distributive Category]~\label{def:distributive}
A Cartesian and cocartesian category \(\C \) is called distributive if the canonical (left) distributivity morphism \(dstl^{-1}\) is an iso:
A Cartesian and coCartesian category \(\C \) is called distributive if the canonical (left) distributivity morphism \(dstl^{-1}\) is an iso:
% https://q.uiver.app/#q=WzAsMixbMCwwLCJYIFxcdGltZXMgWSArIFggXFx0aW1lcyBaIl0sWzMsMCwiWCBcXHRpbWVzIChZICsgWikiXSxbMCwxLCJkc3RsXnstMX0gOj0ge1xcbGJyYWNrIGlkIFxcdGltZXMgaV8xICwgaWQgXFx0aW1lcyBpXzIgXFxyYnJhY2t9IiwwLHsiY3VydmUiOi0zfV0sWzEsMCwiZHN0bCIsMCx7ImN1cnZlIjotM31dXQ==
\[
\begin{tikzcd}
@ -198,17 +198,17 @@ Categories with finite products (i.e.\ binary products and a terminal object) ar
\end{proof}
A Cartesian closed category is a Cartesian category \(\C \) that also has an exponential object \(X^Y\) for any \(X, Y \in \obj{\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.
The internal logic of Cartesian closed categories is the simply typed \(\lambda \)-calculus, which makes them a suitable environment for interpreting programming languages. For the rest of this thesis we will work in an ambient distributive category that however need not be Cartesian closed as to be more general.
\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 modeling 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 an F-coalgebra.
A tuple \((X \in \obj{\C}, \alpha : X \rightarrow FX)\) is called an \emph{F-coalgebra} (hereafter referred to as just \emph{coalgebra}).
\end{definition}
\begin{definition}[Morphisms between Coalgebras]\label{def:coalgmorph}
Let \((X \in \obj{\C} , \alpha : X \rightarrow FX)\) and \((Y \in \obj{\C} , \beta : Y \rightarrow FY)\) be two F-coalgebras. A morphism between these coalgebras is a morphism \(f : X \rightarrow Y\) such that the following diagram commutes:
\begin{definition}[Coalgebra Morphisms]\label{def:coalgmorph}
Let \((X \in \obj{\C} , \alpha : X \rightarrow FX)\) and \((Y \in \obj{\C} , \beta : Y \rightarrow FY)\) be two coalgebras. A morphism between these coalgebras is a morphism \(f : X \rightarrow Y\) such that the following diagram commutes:
% https://q.uiver.app/#q=WzAsNCxbMCwwLCJYIl0sWzAsMiwiWSJdLFsyLDAsIkZYIl0sWzIsMiwiRlkiXSxbMSwzLCJcXGJldGEiXSxbMCwyLCJcXGFscGhhIl0sWzAsMSwiZiIsMl0sWzIsMywiRmYiXV0=
\[
\begin{tikzcd}[ampersand replacement=\&]
@ -224,15 +224,15 @@ Let \(F : \C \rightarrow \C \) be an endofunctor. Recall that F-algebras are tup
\end{definition}
\todo[inline]{Adopt text, lemma style}
Coalgebras together with their morphisms form a category that we call \(\coalgs{F}\).
\begin{proposition}
F-coalgebras together with their morphisms form a category that we call \(Coalg(F)\).
\(\coalgs{F}\) is a category.
\end{proposition}
\begin{proof}
Let \((X , \alpha : X \rightarrow FX)\) be an F-coalgebra. The identity morphism on \((X , \alpha)\) is the identity morphism of \(\C \) that trivially satisfies \(\alpha \circ id = Fid \circ \alpha \).
Let \((X , \alpha : X \rightarrow FX)\) be a coalgebra. The identity morphism on \((X , \alpha)\) is the identity morphism of \(\C\) that trivially satisfies \(\alpha \circ id = Fid \circ \alpha \).
Let \((X , \alpha : X \rightarrow FX), (Y, \beta : Y \rightarrow FY)\) and \((Z , \gamma : Z \rightarrow FZ)\) be F-coalgebras.
Let \((X , \alpha : X \rightarrow FX), (Y, \beta : Y \rightarrow FY)\) and \((Z , \gamma : Z \rightarrow FZ)\) be coalgebras.
Composition of \(f : (X, \alpha) \rightarrow (Y, \beta)\) and \(g : (Y, \beta) \rightarrow (Z, \gamma)\) is composition of the underlying morphisms in \(\C \) where:
\begin{alignat*}{1}
& \gamma \circ g \circ f \\
@ -242,10 +242,10 @@ Let \(F : \C \rightarrow \C \) be an endofunctor. Recall that F-algebras are tup
\end{alignat*}
\end{proof}
The terminal object of \(Coalg(F)\) is sometimes called \textit{final F-coalgebra}, we will however call it the \textit{terminal F-coalgebra} for consistency with initial F-algebras. Similarly to initial F-algebras, the final F-coalgebra can be used for modeling 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:
The terminal object of \(\coalgs{F}\) is sometimes called \textit{final coalgebra}, we will however call it the \textit{terminal coalgebra} for consistency with initial F-algebras. Similarly to initial F-algebras, the final coalgebra can be used for modeling 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 coalgebras concrete:
\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{definition}[Terminal Coalgebra]
A coalgebra \((T, t : T \rightarrow FT)\) is called a terminal coalgebra if for any other coalgebra \((X, \alpha : X \rightarrow FX)\) there exists a unique morphism \(\coalg{\alpha} : X \rightarrow T\) satisfying:
% https://q.uiver.app/#q=WzAsNCxbMCwwLCJYIl0sWzIsMCwiRlgiXSxbMCwyLCJUIl0sWzIsMiwiRlQiXSxbMCwxLCJcXGFscGhhIl0sWzIsMywidCJdLFswLDIsIlxcbGxicmFja2V0IFxcYWxwaGEgXFxycmJyYWNrZXQiLDIseyJzdHlsZSI6eyJib2R5Ijp7Im5hbWUiOiJkYXNoZWQifX19XSxbMSwzLCJGXFxsbGJyYWNrZXQgXFxhbHBoYSBcXHJyYnJhY2tldCJdXQ==
\[
@ -263,8 +263,8 @@ The terminal object of \(Coalg(F)\) is sometimes called \textit{final F-coalgebr
We will discuss the concrete form that induction and coinduction take in a type theory in \autoref{chp:agda-cat}. Let us now reiterate a famous Lemma concerning terminal F-coalgebras.
\begin{lemma}[Lambek's Lemma~\cite{lambek}]
Let \((T, t : T \rightarrow FT)\) be a terminal F-coalgebra. Then \(t\) is an isomorphism.
\begin{lemma}[Lambek's Lemma~\cite{lambek}]\label{lem:lambek}
Let \((T, t : T \rightarrow FT)\) be a terminal coalgebra. Then \(t\) is an isomorphism.
\end{lemma}
% \begin{proof}
% First note that \((FT, Ft : FT \rightarrow FFT)\) is also an F-coalgebra. This yields the unique morphism \(\coalg{Ft} : FT \rightarrow T\) satisfying:
@ -305,7 +305,7 @@ We will discuss the concrete form that induction and coinduction take in a type
% \end{proof}
\section{Monads}
Monads are widely known among programmers as a way of modeling effects in pure languages and are also central to this thesis. Let us recall the basic definitions\cite{Lane1971}\cite{moggi}.
Monads are widely known in functional programming as a means for modeling effects in pure languages and are also central to this thesis. Let us recall the basic definitions\cite{Lane1971}\cite{moggi}.
\begin{definition}[Monad]
A monad \(\mathbf{T}\) on a category \(\C \) is a triple \((T, \eta, \mu)\), where \(T : \C \rightarrow \C \) is an endofunctor and \(\eta : Id \rightarrow T, \mu : TT \rightarrow T\) are natural transformations, satisfying the following laws:
@ -336,11 +336,7 @@ Monads are widely known among programmers as a way of modeling effects in pure l
\]
\end{definition}
As with many categorical concepts we may consider the category of monads:
\todo[inline]{Use text => lemma style}
\begin{definition}[The Category of Monads]~\label{def:monads}
Let \(\C \) be a category.
\begin{definition}[Monad Morphism]\label{def:monadmorphism}
A morphism between monads \((S : \C \rightarrow \C, \eta^S, \mu^S)\) and \((T : \C \rightarrow \C, \eta^T, \mu^T)\) is a natural transformation \(\alpha : S \rightarrow T\) between the underlying functors satisfying:
% https://q.uiver.app/#q=WzAsOCxbMCwwLCJYIl0sWzIsMCwiU1giXSxbMiwxLCJUWCJdLFszLDAsIlNTWCJdLFs1LDAsIlNUWCJdLFszLDEsIlNYIl0sWzcsMCwiVFRYIl0sWzcsMSwiVFgiXSxbMCwxLCJcXGV0YV5TIl0sWzEsMiwiXFxhbHBoYSJdLFswLDIsIlxcZXRhXlQiLDJdLFszLDQsIlNcXGFscGhhIl0sWzMsNSwiXFxtdV5TIiwyXSxbNCw2LCJcXGFscGhhIl0sWzUsNywiXFxhbHBoYSIsMl0sWzYsNywiXFxtdV5UIl1d
\[
@ -357,10 +353,17 @@ As with many categorical concepts we may consider the category of monads:
\arrow["{\mu^T}", from=1-8, to=2-8]
\end{tikzcd}
\]
This yields the category of monads on \(\C \) which we call \(\monads{\C}\). The identity morphism of \(\monads{\C}\) is the identity natural transformation \(Id : F \rightarrow F\) which trivially respects the monad unit and multiplication. Composition of monad morphisms is composition of the underlying natural transformation, the diagrams then also follow easily.
\end{definition}
This yields a category of monads on a given category \(\C\) that we call \(\monads{\C}\).
\begin{proposition}\label{prop:monadscat}
\(\monads{\C}\) is a category.
\end{proposition}
\begin{proof}
The identity morphism of \(\monads{\C}\) is the identity natural transformation \(Id : F \rightarrow F\) which trivially respects the monad unit and multiplication. Composition of monad morphisms is composition of the underlying natural transformation, the diagrams then also follow easily.
\end{proof}
Monads can also be specified in a second equivalent way that is better suited to describe computation.
\begin{definition}[Kleisli Triple]
@ -378,7 +381,7 @@ Let \(f : X \rightarrow TY, g : Y \rightarrow TZ\) be two programs, where \(T\)
f y
\end{minted}
The possibility of Kleisli composition enables us to define the category of programs for any Kleisli triple \(T\).
This yields the category of programs for a Kleisli triple that is called the Kleisli category.
\begin{definition}[Kleisli Category]
Given a monad \(T\) on a category \(\C \), the Kleisli category \(\C^T\) is defined as:
@ -411,7 +414,44 @@ The possibility of Kleisli composition enables us to define the category of prog
For the rest of this thesis we will use both equivalent notions interchangeably to make definitions easier.
\section{Strong and Commutative Monads}
When modeling partiality with a monad, one would expect the following two programs to be equivalent
Consider the following program in do-notation
\begin{minted}{haskell}
do y <- g x
f (x , y)
\end{minted}
where \(g : X \rightarrow TY\) and \(f : X \times Y \rightarrow TZ\) are programs and \(\mathbf{T}\) is a monad. Kleisli composition does not suffice for interpreting this program, we will get stuck at
\[X \overset{\langle id , g \rangle}{\longrightarrow} X \times TY \overset{?}{\longrightarrow} T(X \times Y) \overset{f^*}{\longrightarrow} TZ. \]
Which motivates the following notion.
\begin{definition}[Strong Monad] A monad \((T, \eta, \mu)\) on a Cartesian category \(\C \) is called strong if there exists a natural transformation \(\tau_{X,Y} : X \times TY \rightarrow T(X \times Y)\) that satisfies the following conditions:
\begin{alignat*}{2}
& T\pi_2 \circ \tau_{1,X} & & = \pi_2 \tag*{(S1)}\label{S1} \\
& \tau_{X,Y} \circ (id_X \times \eta_Y) & & = \eta_{X\times Y} \tag*{(S2)}\label{S2} \\
& \tau_{X,Y} \circ (id_X \times \mu_Y) & & = \mu_{X\times Y} \circ T\tau_{X,Y} \circ \tau_{X,TY} \tag*{(S3)}\label{S3} \\
& M \alpha_{X,Y,Z} \circ \tau_{X \times Y, Z} & & = \tau_{X, Y\times Z} \circ (id_X \times \tau_{Y, Z}) \circ \alpha_{X,Y,TZ} \tag*{(S4)}\label{S4}
\end{alignat*}
where \(\alpha_{X,Y,Z} = \langle \langle \pi_1 , \pi_1 \circ \pi_2 \rangle , \pi_2 \circ \pi_2 \rangle : X \times (Y \times Z) \rightarrow (X \times Y) \times Z\) is the associativity morphism on products.
\end{definition}
\begin{definition}[Strong Monad Morphism]\label{def:strongmonadmorphism}
A morphism between two strong monads \((S : \C \rightarrow \C, \eta^S, \mu^S, \tau^S)\) and \((T : \C \rightarrow \C, \eta^T, \mu^T, \tau^T)\) is a morphism between monads as in \autoref{def:monadmorphism} that additionally satisfies:
% https://q.uiver.app/#q=WzAsNCxbMCwwLCJYIFxcdGltZXMgU1kiXSxbMCwyLCJTKFggXFx0aW1lcyBZKSJdLFsyLDIsIlQoWCBcXHRpbWVzIFkpIl0sWzIsMCwiWCBcXHRpbWVzIFRZIl0sWzAsMSwiXFx0YXVeUyJdLFsxLDIsIlxcYWxwaGEiXSxbMCwzLCJpZCBcXHRpbWVzIFxcYWxwaGEiXSxbMywyLCJcXHRhdV5UIiwyXV0=
\[
\begin{tikzcd}[ampersand replacement=\&]
{X \times SY} \&\& {X \times TY} \\
\\
{S(X \times Y)} \&\& {T(X \times Y)}
\arrow["{\tau^S}", from=1-1, to=3-1]
\arrow["\alpha", from=3-1, to=3-3]
\arrow["{id \times \alpha}", from=1-1, to=1-3]
\arrow["{\tau^T}"', from=1-3, to=3-3]
\end{tikzcd}
\]
\end{definition}
As with monads this yields a category of strong monads on \(\C\) that we call \(\strongmonads{\C}\).
Let us now consider the following two programs
\begin{multicols}{2}
\begin{minted}{haskell}
do x <- p
@ -425,40 +465,8 @@ When modeling partiality with a monad, one would expect the following two progra
return (x, y)
\end{minted}
\end{multicols}
Where p and q are (partial) computations. This condition can be expressed categorically, but first we need another definition:
Where p and q are computations of some monad. A monad where such programs are equal is called commutative.
\change[inline]{Find Motivation for strong monads}
\begin{definition}[Strong Monad] A monad \((T, \eta, \mu)\) on a Cartesian category \(\C \) is called strong if there exists a natural transformation \(\tau_{X,Y} : X \times TY \rightarrow T(X \times Y)\) that satisfies the following conditions:
\begin{alignat*}{2}
& T\pi_2 \circ \tau_{1,X} & & = \pi_2 \tag*{(S1)}\label{S1} \\
& \tau_{X,Y} \circ (id_X \times \eta_Y) & & = \eta_{X\times Y} \tag*{(S2)}\label{S2} \\
& \tau_{X,Y} \circ (id_X \times \mu_Y) & & = \mu_{X\times Y} \circ T\tau_{X,Y} \circ \tau_{X,TY} \tag*{(S3)}\label{S3} \\
& M \alpha_{X,Y,Z} \circ \tau_{X \times Y, Z} & & = \tau_{X, Y\times Z} \circ (id_X \times \tau_{Y, Z}) \circ \alpha_{X,Y,TZ} \tag*{(S4)}\label{S4}
\end{alignat*}
where \(\alpha_{X,Y,Z} = \langle \langle \pi_1 , \pi_1 \circ \pi_2 \rangle , \pi_2 \circ \pi_2 \rangle : X \times (Y \times Z) \rightarrow (X \times Y) \times Z\) is the associativity morphism on products.
\end{definition}
\todo[inline]{Use text => lemma style}
As with monads we can now consider the category of strong monads:
\begin{definition}[The Category of Strong Monads]\label{def:strongmonads}
Let \(\C \) be a category. A morphism between two strong monads \((S : \C \rightarrow \C, \eta^S, \mu^S, \tau^S)\) and \((T : \C \rightarrow \C, \eta^T, \mu^T, \tau^T)\) is a morphism between monads as in \autoref{def:monads} that additionally satisfies:
% https://q.uiver.app/#q=WzAsNCxbMCwwLCJYIFxcdGltZXMgU1kiXSxbMCwyLCJTKFggXFx0aW1lcyBZKSJdLFsyLDIsIlQoWCBcXHRpbWVzIFkpIl0sWzIsMCwiWCBcXHRpbWVzIFRZIl0sWzAsMSwiXFx0YXVeUyJdLFsxLDIsIlxcYWxwaGEiXSxbMCwzLCJpZCBcXHRpbWVzIFxcYWxwaGEiXSxbMywyLCJcXHRhdV5UIiwyXV0=
\[
\begin{tikzcd}[ampersand replacement=\&]
{X \times SY} \&\& {X \times TY} \\
\\
{S(X \times Y)} \&\& {T(X \times Y)}
\arrow["{\tau^S}", from=1-1, to=3-1]
\arrow["\alpha", from=3-1, to=3-3]
\arrow["{id \times \alpha}", from=1-1, to=1-3]
\arrow["{\tau^T}"', from=1-3, to=3-3]
\end{tikzcd}
\]
This yields the category \(\strongmonads{\C}\) of strong monads over \(\C \).
\end{definition}
Now we can express the above condition:
\begin{definition}[Commutative Monad]
A strong monad \(\mathbf{T}\) is called commutative if the (right) strength \(\tau \) commutes with the induced left strength
\[\sigma_{X,Y} = Tswap \circ \tau_{Y,X} \circ swap : TX \times Y \rightarrow T(X \times Y)\]
@ -479,20 +487,20 @@ Now we can express the above condition:
\end{definition}
\section{Free Objects}
Free objects are constructions capturing the essence of structures in a minimal way, we will rely
on free structures in \autoref{chp:iteration} to define a monad in a general setting. We recall the definition
Free objects, roughly speaking, are constructions for instantiating structure declarations in a minimal way.
We will rely on free structures in \autoref{chp:iteration} to define a monad in a general setting. We recall the definition
to establish some notation and then describe how to obtain a monad via existence of free objects.
\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 for any \(Y \in \obj{\C}\) and \(f : X \rightarrow UY\) there exists a unique morphism \(\free{f} : UFX \rightarrow UY\) satisfying:
% https://q.uiver.app/#q=WzAsMyxbMCwwLCJYIl0sWzEsMCwiVVkiXSxbMCwxLCJVRlgiXSxbMCwxLCJmIl0sWzAsMiwiXFxldGEiLDJdLFsyLDEsIlxcZnJlZXtmfSIsMix7InN0eWxlIjp7ImJvZHkiOnsibmFtZSI6ImRhc2hlZCJ9fX1dXQ==
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 Y\) satisfying:
% https://q.uiver.app/#q=WzAsMyxbMCwwLCJYIl0sWzEsMCwiVVkiXSxbMCwxLCJVRlgiXSxbMCwxLCJmIl0sWzAsMiwiXFxldGEiLDJdLFsyLDEsIlVcXGZyZWV7Zn0iLDIseyJzdHlsZSI6eyJib2R5Ijp7Im5hbWUiOiJkYXNoZWQifX19XV0=
\[
\begin{tikzcd}[ampersand replacement=\&]
X \& UY \\
UFX
\arrow["f", from=1-1, to=1-2]
\arrow["\eta"', from=1-1, to=2-1]
\arrow["{\free{f}}"', dashed, from=2-1, to=1-2]
\arrow["{U\free{f}}"', dashed, from=2-1, to=1-2]
\end{tikzcd}
\]
\end{definition}

6
thesis/src/02_agda-categories.tex
View file

@ -86,14 +86,14 @@ Let us now consider how to implement category theory in Agda. The usual textbook
Here \textit{collection} refers to something that behaves set-like, which is not a set and is needed to prevent size issues (there is no set of all sets, otherwise we would obtain Russel's paradox, but there is a collection of all sets), it is not immediately clear how to translate this to type theory.
Furthermore, 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. In type theory we need to be more thorough as there is no global notion of equality, eligible for all purposes, e.g.\ the standard notion of propositional equality has issues when dealing with functions in that it requires extra axioms like functional extensionality.
The definition of category that we will work with can be seen in listing~\ref{lst:category} (unnecessary information has been stripped).
The definition of category that we will work with can be seen in \autoref{lst:category} (unnecessary information has been stripped).
The key differences to the definition above are firstly that instead of talking about collections, Agda's infinite \Verb{Set} hierarchy is utilized to prevent size issues.
The notion of category is thus parametrized by 3 universe levels, one for objects, one for morphisms and one for equalities.
The consequence is that the category does not contain a type of all morphisms, instead it contains a type of morphisms for any pair of objects.
Furthermore, the types of morphisms are equipped with an equivalence relation \Verb{_≈_}, making them setoids.
This addresses the aforementioned issue of how to implement equality between morphisms: the notion of equality is just added to the definition of a category. This kind of category is also called a \textit{setoid-enriched category}.
This addresses the aforementioned issue of how to implement equality between morphisms: the notion of equality is just added to the definition of a category. This version of the notion of category is also called a \textit{setoid-enriched category}.
Because of using a custom equality relation, proofs like \Verb{∘-resp-≈} are needed throughout the library to make sure that operations on morphisms respect the equivalence relation.
Lastly, the authors also include symmetric proofs like \Verb{sym-assoc} to definitions, in this case to guarantee that the opposite category of the opposite category is equal to the original category, and a similar reason for requiring \Verb{identity²}, we won't address the need for these proofs and just accept the requirement as given for the rest of the thesis.
Lastly, the designers of agda-categories also include symmetric proofs like \Verb{sym-assoc} to definitions, in this case to guarantee that the opposite category of the opposite category is equal to the original category, and a similar reason for requiring \Verb{identity²}, we won't address the need for these proofs and just accept the requirement as given for the rest of the thesis.
\begin{listing}[H]
\begin{minted}{agda}

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

@ -7,11 +7,11 @@ For this thesis we will restrict ourselves to monads for modeling partiality, th
We will now look at how to express the following non-controversial properties of a minimal partiality monad categorically:
\begin{itemize}
\begin{enumerate}
\item Irrelevance of execution order
\item Partiality of programs
\item No other effect besides some form of non-termination
\end{itemize}
\end{enumerate}
The first property of course holds for any commutative monad, the other two are more interesting.
@ -87,13 +87,13 @@ To make the equational lifting property more comprehensible we can alternatively
\end{minted}
\end{multicols}
That is, if some computation \(p : TX\) terminates with the result \(x : X\), then \(p = return\;x\) must hold. This of course implies that running \(p\) multiple times yields the same result as running \(p\) once.
That is, if some computation \(p : TX\) terminates with the result \(x : X\), then \(p = return\;x\) must hold afterwards. This of course implies that running \(p\) multiple times yields the same result as running \(p\) once.
\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 monads that are commonly used to model partiality.
Definition~\ref{def:eqlm} combines all three properties stated at the beginning of the section, 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 canonical example of an equational lifting monad:
@ -151,19 +151,11 @@ The endofunctor \(MX = X + 1\) extends to a monad by taking \(\eta_X = i_1 : X \
In the setting of classical mathematics this monad is therefore sufficient for modeling partiality, but in general it will not be useful for modeling non-termination as a side effect, since one would need to know beforehand whether a program terminates or not. For the purpose of modeling 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:
This datatype is usually defined by the two coinductive constructors \(now : X \rightarrow D\;X\) and \(later : D\;X \rightarrow D\;X\), where \(now\) is for lifting a value inside a computation and \(later\) intuitively delays a computation by one time unit. See \autoref{chp:setoids} or~\cite{delay}, for a type theoretical study of this monad.
Categorically we obtain the delay monad by the final F-coalgebras \(DX = \nu A. X + A\), which we assume to exist. In this section we will show that these final F-coalgebras indeed yield a monad that is strong and commutative.
\todo[inline]{Explain convention of double lines vs single lines ==> remove double lines here!!}
\[\mprset{fraction={===}}
\inferrule {x : X} {now\; x : DX}\qquad
\inferrule {c : DX} {later\; c : DX}\]
Categorically we obtain this monad by the final coalgebras \(DX = \nu A. X + A\), which we assume to exist. In this section we will show that \(\mathbf{D}\) is a strong and commutative monad.
Since \(DX\) is defined as a final coalgebra, we can define morphisms via corecursion and prove theorems by coinduction. By Lambek's lemma the coalgebra structure \(out : DX \rightarrow X + DX\) is an isomorphism, whose inverse can be decomposed into the two constructors mentioned before: \(out^{-1} = [ now , later ] : X + DX \rightarrow DX\).
Since \(DX\) is defined as a final coalgebra, we can define morphisms via corecursion and prove theorems by coinduction. By \autoref{lem:lambek} the coalgebra structure \(out : DX \rightarrow X + DX\) is an isomorphism, whose inverse can be decomposed into the two constructors mentioned before: \(out^{-1} = [ now , later ] : X + DX \rightarrow DX\).
\begin{lemma}~\label{lem:delay}
The following conditions hold:
@ -580,7 +572,10 @@ Let us record some facts that we will use to prove commutativity of \(\mathbf{D}
\end{alignat*}
\end{proof}
\improvement[inline]{Elaborate more?}
We have now seen that \(\mathbf{D}\) is strong and commutative, however it is not an equational lifting monad, since besides modeling non-termination, the delay monad also counts the execution time of a computation. This is a result of the too intensional notion of equality that this monad comes with.
We have now seen that \(\mathbf{D}\) is strong and commutative, however it is not an equational lifting monad, since besides modeling non-termination, the delay monad also counts the execution time of a computation.
This is a result of the too intensional notion of equality that this monad comes with.
In \autoref{chp:setoids} we will see a way to remedy this: taking the quotient of the delay monad where execution time is ignored. This will then yield an equational lifting monad on the category of setoids. However, in a general setting it is generally believed to be impossible to define a monad structure on this quotient. Chapman et al.\ have identified the axiom of countable choice (which crucially holds in the category of setoids) as a sufficient requirement for defining a monad structure on the quotient of \(\mathbf{D}\).
In \autoref{chp:setoids} we will see a way to remedy this: taking the quotient of the delay monad where execution time is ignored.
This will then yield an equational lifting monad on the category of setoids.
However, in a general setting it is generally believed to be impossible to define a monad structure on this quotient.
Chapman et al.\ have identified the axiom of countable choice (which crucially holds in the category of setoids) as a sufficient requirement for defining a monad structure on the quotient of \(\mathbf{D}\).

101
thesis/src/04_iteration.tex
View file

@ -2,41 +2,60 @@
In this chapter we will draw on the inherent connection between partiality and iteration to establish a partiality monad in a general setting without axioms by utilizing previous research on iteration theories.
\section{Elgot Algebras}
\improvement{Add some text}
Recall the following notion from~\cite{elgotalgebras}, previously called \emph{complete Elgot algebra}.
\begin{definition}[Guarded Elgot Algebra]
\todo[inline]{Definition guarded Elgot algebra}
\end{definition}
\begin{definition}[Elgot Algebra]
A (unguarded) Elgot Algebra~\cite{uniformelgot} consists of:
\ Given a functor \(H : \C \rightarrow \C\), a \emph{(H-)guarded Elgot algebra} consists of: % chktex 36
\begin{itemize}
\item An object A
\item for every \(f : X \rightarrow A + X\) the iteration \(f^\sharp : X \rightarrow A\), satisfying:
\item An object \(A : \obj{\C}\),
\item a H-algebra structure \(a : H\;A \rightarrow A\),
\item and for every \(f : X \rightarrow A + HX\) an \emph{iteration} \(f^\sharp : X \rightarrow A\), satisfying the following axioms:
\begin{itemize}
\item \customlabel{law:fixpoint}{\textbf{Fixpoint}}: \(f^\sharp = [ id , f ^\sharp ] \circ f\)
\\ for \(f : X \rightarrow A + X\)
\item \customlabel{law:uniformity}{\textbf{Uniformity}}: \((id + h) \circ f = g \circ h \Rightarrow f ^\sharp = g^\sharp \circ h\)
\\ for \(f : X \rightarrow A + X,\; g : Y \rightarrow A + Y,\; h : X \rightarrow Y\)
\item \customlabel{law:folding}{\textbf{Folding}}: \({((f^\sharp + id) \circ h)}^\sharp = {[ (id + i_1) \circ f , i_2 \circ h ]}^\sharp \)
\\ for \(f : X \rightarrow A + X,\; h : Y \rightarrow X + Y\)
\item \customlabel{law:guardedfixpoint}{\textbf{Fixpoint}}: \(f^\sharp = [ id , a \circ H(f^\sharp) ] \circ f\)
\\ for any \(f : X \rightarrow A + HX\),
\item \customlabel{law:guardeduniformity}{\textbf{Uniformity}}: \((id + Hh) \circ f = g \circ h\) implies \(f^\sharp = g^\sharp \circ h\)
\\ for any \(f : X \rightarrow A + HX, g : Y \rightarrow A + HY, h : X \rightarrow Y\),
\item \customlabel{law:guardedcompositionality}{\textbf{Compositionality}}: \({((f^\sharp + id) \circ h)}^\sharp = {([ (id + Hi_1) \circ f , i_2 \circ Hi_2 ] \circ [ i_1 , h ])}^\sharp \circ i_2\)
\\ for any \(f : X \rightarrow A + HX, h : Y \rightarrow X + HY\).
\end{itemize}
\end{itemize}
\end{definition}
Consider an Elgot algebra over the identity functor \(Id : \C \rightarrow \C\) together with the trivial Id-algebra structure \(id : A \rightarrow A\). Morphisms of the form \(f : X \rightarrow A + X\) can then be viewed as modelling one iteration of a loop, where \(X \in \obj{\C}\) is the state space and \(A \in \obj{\C}\) the object of values. Intuitively, in such a setting the iteration operator \({(-)}^\sharp\) runs such a morphism in a loop until it terminates (or diverges), thus assigning it a solution. This is what the \ref{law:guardedfixpoint} axiom guarantees. On the other hand the \ref{law:uniformity} axiom states how to handle loop invariants and finally, the \ref{law:guardedcompositionality} axiom is the most sophisticated one, stating that compatible iterations can be combined into a single iteration with a merged state space. % chktex 2
The previous intuition gives rise to the following simpler definition that has been introduced in~\cite{uniformelgot}.
\begin{definition}[Elgot Algebra]
A \emph{(unguarded) Elgot Algebra}~\cite{uniformelgot} consists of:
\begin{itemize}
\item An object \(A : \obj{\C}\),
\item and for every \(f : X \rightarrow A + X\) an \emph{iteration} \(f^\sharp : X \rightarrow A\), satisfying the following axioms:
\begin{itemize}
\item \customlabel{law:fixpoint}{\textbf{Fixpoint}}: \(f^\sharp = [ id , f ^\sharp ] \circ f\)
\\ for any \(f : X \rightarrow A + X\),
\item \customlabel{law:uniformity}{\textbf{Uniformity}}: \((id + h) \circ f = g \circ h\) implies \(f ^\sharp = g^\sharp \circ h\)
\\ for any \(f : X \rightarrow A + X,\; g : Y \rightarrow A + Y,\; h : X \rightarrow Y\),
\item \customlabel{law:folding}{\textbf{Folding}}: \({((f^\sharp + id) \circ h)}^\sharp = {[ (id + i_1) \circ f , i_2 \circ h ]}^\sharp \)
\\ for any \(f : X \rightarrow A + X,\; h : Y \rightarrow X + Y\).
\end{itemize}
\end{itemize}
\end{definition}
In this setting the simpler \ref{law:folding} axiom replaces the sophisticated \ref{law:guardedcompositionality} axiom. % chktex 2
Indeed, for \(Id\)-guarded Elgot algebras with a trivial algebra structure, the \ref{law:folding} and \ref{law:guardedcompositionality} axioms are equivalent, which is illustrated by the following Lemma. % chktex 2
\begin{lemma}
Every Elgot algebra \((A , {(-)}^\sharp)\) satisfies the following additional laws
Every Elgot algebra \((A , {(-)}^\sharp)\) satisfies the following additional axioms
\begin{itemize}
\item \customlabel{law:compositionality}{\textbf{Compositionality}}: \({((f^\sharp + id) \circ h)}^\sharp = {([ (id + i_1) \circ f , i_2 \circ i_2 ] \circ [ i_1 , h ])}^\sharp \circ i_2\)
\\ for \(f : X \rightarrow A + X, h : Y \rightarrow X + Y\)
\\ for any \(f : X \rightarrow A + X, h : Y \rightarrow X + Y\),
\item \customlabel{law:stutter}{\textbf{Stutter}}: \({(([ h , h ] + id) \circ f)}^\sharp = {(i_1 \circ h , [ h + i_1 , i_2 \circ i_2 ] )}^\sharp \circ inr\)
\\ for \(f : X \rightarrow (Y + Y) + X, h : Y \rightarrow A\)
\\ for any \(f : X \rightarrow (Y + Y) + X, h : Y \rightarrow A\),
\item \customlabel{law:diamond}{\textbf{Diamond}}: \({((id + \Delta) \circ f)}^\sharp = {([ i_1 , ((id + \Delta) \circ f)^\sharp + id] \circ f)}^\sharp \)
\\ for \(f : X \rightarrow A + (X + X)\)
\\ for any \(f : X \rightarrow A + (X + X)\).
\end{itemize}
\end{lemma}
\begin{proof}\;\\
\begin{proof} The proofs of the axioms build upon each other, we prove them one by one.
\begin{itemize}
\item \ref{law:compositionality}: First, note that \ref{law:folding} can equivalently be reformulated as % chktex 2
\begin{equation*}
@ -136,9 +155,9 @@ In this chapter we will draw on the inherent connection between partiality and i
\end{itemize}
\end{proof}
\todo[inline]{Mention here that previous lemma implies that unguarded Elgot are id guarded Elgot and diamond gives alternate way of classifying Elgot algebras citing Sergey}
Note that in~\cite{uniformelgot} it has been shown that the \ref{law:diamond} axiom implies \ref{law:compositionality}, yielding another definition of Elgot algebras only requiring the \ref{law:fixpoint}, \ref{law:uniformity} and \ref{law:diamond} axioms. % chktex 2
Morphisms between Elgot algebras that are coherent with respect to the iteration operator are of special interest to us, the following definition classifies them.
Let us now consider morphisms that are coherent with respect to the iteration operator. A special case being morphisms between Elgot algebras.
\begin{definition}[Iteration Preserving Morphisms]
Let \((A, {(-)}^{\sharp_a}), (B, {(-)}^{\sharp_b})\) be two Elgot algebras.
@ -334,29 +353,49 @@ Products and exponentials of Elgot algebras can be formed in a canonical way.
\end{itemize}
\end{proof}
\section{Pre-Elgot Monads}
\section{The Initial (Strong) Pre-Elgot Monad}
In this section we will study the monad that arises from existence of all free Elgot algebras. We will show that this is an equational lifting monad and also the initial strong pre-Elgot monad.
\improvement{Add some text, explain Elgot monads and while loops}
Let us first recall the following notion that was introduced in~\cite{elgotmonad} and reformulated in~\cite{uniformelgot}.
\begin{definition}[Elgot Monad]
An Elgot monad consists of
\begin{itemize}
\item A monad \(\mathbf{T}\),
\item for every \(f : X \rightarrow T(Y + X)\) an iteration \(f^\dag : X \rightarrow TY \) satisfying:
\begin{itemize}
\item \textbf{Fixpoint}: \(f^\dag = {[ \eta , f^\dag ]}^* \circ f \)
\\ for any \(f : X \rightarrow T(Y + X)\),
\item \textbf{Uniformity}: \(f \circ h = T(id + h)\) implies \(f^\dag \circ g = g^\dag\)
\\ for any \(f : X \rightarrow T(Y + X), g : Z \rightarrow T(Y + Z), h : Z \rightarrow X\),
\item \textbf{Naturality}: \(g^* \circ f^\dag = {({[(Ti_1 \circ g , \eta \circ i_2 ]}^* \circ f)}^\dag\)
\\ for any \(f : X \rightarrow T(Y + X), g : Y \rightarrow TZ\),
\item \textbf{Codiagonal}: \({f^\dag}^\dag = {(T[id , i_2] \circ f)}^\dag\)
\\ for any \(f : X \rightarrow T((Y + X) + X)\).
\end{itemize}
\end{itemize}
If the monad \(\mathbf{T}\) is strong with strength \(\tau\) and \(\tau \circ (id \times f^\dag) = {(Tdstl \circ \tau \circ (id \times f)}^\dag\) for any \(f : X \rightarrow T(Y+X)\), then \(\mathbf{T}\) is a strong Elgot monad.
\end{definition}
\begin{definition}[(Strong) Pre-Elgot Monad]
We regard Elgot monads as minimal semantic structures for interpreting side-effecting while loops, as has been argued in~\cite{goncharov2018unguarded, goncharov2017unifying}.
The following notion has been introduced in~\cite{uniformelgot} as a weaker approximation of the notion of Elgot monad, using less sophisticated axioms.
\begin{definition}[Pre-Elgot Monad]
A monad \(\mathbf{T}\) is called pre-Elgot if every \(TX\) extends to an Elgot algebra such that for every \(f : X \rightarrow TY\) the Kleisli lifting \(f^* : TX \rightarrow TY\) is iteration preserving.
If \(\mathbf{T}\) is additionally strong and the strength \(\tau \) is right iteration preserving we call it strong pre-Elgot.
\end{definition}
(Strong) pre-Elgot monads form a subcategory of \(\monads{\C}\) where objects are (strong) pre-Elgot monads and morphisms between pre-Elgot monads are natural transformations \(\alpha \) as in \autoref{def:monads} such that additionally each \(\alpha_X\) is iteration preserving. Similarly, morphisms between strong pre-Elgot monads are natural transformations \(\alpha \) as in \autoref{def:strongmonads} such that each \(\alpha_X\) is iteration preserving. We call these categories \(\preelgot{\C}\) and \(\strongpreelgot{\C}\) respectively.
(Strong) pre-Elgot monads form a subcategory of \(\monads{\C}\) where objects are (strong) pre-Elgot monads and morphisms between pre-Elgot monads are natural transformations \(\alpha \) as in \autoref{def:monadmorphism} such that additionally each \(\alpha_X\) is iteration preserving. Similarly, morphisms between strong pre-Elgot monads are natural transformations \(\alpha \) as in \autoref{def:strongmonadmorphism} such that each \(\alpha_X\) is iteration preserving. We call these categories \(\preelgot{\C}\) and \(\strongpreelgot{\C}\) respectively.
\begin{lemma}
\(\preelgot{\C}\) and \(\strongpreelgot{\C}\) are categories.
\end{lemma}
\begin{proof}
Using \autoref{def:monads} and \autoref{def:strongmonads} it suffices to show that the components of the identity natural transformation are iteration preserving and that the composition of two pre-Elgot monad morphisms is iteration preserving component wise. This has already been shown in \autoref{lem:elgotalgscat}.
Since \(\preelgot{\C}\) and \(\strongpreelgot{\C}\) are subcategories of the previously defined categories \(\monads{\C}\) and \(\strongmonads{\C}\) respectively, it suffices to show that the components of the identity natural transformation are iteration preserving and that the component wise composition of two pre-Elgot monad morphisms is iteration preserving. This has already been shown in \autoref{lem:elgotalgscat}.
\end{proof}
\todo[inline]{Initial pre-Elgot bridges gap to Elgot monads under countable choice\ldots}
\section{The Initial Strong Pre-Elgot Monad}
In this section we will study the monad that arises from existence of all free Elgot algebras. We will show that this is an equational lifting monad and also the initial strong pre-Elgot monad.
Assuming a form of the axiom of countable choice it has been proven in~\cite{uniformelgot} that the initial pre-Elgot monad and the initial Elgot monad coincide, thus closing the expressivity gap in such a setting.
However, it is believed to be impossible to close this gap in a general setting.
\begin{proposition}
Existence of all free Elgot algebras yields a monad that we call \(\mathbf{K}\).

5
thesis/src/05_setoids.tex
View file

@ -107,11 +107,6 @@ Setoids together with setoid functions form a category that we will call \(\seto
\end{proof}
\section{Quotienting the Delay Monad}
% TODO merge this into introduction
% Chapman et al. have already proven that quotienting the delay datatype by weak bisimilarity using the quotients-as-setoids approach yields a monad~\cite{quotienting}, we will build upon their results and show that this quotient is indeed an instance of our monad \(\mathbf{K}\).
% Historically proof assistants like Agda and Coq have been offering multiple ways of defining coinductive types, nowadays the manuals of both Agda and Coq advise users to use coinductive records instead of defining coinductive types by constructors, we will heed this advice.
% Since the delay monad is usually defined by the constructors \(now\) and \(later\)
In this section we will introduce data types only using inference rules. For that we adopt the convention that coinductive types are introduced by doubled lines while inductive types are introduced with a single line.
Now, recall from previous chapters that Capretta's delay monad~\cite{delay} is a coinductive type defined by the two constructors: