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

wording and typos

Browse source
This commit is contained in:
Leon Vatthauer 2024-02-22 18:04:09 +01:00
parent 96f9bf4bb9
commit 8464a80e26
Signed by: leonv
SSH key fingerprint: SHA256:G4+ddwoZmhLPRB1agvXzZMXIzkVJ36dUYZXf5NxT+u8
7 changed files with 94 additions and 53 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -0,0 +1,49 @@
cocartesian
cartesian
iso
coproducts
Coalgebras
adjunctions
coalgebras
Adjunctions
Lambek
endofunctor
pointful
Kleisli
functoriality
formalizations
Agda
Coq
agda-categories
setoids
sym-assoc
setoid-enriched
extensionality
Setoid
Moggi
Cockett
Bucalo
equational
coinductive
corecursion
coinduction
coalgebra
Capretta
monic
monicity
intensional
Fixpoint
Elgot
exponentials
Pre-Elgot
pre-Elgot
quotiented
quotients-as-setoid
setoid
Setoids
Coproducts
iff
Quotienting
bisimilarity
corecursively
coproduct

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

@ -0,0 +1,3 @@
{"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$"}

12
thesis/src/01_preliminaries.tex
View file

@ -38,7 +38,7 @@ Categories with finite products (i.e. binary products and a terminal object) are
\begin{definition}[Distributive Category]
\label{def:distributive}
A cartesian and cocartesian category $\C$ is called distributive if the canonical (left) distributivity morphism 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}
{X \times Y + X \times Z} &&& {X \times (Y + Z)}
@ -114,10 +114,10 @@ The internal logic of cartesian closed categories is the simply typed $\lambda$-
\section{Coalgebras}
\todo[inline]{Maybe introduce (co-)induction here via (co-)algebras}
\todo[inline]{introduce (terminal) coalgebras, proof lambeks lemma}
\todo[inline]{Introduce (terminal) coalgebras, proof Lambek's lemma}
\section{Adjunctions and Free Objects}
\todo[inline]{introduce adjunctions}
\todo[inline]{Introduce adjunctions}
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:
@ -227,14 +227,14 @@ 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.
''$\Rightarrow$'':
\change[inline]{Change quotation marks}
'' $\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$.

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

@ -1,6 +1,6 @@
\chapter{Category Theory in Agda}
There are many formalizations of category theory in proof assistants like Coq or Agda. The benefits of such a formalization are clear: having a usable formalization allows one to reason about categorical notions in a typechecked environment that makes errors less likely.
There are many formalizations of category theory in proof assistants like Coq or Agda. The benefits of such a formalization are clear: having a usable formalization allows one to reason about categorical notions in a type checked environment that makes errors less likely.
Ideally such a development will bring researchers together and enable them to work in a unified setting that enables efficient communication of ideas and concepts.
In this thesis we will work with the dependently typed programming language Agda~\cite{agda} and the agda-categories~\cite{agda-categories} library that serves as an extensive foundation of categorical definitions.
This chapter shall serve as a quick introduction to the library and the formalization of this thesis.
@ -15,17 +15,17 @@ A category consists of
\item For every two morphisms $f : X \rightarrow Y, g : Y \rightarrow Z$ another morphism $g \circ f : X \rightarrow Z$ called the composition
\item For every object $X$ a morphism $id_X : X \rightarrow X$ called the identity
\end{itemize}
where the composition is associative and the identity morphisms are identities with respect to the composition.
where the composition is associative, and the identity morphisms are identities with respect to the composition.
\end{definition}
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.
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 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.
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}.
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.
@ -62,8 +62,8 @@ From this it should be clear how other basic notions like functors or natural tr
\section{The formalization}
\improvement{explain more}
\improvement{Explain more}
The agda formalization of this thesis is structured similar to the agda-categories library, e.g. key concepts like monads and categories correspond to separate top-level folders, which contain the core definitions as well as folders for sub-concepts and their properties, and possibly folders 'Instances' for specific instances, and 'Construction' for blueprints for constructing this concept (e.g. the Kleisli category of a monad would be in 'Category.Construction.Kleisli'.
The Agda formalization of this thesis is structured similar to the agda-categories library, e.g. key concepts like monads and categories correspond to separate top-level folders, which contain the core definitions as well as folders for sub-concepts and their properties, and possibly folders 'Instances' for specific instances, and 'Construction' for blueprints for constructing this concept (e.g. the Kleisli category of a monad would be in 'Category.Construction.Kleisli').
The source code of the formalization can be found \href{https://git8.cs.fau.de/theses/bsc-leon-vatthauer}{here} (internal) or as clickable HTML \href{https://wwwcip.cs.fau.de/~hy84coky/bsc-thesis/}{here} (public).

23
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 effectul programming language in a category. For this one needs a (strong) monad $T$ capturing the desired effects, then we can take the elements of $TA$ as denotations for programs of type $A$. The kleisli category of $T$ can be viewed as the category of programs, which gives us a way of composing programs (Kleisli composition).
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.
@ -31,7 +31,7 @@ To ensure that programs are partial, we recall the following notion by Cockett a
\end{definition}
\todo[inline]{be more precise}
Intuitively $\tdom f$ captures the domain of definedness of $f$.
Intuitively $\tdom f$ captures the domain of definiteness of $f$.
\begin{definition}[Restriction Category]
Every category has a trivial restriction structure by taking $dom (f : X \rightarrow Y) = id_X$.
@ -162,7 +162,7 @@ Since $DX$ is defined as a final coalgebra, we can define morphisms via corecurs
We will make use of the fact that every $DX$ is a final coalgebra:
\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:
\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}
% https://q.uiver.app/#q=WzAsNSxbMCwxLCJEWCArIERZIl0sWzcsMSwiWSArIChEWCArIERZKSJdLFswLDAsIkRYIl0sWzAsMiwiRFkiXSxbNywyLCJZICsgRFkiXSxbMCwxLCJbIFsgWyBpXzEgLCBpXzIgXFxjaXJjIGlfMiBdIFxcY2lyYyAob3V0IFxcY2lyYyBmKSAsIGlfMiBcXGNpcmMgaV8xIF0gXFxjaXJjIG91dCAsIChpZCArIGlfMikgXFxjaXJjIG91dCBdIl0sWzIsMCwiaV8xIl0sWzAsMywiISIsMCx7InN0eWxlIjp7ImJvZHkiOnsibmFtZSI6ImRhc2hlZCJ9fX1dLFszLDQsIm91dCJdLFsxLDQsImlkICsgISIsMCx7InN0eWxlIjp7ImJvZHkiOnsibmFtZSI6ImRhc2hlZCJ9fX1dXQ==
@ -186,7 +186,7 @@ Since $DX$ is defined as a final coalgebra, we can define morphisms via corecurs
\end{proof}
\begin{theorem}
$\mathbf{D} = (D, now, (-)^*)$ is a kleisli triple.
$\mathbf{D} = (D, now, (-)^*)$ is a Kleisli triple.
\end{theorem}
\begin{proof}
We will now use the properties proven in Corollary~\ref{col:delay} to prove the Kleisli triple laws:
@ -245,7 +245,7 @@ Since $(DX, out)$ is a final coalgebra we get the following proof principle:
\end{tikzcd}\]
Next we check the strength laws:
\begin{itemize}
\item[\ref{S1}] To show that $(now \circ \pi_2)^* \circ \tau = \pi_2$ we take the following coalgebra:
\item[\ref{S1}] To show that $(now \circ \pi_2)^* \circ \tau = \pi_2$ we do coinduction using the following coalgebra:
% https://q.uiver.app/#q=WzAsNixbMCwwLCIxIFxcdGltZXMgRFgiXSxbMCwxLCJEWCJdLFszLDAsIlggKyAxIFxcdGltZXMgRFgiXSxbMywxLCJYICsgRFgiXSxbMSwwLCIxIFxcdGltZXMgWCArIERYIl0sWzIsMCwiMSBcXHRpbWVzIFggKyAxIFxcdGltZXMgRFgiXSxbMSwzLCJvdXQiXSxbMCwxLCIhIiwwLHsic3R5bGUiOnsiYm9keSI6eyJuYW1lIjoiZGFzaGVkIn19fV0sWzIsMywiaWQgKyAhIl0sWzAsNCwiaWQgXFx0aW1lcyBvdXQiXSxbNCw1LCJkc3RsIl0sWzUsMiwiXFxwaV8yICsgaWQiXV0=
\[\begin{tikzcd}
{1 \times DX} & {1 \times X + DX} & {1 \times X + 1 \times DX} & {X + 1 \times DX} \\
@ -283,7 +283,7 @@ Since $(DX, out)$ is a final coalgebra we get the following proof principle:
\arrow["{id + \;!}"', from=2-3, to=3-3]
\arrow["{[ (id + (id \times now)) \circ dstl \circ (id \times out) , i_2 ]}"', from=1-3, to=2-3]
\end{tikzcd}\]
\item[\ref{S4}] To show that $D\alpha \circ \tau = \tau \circ (id \times \tau) \circ \alpha$ we take the following coalgebra:
\item[\ref{S4}] To show $D\alpha \circ \tau = \tau \circ (id \times \tau) \circ \alpha$ by coinduction we take the coalgebra:
% https://q.uiver.app/#q=WzAsNixbMCwwLCIoWCBcXHRpbWVzIFkpIFxcdGltZXMgRFoiXSxbMCwyLCJEKFggXFx0aW1lcyBZIFxcdGltZXMgWikiXSxbMiwyLCJYIFxcdGltZXMgWSBcXHRpbWVzIFogKyBEKFggXFx0aW1lcyBZIFxcdGltZXMgWikiXSxbMiwxLCJYIFxcdGltZXMgWSAgXFx0aW1lcyBaICsgKFggXFx0aW1lcyBZKSBcXHRpbWVzIERaIl0sWzEsMCwiKFggXFx0aW1lcyBZKSBcXHRpbWVzIChaKyBEWikiXSxbMiwwLCIoWFxcdGltZXMgWSkgXFx0aW1lcyBaICsgKFggXFx0aW1lcyBZKSBcXHRpbWVzIERaIl0sWzAsMSwiISIsMCx7InN0eWxlIjp7ImJvZHkiOnsibmFtZSI6ImRhc2hlZCJ9fX1dLFsxLDIsIm91dCJdLFszLDIsImlkICtcXDshIiwyXSxbMCw0LCJpZCBcXHRpbWVzIG91dCJdLFs0LDUsImRzdGwiXSxbNSwzLCJcXGxhbmdsZSBcXHBpXzEgXFxjaXJjIFxccGlfMSAsIFxcbGFuZ2xlIFxccGlfMiBcXGNpcmMgXFxwaV8xICwgXFxwaV8yIFxccmFuZ2xlIFxccmFuZ2xlICsgaWQiLDJdXQ==
\[\begin{tikzcd}
{(X \times Y) \times DZ} & {(X \times Y) \times (Z+ DZ)} & {(X\times Y) \times Z + (X \times Y) \times DZ} \\
@ -303,7 +303,6 @@ To show that $\mathbf{D}$ is commutative we will use another proof principle pre
\begin{definition}
We call a morphism $g : X \rightarrow D (Y + X)$ \textit{guarded} if there exists an $h : X \rightarrow Y + D(Y+X)$ such that the following diagram commutes:
\todo[inline]{change name of morphism}
% https://q.uiver.app/#q=WzAsNCxbMCwwLCJYIl0sWzMsMCwiRCAoWSArWCkiXSxbMywxLCIoWSArIFgpICsgRChZICsgWCkiXSxbMCwxLCJZICsgRChZK1gpIl0sWzAsMSwiZyJdLFsxLDIsIm91dCJdLFszLDIsImlfMSArIGlkIiwyXSxbMCwzLCJoIiwyXV0=
\[\begin{tikzcd}[ampersand replacement=\&]
X \&\&\& {D (Y +X)} \\
@ -325,6 +324,7 @@ To show that $\mathbf{D}$ is commutative we will use another proof principle pre
It suffices to show $[ now , f ]^* = [ now , i ]^*$, because then follows:
\[f = [ now , f ]^* \circ g = [ now , i ]^* \circ g = i\]
We prove this by coinduction using:
\change[inline]{Change name of morphism}
% https://q.uiver.app/#q=WzAsNSxbMCwxLCJEWSJdLFszLDEsIlkgKyBEWSJdLFswLDAsIkQoWSArIFgpIl0sWzEsMCwiKFkgKyBYKSArIEQoWStYKSJdLFszLDAsIlkgKyBEKFkrWCkiXSxbMCwxLCJvdXQiXSxbMiwzLCJvdXQiXSxbMyw0LCJbIFsgaV8xICwgaCBdICwgaV8yIF0iXSxbNCwxLCJpZCArIFxcOyEiXSxbMiwwLCIhIiwwLHsic3R5bGUiOnsiYm9keSI6eyJuYW1lIjoiZGFzaGVkIn19fV1d
\[\begin{tikzcd}[ampersand replacement=\&]
{D(Y + X)} \& {(Y + X) + D(Y+X)} \&\& {Y + D(Y+X)} \\
@ -347,11 +347,12 @@ To show that $\mathbf{D}$ is commutative we will use another proof principle pre
\[g = out^{-1} \circ [ i_1 + D i_1 \circ \sigma , i_2 \circ [ D i_1 \circ \tau , later \circ now \circ i_2 ] ] \circ w\]
$g$ is trivially guarded by $[ id + D i_1 \circ \sigma , i_2 \circ [ D i_1 \circ \tau , later \circ now \circ i_2 ] ] \circ w$.
We are left to show that $\tau^* \circ \sigma$ and $\sigma^* \circ \tau$ are solutions of $g$, i.e.:
We are left to show that both $\tau^* \circ \sigma$ and $\sigma^* \circ \tau$ are solutions of $g$. Consider:
\[\tau^* \circ \sigma = out^{-1} \circ [ id + \sigma , i_2 \circ [ \tau , later \circ \tau^* \circ \sigma ] ] \circ w = [ now , \tau^* \circ \sigma]^* \circ g \]
\[\sigma^* \circ \tau = out^{-1} \circ [ id + \sigma , i_2 \circ [ \tau , later \circ \sigma^* \circ \tau ] ] \circ w = [ now , \sigma^* \circ \tau]^* \circ g \]
\change[inline]{Make this more explicit}
The first step in both equations can be proven by monicity of $out$ and then using \ref{D3} and the dual diagram for $\sigma$ which is a direct consequence of \ref{D3}:
% https://q.uiver.app/#q=WzAsNSxbMCwwLCJYIFxcdGltZXMgRFkiXSxbMCwxLCJEKFggXFx0aW1lcyBZKSJdLFs0LDAsIlggXFx0aW1lcyBZICsgWCBcXHRpbWVzIERZIl0sWzQsMSwiWCBcXHRpbWVzIFkgK0QoWCBcXHRpbWVzIFkpIl0sWzIsMCwiWCBcXHRpbWVzIChZICsgRFkpIl0sWzAsMSwiXFxoYXR7XFx0YXV9IiwwLHsic3R5bGUiOnsiYm9keSI6eyJuYW1lIjoiZGFzaGVkIn19fV0sWzEsMywib3V0Il0sWzIsMywiaWQgKyBcXGhhdHtcXHRhdX0iLDJdLFswLDQsImlkIFxcdGltZXMgb3V0Il0sWzQsMiwiZHN0bCJdXQ==
\[\begin{tikzcd}[ampersand replacement=\&]
@ -366,7 +367,7 @@ To show that $\mathbf{D}$ is commutative we will use another proof principle pre
the last step holds generally for any $f : DX \times DY \rightarrow D(X \times Y)$.
\end{proof}
\change[inline]{wording}
We have now seen that $\mathbf{D}$ is strong and commutative, ideally we would want it to be an equational lifting monad, but this is not the case since besides modelling non-termination, the delay monad also captures the execution time. This is a result of the too intensional notion of equality that this monad comes with.
\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 modelling 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 chapter~\ref{chp:setoids} we will see how to remedy this, by taking the quotient of the delay monad where execution time is ignored. This will then give us an equational lifting monad in the category of setoids, but Chapman et al.~\cite{quotienting} have found that this does not work generally without assuming some form of the axiom of countable choice (which crucially holds in the category of setoids).
In chapter~\ref{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}$.

30
thesis/src/04_iteration.tex
View file

@ -1,5 +1,6 @@
\chapter{Iteration Algebras and Monads}\label{chp:iteration}
In this chapter we will draw on the inherent connection between recursion and iteration to establish a partiality monad in a general setting without axioms that comes from previous results in the research on iteration theories.
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}
@ -64,10 +65,10 @@ We can form products and exponentials of Elgot algebras in a canonical way, for
\section{Pre-Elgot Monads}
\improvement{Add some text, explain elgot monads and while loops}
\improvement{Add some text, explain Elgot monads and while loops}
\begin{definition}[Pre-Elgot Monad]
A monad $\mathbf{T}$ is called pre-Elgot if every $TX$ extends to an Elgot algebra such that Kleisli lifting is iteration preversing, i.e.
A monad $\mathbf{T}$ is called pre-Elgot if every $TX$ extends to an Elgot algebra such that Kleisli lifting is iteration preserving, i.e.
\[h^* \circ f^\# = ((h^* + id) \circ f)^\#\qquad \text{for}\; f : Z \rightarrow TX + Z, h : X \rightarrow TY\]
\end{definition}
@ -110,6 +111,7 @@ In this section we will study the monad that arises from existence of all free E
If every $X \in \obj{\C}$ extends to a free Elgot algebra $KX$ we get a monad $\mathbf{K}$.
\end{lemma}
\begin{proof}
\todo[inline]{Proof in preliminaries}
Existence of all free objects in $\elgotalgs{\C}$ yields an adjunction between $\C$ and $\elgotalgs{\C}$ that in turn gives us a monad on $\C$.
\end{proof}
@ -164,7 +166,7 @@ Stability of $KX$ expresses that it somehow behaves like it would in a cartesian
\ref{sharpl1} and \ref{sharpl2} then follow by properties of the exponential and of distributive categories, uniqueness is more interesting:
Let $g : KY \times X \rightarrow A$ be a morphism satisfying \ref{sharpl1} and \ref{sharpl2}, we need to show that $g = eval \circ (\llbracket curry\;f \rrbracket \times id)$. We use that fact that $curry$ is an injective mapping, i.e. it suffices to show that:
\[curry\; g = \llbracket curry\;f \rrbracket = curry (eval \circ (\llbracket curry\;f \rrbracket \times id))\]
Where the second step holds for any exponential and the first step is proven by the universal property of free objects, i.e. we need to show that $curry\;g \circ \eta = curry\;f$ which follows by \ref{sharpl1} and we need to check that $curry\;g$ is left iteration preversing which follows from \ref{sharpl2}.
Where the second step holds for any exponential and the first step is proven by the universal property of free objects, i.e. we need to show that $curry\;g \circ \eta = curry\;f$ which follows by \ref{sharpl1}, and we need to check that $curry\;g$ is left iteration preserving which follows from \ref{sharpl2}.
\end{proof}
For the rest of this chapter we will assume every $KX$ to exist and be stable to show that it is an equational lifting monad and in fact the initial strong pre-Elgot monad.
@ -193,21 +195,7 @@ Of course there is also a symmetric version of this:
To check naturality and the strength laws we will use remark~\ref{rem:proofbystability} and for brevity only state the needed unifying morphism by pasting \ref{sharpl1} into the required diagram. The proofs of \ref{sharpr1} and \ref{sharpr2} can then be looked up in the formalization.
% For naturality of $\tau$, i.e. $\tau \circ (f \times Kg) = K(f \times g) \circ \tau$ for $f : A \rightarrow X, g : B \rightarrow Y$ we use:
For naturality of $\tau$ we use:
% % https://q.uiver.app/#q=WzAsMyxbMCwwLCJBIFxcdGltZXMgS0IiXSxbMiwwLCJLKFggXFx0aW1lcyBZKSJdLFswLDIsIkEgXFx0aW1lcyBCIl0sWzAsMSwiXFx0YXUgXFxjaXJjIChmIFxcdGltZXMgS2cpIiwwLHsib2Zmc2V0IjotMX1dLFswLDEsIksoZlxcdGltZXMgZykgXFxjaXJjIFxcdGF1IiwyLHsib2Zmc2V0IjoxfV0sWzIsMCwiaWQgXFx0aW1lcyBcXGV0YSIsMl0sWzIsMSwiXFxldGEgXFxjaXJjIEsoZiBcXHRpbWVzIGcpIiwyXV0=
% \[\begin{tikzcd}
% {A \times KB} && {K(X \times Y)} \\
% \\
% {A \times B}
% \arrow["{\tau \circ (f \times Kg)}", shift left, from=1-1, to=1-3]
% \arrow["{K(f\times g) \circ \tau}"', shift right, from=1-1, to=1-3]
% \arrow["{id \times \eta}"', from=3-1, to=1-1]
% \arrow["{\eta \circ K(f \times g)}"', from=3-1, to=1-3]
% \end{tikzcd}\]
% https://q.uiver.app/#q=WzAsNSxbMSwwLCJBIFxcdGltZXMgS0IiXSxbMCwzLCJBIFxcdGltZXMgQiJdLFsxLDIsIksoQSBcXHRpbWVzIEIpIl0sWzMsMiwiSyhYIFxcdGltZXMgWSkiXSxbMywwLCJYIFxcdGltZXMgS1kiXSxbMSwwLCJpZCBcXHRpbWVzIFxcZXRhIiwwLHsiY3VydmUiOi0yfV0sWzAsMiwiXFx0YXUiLDJdLFsyLDMsIksoZlxcdGltZXMgZykiLDJdLFswLDQsImYgXFx0aW1lcyBLZyJdLFs0LDMsIlxcdGF1Il0sWzEsMywiXFxldGEgXFxjaXJjIChmIFxcdGltZXMgZykiLDIseyJjdXJ2ZSI6Mn1dXQ==
\[\begin{tikzcd}
& {A \times KB} && {X \times KY} \\
@ -307,7 +295,7 @@ Of course there is also a symmetric version of this:
\arrow["{\tau \circ (id \times h^\#)}"', from=4-1, to=2-5]
\end{tikzcd}\]
\change[inline]{Be more specific}
\todo[inline]{introduce Diamond and Stutter laws}
\todo[inline]{Introduce Diamond and Stutter laws}
\end{proof}
\begin{theorem}
@ -315,7 +303,7 @@ Of course there is also a symmetric version of this:
\end{theorem}
\begin{proof}
\todo[inline]{proof that K is equational lifting}
\todo[inline]{Proof that K is equational lifting}
\end{proof}
\begin{theorem}
@ -323,5 +311,5 @@ Of course there is also a symmetric version of this:
\end{theorem}
\begin{proof}
Note that $\mathbf{K}$ is by definition a pre-Elgot monad.
\todo[inline]{proof that K is initial strong pre-Elgot}
\todo[inline]{Proof that K is initial strong pre-Elgot}
\end{proof}

18
thesis/src/05_setoids.tex
View file

@ -1,6 +1,6 @@
\chapter{A Case Study on Setoids}\label{chp:setoids}
In chapter~\ref{chp:partiality} we have argued that the delay monad is not an equational lifting monad, because it does not only model partiality but it also respects computation time. One way to remedy this is to take the quotient of the delay monad where computations with the same result are identified. In this chapter we will use the quotients-as-setoid approach, i.e. we will work in the category of setoids and show that the quotiented delay monad is the initial pre-Elgot monad in this category.
In chapter~\ref{chp:partiality} we have argued that the delay monad is not an equational lifting monad, because it does not only model partiality, but it also respects computation time. One way to remedy this is to take the quotient of the delay monad where computations with the same result are identified. In this chapter we will use the quotients-as-setoid approach, i.e. we will work in the category of setoids and show that the quotiented delay monad is the initial pre-Elgot monad in this category.
Let us introduce the category that we are working in:
@ -25,7 +25,7 @@ Setoids and setoid morphisms form a category that we call $\setoids$.
$\setoids$ is a distributive category.
\end{lemma}
\begin{proof}
To show that $\setoids$ is (co-)cartesian we will give the respective datatypes and unique morphisms, this also introduces notation we will use for the rest of the chapter. We will not include the proofs that the morphisms are setoid morphisms, these can be looked up in the agda standard library.
To show that $\setoids$ is (co-)cartesian we will give the respective data types and unique morphisms, this also introduces notation we will use for the rest of the chapter. We will not include the proofs that the morphisms are setoid morphisms, these can be looked up in the Agda standard library.
\begin{itemize}
\item \textbf{Products}:
@ -82,7 +82,7 @@ Setoids and setoid morphisms form a category that we call $\setoids$.
distributeˡ (x , i₁ y) = i₁ (x , y)
distributeˡ (x , i₂ y) = i₂ (x , y)
\end{minted}
Then these functions are inverse by definition and it is easy to show that they are setoid morphisms.
Then these functions are inverse by definition, and it is easy to show that they are setoid morphisms.
\end{proof}
\begin{lemma}
@ -90,7 +90,7 @@ Setoids and setoid morphisms form a category that we call $\setoids$.
\end{lemma}
\begin{proof}
We have already shown that $\setoids$ is cartesian, we need to show that given two setoids $(A, =^A), (B, =^B)$ we can construct an exponential object.
Indeed take the function space setoid $(A \rightarrow B, \doteq)$ where $\doteq$ is pointwise equality of setoid morphisms i.e. $f , g : A \rightarrow B$ are pointwise equal $f \doteq g$ \textit{iff} $f x =^B g x$ for any $x : A$. $curry$ and $eval$ are then defined as usual:
Indeed, take the function space setoid $(A \rightarrow B, \doteq)$ where $\doteq$ is point wise equality of setoid morphisms i.e. $f , g : A \rightarrow B$ are point wise equal $f \doteq g$ \textit{iff} $f x =^B g x$ for any $x : A$. $curry$ and $eval$ are then defined as usual:
\begin{minted}{agda}
curry : ∀ {a b c} {A : Set a} {B : Set b} {C : Set c}
→ (C × A → B) → C → A → B
@ -107,14 +107,14 @@ Setoids and setoid morphisms form a category that we call $\setoids$.
% 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$
Originally the delay monad has been introduced as a coinductive datatype with two constructors, in pseudo Agda-like code this would look something like:
Originally the delay monad has been introduced as a coinductive datatype with two constructors, in pseudo Agda like code this would look something like:
\begin{minted}{agda}
codata (A : Set) : Set where
now : A → Delay A
later : Delay A → Delay A
\end{minted}
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}
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}
\cite{nad-delay}
@ -128,7 +128,7 @@ record Delay′ (A : Set) : Set where
field force : Delay A
\end{minted}
Here \Verb{Delay} is defined as a inductive datatype where the coinductive part of the original definition (i.e. the coinductive occurence of the delay type in the \Verb{later} constructor) references a coinductive record \Verb{Delay'} which consists of only one field that forces a coinductive value to an inductive one.
Here \Verb{Delay} is defined as an inductive datatype where the coinductive part of the original definition (i.e. the coinductive occurrence of the delay type in the \Verb{later} constructor) references a coinductive record \Verb{Delay'} which consists of only one field that forces a coinductive value to an inductive one.
For the sake of readability we will introduce other concepts only by inference rules instead of Agda code, for the delay monad this looks like:
@ -190,9 +190,9 @@ Now we can relate two computations \textit{iff} they evaluate to the same result
\end{theorem}
\begin{proof}
We need to show that for every setoid $(A, =^A)$ the resulting setoid $(Delay\;A, \approx)$ can be extended to a stable free Elgot algebra.
Stability follows automatically by theorem~\ref{thm:stability} and the fact that $\setoids$ is cartesian closed, so it suffices to define a free elgot Algebra on $(Delay\;A, \approx)$.
Stability follows automatically by theorem~\ref{thm:stability} and the fact that $\setoids$ is cartesian closed, so it suffices to define a free Elgot Algebra on $(Delay\;A, \approx)$.
Let $(X , =^X) \in \obj{\setoids}$ and $f : X \rightarrow Delay\; A + X$ be a setoid morphism, we define $f^\# : X \rightarrow Delay\;A$ pointwise:
Let $(X , =^X) \in \obj{\setoids}$ and $f : X \rightarrow Delay\; A + X$ be a setoid morphism, we define $f^\# : X \rightarrow Delay\;A$ point wise:
\[
f^\# (x) :=
\begin{cases}