Work on slides

slides/bibliography.bib

@@ -1,15 +1,21 @@
 @article{eqlm,
-  title    = {Equational Lifting Monads},
+  author     = {Bucalo, Anna and F\"{u}hrmann, Carsten and Simpson, Alex},
-  journal  = {Electronic Notes in Theoretical Computer Science},
+  title      = {An Equational Notion of Lifting Monad},
-  volume   = {29},
+  year       = {2003},
-  pages    = {22},
+  issue_date = {15 February 2003},
-  year     = {1999},
+  publisher  = {Elsevier Science Publishers Ltd.},
-  note     = {CTCS '99, Conference on Category Theory and Computer Science},
+  address    = {GBR},
-  issn     = {1571-0661},
+  volume     = {294},
-  doi      = {https://doi.org/10.1016/S1571-0661(05)80303-2},
+  number     = {1–2},
-  url      = {https://www.sciencedirect.com/science/article/pii/S1571066105803032},
+  issn       = {0304-3975},
-  author   = {Anna Bucalo and Carsten Führmann and Alex Simpson},
+  url        = {https://doi.org/10.1016/S0304-3975(01)00243-2},
-  abstract = {We introduce the notion of an “equational lifting monad” : a commutative strong monad satisfying one additional equation (valid for monads arising from partial map classifiers). We prove that any equational lifting monad has a representation by a partial map classifier such that the Kleisli category of the former fully embeds in the partial category of the latter. Thus equational lifting monads precisely capture the (partial) equational properties of partial map classifiers. The representation theorem also provides a tool for transferring non-equational properties of partial map classifiers to equational lifting monads.}
+  doi        = {10.1016/S0304-3975(01)00243-2},
+  abstract   = {We introduce the notion of an equational lifting monad: a commutative strong monad satisfying one additional equation (valid for monads arising from partial map classifiers). We prove that any equational lifting monad has a representation by a partial map classifier such that the Kleisli category of the former fully embeds in the partial category of the latter. Thus, equational lifting monads precisely capture the equational properties of partial maps as induced by partial map classifiers. The representation theorem also provides a tool for transferring nonequational properties of partial map classifiers to equational lifting monads. It is proved using a direct axiomatization of Kleisli categories of equational lifting monads. This axiomatization is of interest in its own right.},
+  journal    = {Theor. Comput. Sci.},
+  month      = {2},
+  pages      = {31–60},
+  numpages   = {30},
+  keywords   = {premonoidal categories, categories, partiality and partial categories, abstract Kleish, commutative strong monads}
 }
 
 @article{moggi,
@@ -30,6 +36,18 @@
   numpages   = {38}
 }
 
+@article{quotienting,
+  title     = {Quotienting the delay monad by weak bisimilarity},
+  volume    = {29},
+  doi       = {10.1017/S0960129517000184},
+  number    = {1},
+  journal   = {Mathematical Structures in Computer Science},
+  publisher = {Cambridge University Press},
+  author    = {CHAPMAN, JAMES and UUSTALU, TARMO and VELTRI, NICCOLÒ},
+  year      = {2019},
+  pages     = {67–92}
+}
+
 @article{restriction,
   author     = {Cockett, J. R. B. and Lack, Stephen},
   title      = {Restriction Categories I: Categories of Partial Maps},

slides/main.tex

@@ -51,7 +51,7 @@
 % Setup for Titlepage
 % ----------------------------------------------------------------------------------------
 \title{Implementing Categorical Notions of Partiality and Delay in Agda}
-\subtitle{Subtitle}
+% \subtitle{Subtitle}
 \author[L. Vatthauer]{
 Leon Vatthauer%\inst{1}
 }

slides/sections/01_abstracting.tex

@@ -9,7 +9,7 @@ Goal: interpret an effectul programming language in a category $\mathcal{C}$
 \end{itemize}
 
 \onslide<4->
-What properties should a partiality monad $T$ have?
+What properties should a monad $T$ for modelling partiality have?
 
 \begin{enumerate}
   \item<5-> Commutativity (also entails strength), i.e. the following programs should yield equal results:
@@ -27,7 +27,8 @@ What properties should a partiality monad $T$ have?
       \end{minted}
     \end{multicols}
     where p and q are programs.  
-  \item<6-> Morphisms in $\mathcal{C}_T$ should be partial maps (How?)
+  \item<6-> Morphisms in $\mathcal{C}_T$ should be partial maps
+  \item<7-> There should be no other effect besides partiality
 \end{enumerate}
 
 \end{frame}
@@ -55,7 +56,7 @@ Intuitively $\tdom f$ captures the domain of definiteness of $f$.
 \end{frame}
 
 \begin{frame}[t, fragile]{Capturing Partiality Categorically}{Equational Lifting Monads~\cite{eqlm}}
-  The following criterion is sufficient for guaranteeing that the kleisli category is a restriction category:
+  The following criterion guarantees that some form of partiality is the only possible side-effect:
   \pause
   \begin{definition}
     A commutative monad $T$ is called an \textit{equational lifting monad} if the following diagram commutes:
@@ -76,14 +77,15 @@ Intuitively $\tdom f$ captures the domain of definiteness of $f$.
   \end{theorem}
 \end{frame}
 
-% TODO is the maybe monad an equational lifting monad? Ask sergey
+% write on board:
+% equational lifting: do x <- p; return (return x, x) = do x <- p; return (p, x)
 
 \begin{frame}[t, fragile]{The Maybe Monad}
 \begin{itemize}[<+->]
   \item $MX = X + 1$
   \item on a distributive category the maybe monad is strong and commutative:
     \[ \tau_{X,Y} := X \times (Y + 1) \overset{dstr}{\longrightarrow} (X \times Y) + (X \times 1) \overset{id+1}{\longrightarrow} (X \times Y) + 1 \]
-  \item and the following diagram commutes (i.e. it's an equational lifting monad):
+  \item and the following diagram commutes (i.e. it is an equational lifting monad):
     % https://q.uiver.app/#q=WzAsNCxbMCwwLCJYKzEiXSxbMywwLCIoWCsxKVxcdGltZXMoWCsxKSJdLFszLDIsIigoWCsxKVxcdGltZXMgWCkgKygoWCsxKVxcdGltZXMgMSkiXSxbMyw0LCIoKFgrMSlcXHRpbWVzIFgpKzEiXSxbMCwxLCJcXERlbHRhIl0sWzEsMiwiZHN0ciJdLFsyLDMsImlkKyEiXSxbMCwzLCJcXGxhbmdsZSBpbmwsaWRcXHJhbmdsZSArICEiLDJdXQ==
     \[\begin{tikzcd}
       {X+1} &&& {(X+1)\times(X+1)} \\
@@ -100,26 +102,83 @@ Intuitively $\tdom f$ captures the domain of definiteness of $f$.
 \end{itemize}
 \end{frame}
 
-% TODO is delay equational lifting?? maybe rethink the story here...
-
 \begin{frame}[t, fragile]{The Delay Monad}
-\begin{itemize}
+\begin{itemize}[<+->]
   \item Recall the delay codatatype:
     
     \[\mprset{fraction={===}}
-    \inferrule {\;} {now\; x : DX}\hskip 2cm
+    \inferrule {x : X} {now\; x : DX}\hskip 2cm
     \inferrule {c : DX} {later\; c : DX}\]
 
-  \item Categorically: $DX = \nu \gamma. X + \gamma$
+  \item Categorically: $DX = \nu A. X + A$
+  \item By Lambek we get $DX \cong X + DX$ which yields:
+  \begin{alignat*}{2}
+    &out &&: DX \rightarrow X + DX\\
+    &out^{-1} &&: X + DX \rightarrow DX = [ now , later ]
+  \end{alignat*}
   \item $D$ (if it exists) is a strong and commutative monad (on a cartesian, cocartesian, distributive category)
+  \item $D$ is not an equational lifting monad, because besides modelling partiality, it also counts steps \\(e.g. $now\; c \not= later\; (now\; c)$)
 \end{itemize}
 \end{frame}
 
-\begin{frame}[t, fragile]{Partiality from iteration}
+% write on board:
-\begin{itemize}
+% \eta = now
-  \item Elgot-Algebras
+% given f : X \rightarrow TY, f* is defined by corecursion.
-  \item Free Elgot-Algebras yield monad K
+
-  \item K is equational lifting
+
-  \item K instantiates to maybe and delay
+
-\end{itemize}
+%%%%%%%%
-\end{frame}
+% NOTE:
+% quotienting D should be covered later in the agda chapter, not here!
+
+% \begin{frame}[t, fragile]{The quotiented Delay Monad}
+%   Following the work in~\cite{quotienting} we quotient $D$ by weak bisimilarity: 
+%   \[\mprset{fraction={===}}
+%   \inferrule {p \downarrow c \\ q \downarrow c} {p \approx q}\hskip 2cm
+%   \inferrule {p \approx q} {later\; p \approx later\; q}\]
+
+% \end{frame}
+%%%%%%%
+
+\begin{frame}[t, fragile]{Partiality from Iteration}{Elgot Algebras}
+The following is an adaptation of Ad\'amek, Milius and Velebil's \textit{complete Elgot Algebras}:
+\begin{definition}
+  A (unguarded) Elgot Algebra consists of:
+  \begin{itemize}
+    \item An object X
+    \item for every $f : S \rightarrow X + S$ the iteration $f^\# : S \rightarrow X$, satisfying:
+    \begin{itemize}
+      \item \textbf{Fixpoint}: $f^\# = [ id , f ^\# ] \circ f$
+      \item \textbf{Uniformity}: $(id + h) \circ f = g \circ h \Rightarrow f ^\# = g^\# \circ h$
+      \\ for $f : S \rightarrow X + S,\; g : R \rightarrow A + R,\; h : S \rightarrow R$
+      \item \textbf{Folding}: $((f^\# + id) \circ h)^\# = [ (id + inl) \circ f , inr \circ h ] ^\#$
+      \\ for $f : S \rightarrow A + S,\; h : R \rightarrow S + R$
+    \end{itemize}
+  \end{itemize}
+\end{definition}
+\pause
+\begin{block}{Remark}
+  Every Elgot algebra $(A, (-)^\#)$ comes with a divergence constant $\bot = (inr : 1 \rightarrow A + 1)^\# : 1 \rightarrow A$
+\end{block}
+\end{frame}
+
+
+% TODO 
+% maybe dont talk about elgot monads at all, give intuition for the initial pre Elgot monad.
+\begin{frame}[t, fragile]{Partiality from Iteration}{pre-Elgot Monads}
+  TODO
+\end{frame}
+
+\begin{frame}[t, fragile]{Partiality from iteration}{The K Monad}
+  \begin{itemize}[<+->]
+    \item By defining $KX$ as the free Elgot algebra over $X$ we get a monad $K$
+    \item $K$ is strong and commutative
+    \item $K$ is an equational lifting monad
+    \item $K$ is the initial pre-Elgot monad
+  \end{itemize}
+\end{frame}
+
+
+%% TODOs:
+% cite stefan
+% cite sergey

slides/sections/02_goals.tex

@@ -2,9 +2,18 @@
 
 \begin{frame}[t, fragile]{Goals}
   \begin{itemize}
-    \item Formalize delay monad (categorically as terminal coalgebra) + properties
+    \item Formalize the delay monad categorically and show that it is..
-    \item Formalize K + properties
+    \begin{itemize}
-    \item Case study on Setoids
+      \item strong
+      \item commutative
+    \end{itemize}
+    \item Formalize K and show that it is..
+    \begin{itemize}
+      \item strong
+      \item commutative
+      \item an equational lifting monad
+    \end{itemize}
+    \item Take the category of setoids and show that $K$ instantiates to $D$ quotiented by weak-bisimilarity
   \end{itemize}
 \end{frame}
 
@@ -12,13 +21,7 @@
   agda-categories
 \end{frame}
 
-\begin{frame}[t, fragile]{What I managed to show}
+\begin{frame}[t, fragile]{Resumee}
-  TODO
+  On doing category theory in agda
-\end{frame}
+  (pro/con)
-
-\begin{frame}[t, fragile]{Further work}
-\begin{itemize}
-  \item Show that $\tilde{D}$ is monad (under conditions)
-  \item Show that $K \cong \tilde{D}$ (under conditions)
-\end{itemize}
 \end{frame}