From cae7662b76b677912890803071c666c5c2ebe6f4 Mon Sep 17 00:00:00 2001 From: Leon Vatthauer Date: Sun, 11 Feb 2024 13:01:07 +0100 Subject: [PATCH] add todos --- .gitignore | 1 + thesis/main.tex | 10 +++++++ thesis/src/00_introduction.tex | 3 ++ thesis/src/01_preliminaries.tex | 13 ++++---- thesis/src/02_agda-categories.tex | 11 ++++--- thesis/src/04_iteration.tex | 50 ++++++++++++++++++++++++++++--- thesis/src/05_setoids.tex | 12 +++++++- 7 files changed, 82 insertions(+), 18 deletions(-) diff --git a/.gitignore b/.gitignore index 5af6080..7da4792 100644 --- a/.gitignore +++ b/.gitignore @@ -54,3 +54,4 @@ thesis/_minted-main/ slides/_minted-main/ thesis/main.bbl-SAVE-ERROR thesis/main.bcf-SAVE-ERROR +thesis/main.tdo diff --git a/thesis/main.tex b/thesis/main.tex index 2bbfefe..1ac6f0a 100644 --- a/thesis/main.tex +++ b/thesis/main.tex @@ -101,6 +101,9 @@ \usepackage{noto-mono} +\usepackage[colorinlistoftodos,prependcaption,textsize=tiny]{todonotes} +\usepackage{xargs} +\usepackage[dvipsnames]{xcolor} % Coloured text etc. %\usepackage{fontspec} %\setmonofont{Noto Sans Mono} @@ -122,6 +125,13 @@ Erlangen, \today{} \rule{7cm}{1pt}\\ \doclicenseThis{} \tableofcontents +\listoftodos + +\newcommandx{\unsure}[2][1=]{\todo[inline,linecolor=red,backgroundcolor=red!25,bordercolor=red,#1]{#2}} +\newcommandx{\change}[2][1=]{\todo[linecolor=blue,backgroundcolor=blue!25,bordercolor=blue,#1]{#2}} +\newcommandx{\info}[2][1=]{\todo[inline,linecolor=OliveGreen,backgroundcolor=OliveGreen!25,bordercolor=OliveGreen,#1]{#2}} +\newcommandx{\improvement}[2][1=]{\todo[inline,linecolor=Plum,backgroundcolor=Plum!25,bordercolor=Plum,#1]{#2}} + % \include{src/examples} \include{src/00_introduction} diff --git a/thesis/src/00_introduction.tex b/thesis/src/00_introduction.tex index f4ec3a1..9202a59 100644 --- a/thesis/src/00_introduction.tex +++ b/thesis/src/00_introduction.tex @@ -1 +1,4 @@ \chapter{Introduction} + +\info[inline]{use introductory example from talk} +\todo[inline]{give overview of thesis} \ No newline at end of file diff --git a/thesis/src/01_preliminaries.tex b/thesis/src/01_preliminaries.tex index be4e881..0c87eaf 100644 --- a/thesis/src/01_preliminaries.tex +++ b/thesis/src/01_preliminaries.tex @@ -2,15 +2,12 @@ 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. 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 $\mathcal{C}$, $id_X$ for the identity morphism on $X$ and $(-) \circ (-)$ for the composition of morphisms. +We write $\obj{C}$ for the objects of a category $\mathcal{C}$, $id_X$ for the identity morphism on $X$, $(-) \circ (-)$ for the composition of morphisms and $\mathcal{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. \section{Distributive and Cartesian Closed Categories} Let us first introduce notation for binary (co-)products by giving their usual diagrams: -% TODO products bind stronger than coproducts irgendwo erwähnen -% TODO notation $\mathcal{C}(X,Y)$ einführen - \begin{figure}[ht] % https://q.uiver.app/#q=WzAsOCxbMiwwLCJBIFxcdGltZXMgQiJdLFswLDAsIkEiXSxbNCwwLCJCIl0sWzIsMiwiQyJdLFs4LDAsIkEgKyBCIl0sWzYsMCwiQSJdLFsxMCwwLCJCIl0sWzgsMiwiQyJdLFswLDEsIlxccGlfMSIsMl0sWzAsMiwiXFxwaV8yIl0sWzMsMiwiZyIsMl0sWzMsMSwiZiJdLFszLDAsIlxcZXhpc3RzISBcXGxhbmdsZSBmICwgZyBcXHJhbmdsZSIsMix7InN0eWxlIjp7ImJvZHkiOnsibmFtZSI6ImRhc2hlZCJ9fX1dLFs1LDQsImlfMSJdLFs2LDQsImlfMiIsMl0sWzUsNywiZiIsMl0sWzYsNywiZyJdLFs0LDcsIlxcZXhpc3RzICEgW2YgLCBnXSIsMV1d \[\begin{tikzcd} @@ -31,7 +28,7 @@ Let us first introduce notation for binary (co-)products by giving their usual d \caption{The defining diagrams of products and coproducts} \end{figure} -We will furthermore overload this notation and write $f \times g := \langle f \circ \pi_1 , g \circ \pi_2 \rangle$ and $f + g := \lbrack i_1 \circ f , i_2 \circ g \rbrack$ on morphisms. +We will furthermore overload this notation and write $f \times g := \langle f \circ \pi_1 , g \circ \pi_2 \rangle$ and $f + g := \lbrack i_1 \circ f , i_2 \circ g \rbrack$ on morphisms. To avoid parentheses we will use the convention that products bind stronger than coproducts. 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 $\text{!`} : A \rightarrow 0$. @@ -97,7 +94,6 @@ Categories with finite products (i.e. binary products and a terminal object) are \end{proof} \begin{definition}[Exponential Object] - % TODO introduce notation | C | Let $\mathcal{C}$ be a cartesian category and $X , Y \in \vert \mathcal{C} \vert$. An object $X^Y$ is called an exponential object (of $X$ and $Y$) if there exists an evaluation morphism $eval : X^Y \times Y \rightarrow X$ and for any $f : X \times Y \rightarrow Z$ there exists a morphism $curry\; f : X \rightarrow Z^Y$ that is unique with respect to the following diagram: % https://q.uiver.app/#q=WzAsMyxbMCwwLCJaIFxcdGltZXMgWSJdLFsyLDAsIlheWSBcXHRpbWVzIFkiXSxbMiwyLCJYIl0sWzEsMiwiZXZhbCJdLFswLDEsImN1cnJ5XFw7ZiBcXHRpbWVzIGlkIl0sWzAsMiwiZiIsMl1d @@ -116,6 +112,8 @@ The internal logic of cartesian closed categories is the simply typed $\lambda$- \section{Stable Natural Numbers Object} +\unsure[inline]{Introduce NNO? Actually not needed!} + \section{Monads} Monads are widely known among programmers as a way of modelling effects in pure languages and are also central to this thesis. Let's recall the basic definitions\cite{Lane1971}\cite{moggi}. @@ -139,6 +137,7 @@ For programmers a second equivalent definition is more useful: \end{alignat*} \end{definition} +\change[inline]{Rewrite this paragraph, it's not so good} In functional programming languages like Haskell the Kleisli lifting $(-)^*$ is usually called \textit{bind} or written infix as \mintinline{haskell}{>>=} and $\eta$ is called $return$. Given two programs $f : X \rightarrow MY, g : Y \rightarrow MZ$, where $M$ is a Kleisli triple the composition $g^* \circ f$ can then be (in a pointful manner) written as \mintinline{haskell}{f x >>= g} or using Haskell's do-notation: \begin{minted}{haskell} do y <- f x @@ -214,6 +213,6 @@ Now we can express the above condition: \end{definition} \section{Free Objects} - +\todo[inline]{Definition of free objects} For the rest of this thesis we will work in an ambient distributive category $\mathcal{C}$ that has a stable natural numbers object $\mathbb{N}$. \ No newline at end of file diff --git a/thesis/src/02_agda-categories.tex b/thesis/src/02_agda-categories.tex index a3f6a98..13c6737 100644 --- a/thesis/src/02_agda-categories.tex +++ b/thesis/src/02_agda-categories.tex @@ -4,8 +4,7 @@ There are many formalizations of category theory in proof assistants like Coq or Also ideally such a development will bring researchers together and enable them to work in a unified setting. In this thesis we will work with the dependently typed programming language Agda~\cite{agda} and the agda-categories~\cite{agda-categories} library by Jason Hu and Jacques Carette that gives us a good foundation of categorical definitions to work with. This section shall serve as a quick introduciton to the library. - -% In this section we will talk about some design decisions that Hu and Carette made in their library that influence this development. This also serves as a quick introduction to the library. +\change[inline]{rewrite intro text, goal of chapter changed to introducing the thesis project} \section{Setoid Enriched Categories} The usual textbook definition of category hides some design decisions that have to be made when implementing it in type theory. One would usually see something like this: @@ -22,10 +21,8 @@ where the composition is associative and the identity morphisms are identities w Here a \textit{collection} usually is something that behaves set-like, but prevents size issues (there is no collection of all collections, preventing Russel's Paradox), it is not instantly clear how to translate this to a proof assistant. 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 Agda we need to be more thorough, there is no global notion of equality that 'just works', e.g. the standard notion of propositional equality has trouble dealing with functions and needs 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 \mintinline{agda}|Set| hierarchy is utilized to prevent size issues, i.e. the whole category is 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 set of all morphisms, instead it contains a set of morphisms for any pair of objects. Furthermore the sets of morphisms are equipped with an equivalence relation \mintinline{agda}|_≈_|, making them setoids. This solves the aforementioned issue of how to implement equality between morphisms, it is just added to the definition of a category. This kind of category is also called a \textit{setoid-enriched category}. -Because of this proofs like \mintinline{agda}|∘-resp-≈| are needed throughout the library to make sure that operations on morphisms respect the equivalence relation. Lastly, the authors also add symmetric proofs like \mintinline{agda}|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 \mintinline{agda}|identity²|, we won't address the need for these proofs and just accept the requirement as given for the rest of the thesis. - -% For the rest of this thesis we will assume familiarity with basic concepts of category theory (like functors and natural transformations)~\cite{Lane1971}. We will not explain how they are implemented in order to look at more interesting concepts, for that one should seek out the agda-categories library (\href{https://github.com/agda/agda-categories}{Github}) or consult \cite{agda-categories}. We will however introduce further categorical notions using only their agda representation, it goes without saying that every time we say category, we actually mean setoid-enriched category as defined above. +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, i.e. the whole category is 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 set of all morphisms, instead it contains a set of morphisms for any pair of objects. Furthermore the sets of morphisms are equipped with an equivalence relation \Verb{_≈_}, making them setoids. This solves the aforementioned issue of how to implement equality between morphisms, it is just added to the definition of a category. This kind of category is also called a \textit{setoid-enriched category}. +Because of this proofs like \Verb{∘-resp-≈} are needed throughout the library to make sure that operations on morphisms respect the equivalence relation. Lastly, the authors also add 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} @@ -59,6 +56,8 @@ From this it should be clear how other basic notions like functors or natural tr \section{The formalization} +\improvement{explain more} + The agda formalization of this thesis is structured similar to the agda-categories library, e.g. 'big' concepts like monads and categories get a top-level folder, that itself contains the core definitions, 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). \ No newline at end of file diff --git a/thesis/src/04_iteration.tex b/thesis/src/04_iteration.tex index 18891aa..4400672 100644 --- a/thesis/src/04_iteration.tex +++ b/thesis/src/04_iteration.tex @@ -2,7 +2,8 @@ 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. \section{Elgot Algebras} -% TODO check everything here more thoroughly +\improvement{Add some text} +\unsure[inline]{Check types etc.} \begin{definition}[Elgot Algebra] A (unguarded) Elgot Algebra~\cite{uniformelgot} consists of: @@ -19,7 +20,7 @@ In this chapter we will draw on the inherent connection between recursion and it \end{itemize} \end{definition} -A morphism between Elgot algebras $h : (A, (-)^{\#_a}) \rightarrow (B, (-)^{\#_a})$ is an iteration preserving morphism $h : A \rightarrow B$ i.e. a morphism satisfying: $h \circ f^{\#_a} = ((h + id) \circ f)^{\#_b}$ +A morphism between Elgot algebras $h : (A, (-)^{\#_a}) \rightarrow (B, (-)^{\#_a})$ is an iteration preserving morphism $h : A \rightarrow B$ i.e. a morphism satisfying: $h \circ f^{\#_a} = ((h + id) \circ f)^{\#_b}$ for any $f : X \rightarrow A + X$. \begin{theorem} Elgot algebras on a category $\mathcal{C}$ and the morphisms between them form a category that we call $\mathit{Elgot}(\mathcal{C})$. @@ -37,12 +38,45 @@ A morphism between Elgot algebras $h : (A, (-)^{\#_a}) \rightarrow (B, (-)^{\#_a The laws concerning $id$ and composition follow directly since they hold in $\mathcal{C}$. \end{proof} +\improvement{Add some text} + +\begin{lemma} + If $\mathcal{C}$ is a cartesian category, so is $\mathit{Elgot}(\mathcal{C})$. +\end{lemma} + +\begin{proof} + Let $1$ be the terminal object of $\mathcal{C}$. Given $f : X \rightarrow 1 + X$ we define the iteration $f^\# =\;! : X \rightarrow 1$ as the unique morphism into the terminal object. The laws of Elgot algebras then follow instantly, i.e. $(1 , !)$ is an Elgot algebra and it is the terminal object in $\mathit{Elgot}(\mathcal{C})$ since $!$ is trivially iteration preserving. + + Let $(A, (-)^{\#_a}) , (B, (-)^{\#_b}) \in \vert\mathit{Elgot}(\mathcal{C})\vert$ and $A \times B$ be the product in $\mathcal{C}$. Given $f : X \rightarrow (A \times B) + X$ we define the iteration as: + \[f^\# = \langle ((\pi_1 + id) \circ f)^{\#_a} , ((\pi_2 + id) \circ f)^{\#_b} \rangle : X \rightarrow A \times B\] + Then $(A \times B, (-)^\#)$ is indeed an Elgot algebra, the laws follow by the laws of the algebras on A and B. + + The product diagram of $A \times B$ in $\mathcal{C}$ then also holds in $\mathit{Elgot}(\mathcal{C})$, we just have to check that the projections are iteration preserving, which follows instantly, and that the unique morphism $\langle f , g \rangle$ is iteration preserving for any $f : (Z, (-)^{\#_z}) \rightarrow (X, (-)^{\#_x}), g : (Z, (-)^{\#_z}) \rightarrow (Y, (-)^{\#_y})$, which follows since $f$ and $g$ are iteration preserving. +\end{proof} + +\improvement{Add some text} +\todo[inline]{add Exponentials} + +\begin{lemma} + +\end{lemma} + \section{Pre-Elgot Monads} +\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. \[h^* \circ f^\# = ((h^* + id) \circ f)^\#\qquad \text{for}\; f : Z \rightarrow TX + Z, h : X \rightarrow TY\] \end{definition} + + +\begin{remark}[Strong pre-Elgot Monad] + A pre-Elgot monad $\mathbf{T}$ is strong if $\mathbf{T}$ is a strong monad and the strength $\tau$ is iteration preserving in the following sense: + \[\tau \circ (id \times f^\#) = ((\tau + id) \circ dstl \circ (id \times f))^\#\] + \change[inline]{be more concrete with types here} +\end{remark} + \section{The Initial 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 pre-Elgot monad. @@ -90,9 +124,17 @@ We get the following dual definition: We will usually refer to right-stable free Elgot algebras as just stable Elgot algebras. +\todo[inline]{proof that KX stable in CCC} + \begin{theorem} In a cartesian closed category every free Elgot algebra is stable. \end{theorem} \begin{proof} - asd -\end{proof} \ No newline at end of file + TODO +\end{proof} + +\todo[inline]{proof that K is strong and commutative} + +\todo[inline]{proof that K is equational lifting} + +\todo[inline]{proof that K is initial strong pre-Elgot} \ No newline at end of file diff --git a/thesis/src/05_setoids.tex b/thesis/src/05_setoids.tex index fe22860..a4b28c7 100644 --- a/thesis/src/05_setoids.tex +++ b/thesis/src/05_setoids.tex @@ -1 +1,11 @@ -\chapter{A Case Study on Setoids}\label{chp:setoids} \ No newline at end of file +\chapter{A Case Study on Setoids}\label{chp:setoids} + +\todo[inline]{Introduce category of setoids} + +\todo[inline]{introduce delay monad in agda (coinductive types)} + +\todo[inline]{quotient of delay} + +\todo[inline]{proof: delay is monad} + +\todo[inline]{proof: delay is free elgot}