change file names to final chapter order, work on introduction.

thesis/agda/Coind.agda

@@ -1,4 +1,8 @@
 {-# OPTIONS --guardedness #-}
+
+-- Agda code that is included in the thesis.
+-- just for making sure that everything used in the thesis actually compiles ;)
+
 open import Agda.Builtin.Equality
 module Coind where
 module Streams where

thesis/agda/Setoids.agda

@@ -1,3 +1,6 @@
+-- Agda code that is included in the thesis.
+-- just for making sure that everything used in the thesis actually compiles ;)
+
 module Setoids where
   open import Level
 

thesis/main.tex

@@ -205,13 +205,7 @@
 % \chapter*{Licensing}
 % \doclicenseThis{}
 
-\chapter*{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.
-
+\include{src/00_abstract}
 
 \tableofcontents
 
@@ -233,13 +227,13 @@ Since fixing this seems to be impossible without additional axioms, we will look
 
 \ifdraft{\linenumbers}
 
-\include{src/00_introduction}
-\include{src/01_preliminaries}
-\include{src/02_agda-categories}
-\include{src/03_partiality-monads}
-\include{src/04_iteration}
-\include{src/05_setoids}
-\include{src/10_conclusion}
+\include{src/01_introduction}
+\include{src/02_preliminaries}
+\include{src/03_agda-categories}
+\include{src/04_partiality-monads}
+\include{src/05_iteration}
+\include{src/06_setoids}
+\include{src/07_conclusion}
 
 \todo[inline]{Add fullstop behind every proof}
 

thesis/src/00_abstract.tex

@@ -0,0 +1,10 @@
+\chapter*{Abstract}
+Moggi famously showed how to use category theory (specifically monads) to model the semantics of effectful computations.
+
+In this thesis we will 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 examine a novel approach of 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.
+
+Finally, we will show that in the category of setoids this partiality monad instantiates to a quotient of the delay monad, yielding a concrete description of the partiality monad in this category.

thesis/src/00_introduction.tex

@@ -1,5 +0,0 @@
-\chapter{Introduction}
-
-\section{Motivation}
-\info[inline]{Use introductory example from talk}
-\todo[inline]{Give overview of thesis}

thesis/src/01_introduction.tex

@@ -0,0 +1,38 @@
+\chapter{Introduction}
+
+Haskell is considered a purely functional programming language, though the notion of purity used is an informal one, not to be confused with the standard notion of pure function, i.e.\ a function that does not have any side effects.
+For there are indeed Haskell functions that have side effects, consider the following function for retrieving the head of a list:
+
+\begin{minted}{haskell}
+head :: [a] -> a
+head (x:xs) = x 
+\end{minted}
+
+Indeed, this function is partial, since for empty lists it will cause an exception to be thrown by the Haskell compiler and thus Haskell does at least offer exceptions as a side effect.
+Furthermore, consider the following standard list reversal function
+
+\begin{minted}{haskell}
+reverse :: [a] -> [a]
+reverse l = revAcc l []
+  where
+    revAcc []     a = a
+    revAcc (x:xs) a = revAcc xs (x:a)
+\end{minted}
+and regard the following infinite list
+\begin{minted}{haskell}
+ones :: [Int]
+ones = 1 : ones
+\end{minted}
+
+Now, notice that the call \texttt{reverse ones} will never terminate, thus Haskell does also offer non-termination as a side effect.
+
+Combining these observations we can draw the conclusion that in order to interpret the Haskell programming language, we will need a way to model general partiality as a side effect.
+Moggi has introduced a method for interpreting programming languages by means of category theory.
+Notably, one needs a monad that is suitable for modelling the desired effects.
+We will thus consider monads that are suitable for modelling partiality and the properties that they should have in \autoref{chp:partiality}.
+Capretta's delay monad is one such monad that is useful for modelling partiality in type theory.
+In a more general setting the delay monad however turns out to be not suitable, thus we will introduce a novel partiality monad that is defined using minimal assumptions in \autoref{chp:iteration}.
+Lastly, in \autoref{chp:setoids} we will give a concrete description of this very general monad in the category of setoids, where it instantiates to a specific quotient of the delay monad.
+
+\todo[inline]{Text needs a lot of work\ldots}
+\todo[inline]{Mention formalization and chapter.}

thesis/src/05_iteration.tex

@@ -20,7 +20,7 @@ Recall the following notion from~\cite{elgotalgebras}, previously called \emph{c
   \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
+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 modeling 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}.