diff --git a/slides/bibliography.bib b/slides/bibliography.bib index 825ed34..e7a9291 100644 --- a/slides/bibliography.bib +++ b/slides/bibliography.bib @@ -35,7 +35,9 @@ number = {2}, journal = {Mathematical Structures in Computer Science}, publisher = {Cambridge University Press}, - author = {ADÁMEK, JIŘÍ and MILIUS, STEFAN and VELEBIL, JIŘÍ}, + author = {Jir{\'{\i}} Ad{\'{a}}mek and + Stefan Milius and + Jir{\'{\i}} Velebil}, year = {2011}, pages = {417–480} } diff --git a/slides/main.tex b/slides/main.tex index 3ffe3a6..965005c 100644 --- a/slides/main.tex +++ b/slides/main.tex @@ -7,7 +7,7 @@ % of the GNU Public License, version 2. % % ------------------------------------------------------------------------------ -\documentclass[final, handout]{beamer} +\documentclass[final]{beamer} % ======================================================================================== % Theme: inner, outer, font and colors @@ -46,7 +46,7 @@ % custom commands for symbols \usepackage{styles/symbols} - +\newcommand*\quot[2]{{^{\textstyle #1}\big/_{\textstyle #2}}} % ======================================================================================== % Setup for Titlepage % ---------------------------------------------------------------------------------------- @@ -87,7 +87,7 @@ Leon Vatthauer%\inst{1} sortcites=true,% sort citations when multiple entries are passed to one cite command doi=true,% isbn=false,% - url=false,% + % url=false,% eprint=false,% backend=biber% ]{biblatex} @@ -195,7 +195,7 @@ at (#3) {#4}; \input{sections/02_goals.tex} % bibliography - \begin{frame}[t]{Bibliography} + \begin{frame}[allowframebreaks]{Bibliography} \printbibliography[heading=none] \end{frame} diff --git a/slides/sections/01_abstracting.tex b/slides/sections/01_abstracting.tex index 01e5903..4d80183 100644 --- a/slides/sections/01_abstracting.tex +++ b/slides/sections/01_abstracting.tex @@ -36,7 +36,7 @@ What properties should a monad $T$ for modelling partiality have? \begin{frame}[t, fragile]{Capturing Partiality Categorically}{Preliminaries} We work in category $\mathcal{C}$ that - \begin{itemize} + \begin{itemize}[<+->] \item has finite products \item has finite coproducts \item is distributive, i.e. the following is an iso: @@ -50,6 +50,7 @@ What properties should a monad $T$ for modelling partiality have? {X \times (Y + Z)} &&&& {(X \times Y) + (X \times Z)} \arrow["dstl", from=1-1, to=1-5] \end{tikzcd}\] + \item has a natural numbers object $\mathbb{N}$ (which is stable) \end{itemize} \end{frame} @@ -65,7 +66,7 @@ What properties should a monad $T$ for modelling partiality have? \tdom(g \circ (\tdom f)) &= (\tdom g) \circ (\tdom f)\\ (\tdom h) \circ f &= f \circ \tdom (h \circ f) \end{alignat} - for any $X, Y, Z \in \vert\mathcal{C}\vert, f : X \rightarrow KY, g : X \rightarrow KZ, h: Y \rightarrow KZ$. + for any $X, Y, Z \in \vert\mathcal{C}\vert, f : X \rightarrow Y, g : X \rightarrow Z, h: Y \rightarrow Z$. \end{definition} \onslide<2-> @@ -104,8 +105,8 @@ Intuitively $\tdom f$ captures the domain of definedness of $f$. \begin{frame}[t, fragile]{Capturing Partiality Categorically}{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 The maybe monad is strong and commutative: + \[ \tau_{X,Y} := X \times (Y + 1) \overset{dstl}{\longrightarrow} (X \times Y) + (X \times 1) \overset{id+!}{\longrightarrow} (X \times Y) + 1 \] \item and the following diagram commutes (i.e. it is an equational lifting monad): % https://q.uiver.app/#q=WzAsNCxbMCwwLCJYKzEiXSxbMywwLCIoWCsxKVxcdGltZXMoWCsxKSJdLFszLDIsIigoWCsxKVxcdGltZXMgWCkgKygoWCsxKVxcdGltZXMgMSkiXSxbMyw0LCIoKFgrMSlcXHRpbWVzIFgpKzEiXSxbMCwxLCJcXERlbHRhIl0sWzEsMiwiZHN0ciJdLFsyLDMsImlkKyEiXSxbMCwzLCJcXGxhbmdsZSBpbmwsaWRcXHJhbmdsZSArICEiLDJdXQ== \[\begin{tikzcd} @@ -115,7 +116,7 @@ Intuitively $\tdom f$ captures the domain of definedness of $f$. \\ &&& {((X+1)\times X)+1} \arrow["\Delta", from=1-1, to=1-4] - \arrow["dstr", from=1-4, to=3-4] + \arrow["dstl", from=1-4, to=3-4] \arrow["{id+!}", from=3-4, to=5-4] \arrow["{\langle inl,id\rangle + !}"', from=1-1, to=5-4] \end{tikzcd}\] @@ -131,13 +132,13 @@ Intuitively $\tdom f$ captures the domain of definedness of $f$. \inferrule {x : X} {now\; x : DX}\hskip 2cm \inferrule {c : DX} {later\; c : DX}\] - \item Categorically: $DX = \nu A. X + A$ + \item $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$ (if it exists) is a strong and commutative monad \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} @@ -146,25 +147,34 @@ Intuitively $\tdom f$ captures the domain of definedness of $f$. % \eta = now % given f : X \rightarrow TY, f* is defined by corecursion. +\begin{frame}[t, fragile]{Capturing Partiality Categorically}{Quotienting the Delay Monad~\cite{quotienting}} + Following the work by Chapman, Uustalu and Veltri we can quotient $D$ by the 'correct' kind of equality: + \[\mprset{fraction={===}} + \inferrule {p \downarrow c \\ q \downarrow c} {p \approx q}\hskip 2cm + \inferrule {p \approx q} {later\; p \approx later\; q}\] + \pause + where + \[ + \inferrule {\;} {now\;c \downarrow c}\hskip 2cm + \inferrule {x \downarrow c} {later\; x \downarrow c}\] + \pause + we can model this as the coequalizer: + % https://q.uiver.app/#q=WzAsMyxbMCwwLCJEKFhcXHRpbWVzIFxcbWF0aGJie059KSJdLFsyLDAsIkRYIl0sWzQsMCwiRF9cXGFwcHJveCJdLFswLDEsIlxcaW90YV4qIiwwLHsib2Zmc2V0IjotMn1dLFswLDEsIkQgZnN0IiwyLHsib2Zmc2V0IjoyfV0sWzEsMiwiXFxyaG9fWCJdXQ== + \[\begin{tikzcd} + {D(X\times \mathbb{N})} && DX && {D_\approx X} + \arrow["{\iota^*}", shift left=2, from=1-1, to=1-3] + \arrow["{D fst}"', shift right=2, from=1-1, to=1-3] + \arrow["{\rho_X}", from=1-3, to=1-5] + \end{tikzcd}\] + \pause + \textbf{Problem}: Defining $\mu_X : D_\approx^2 X \rightarrow D_\approx X$ requires countable choice. +\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~\cite{elgotalgebras}} -The following is an adaptation of Ad\'amek, Milius and Velebil's \textit{complete Elgot Algebras}: +\begin{frame}[t, fragile]{Partiality from Iteration}{Elgot Algebras} +\pause +The following is an adaptation of Ad\'amek, Milius and Velebil's \textit{complete Elgot Algebras}~\cite{elgotalgebras}: \begin{definition} - A (unguarded) Elgot Algebra consists of: + A (unguarded) Elgot Algebra~\cite{uniformelgot} consists of: \begin{itemize} \item An object X \item for every $f : S \rightarrow X + S$ the iteration $f^\# : S \rightarrow X$, satisfying: @@ -184,16 +194,20 @@ The following is an adaptation of Ad\'amek, Milius and Velebil's \textit{complet \end{frame} \begin{frame}[t, fragile]{Partiality from Iteration}{Elgot Monads~\cite{elgotmonad}} -Recall the following notion: \begin{definition} A monad $\mathbf{T}$ is an Elgot monad if it has an iteration operator $(f : X \rightarrow T(Y + X))^\dagger : X \rightarrow TY$ satisfying: \begin{itemize} - \item \textbf{Fixpoint}: - \item \textbf{Naturality}: - \item \textbf{Codiagonal}: - \item \textbf{Uniformity}: + \item \textbf{Fixpoint}: $f^\dagger = [ \eta , f^\dagger ]^* \circ f$ + \\for $f : X \rightarrow T(Y + X)$ + \item \textbf{Uniformity}: $f \circ h = T(id + h) \circ g \Rightarrow f^\dagger \circ h = g^\dagger$ + \\for $f : X \rightarrow T(Y + X) , g : Z \rightarrow T(Y + Z)$ + \item \textbf{Naturality}: $g^* \circ f^\dagger = ([ (T inl) \circ g , \eta \circ inr ]^* \circ f )^\dagger$ + \\for $f : X \rightarrow T(Y + X), g : Y \rightarrow TZ$ + \item \textbf{Codiagonal}: $f^{\dagger\dagger} = (T[id , inr ] \circ f)^\dagger$ + \\for $f : X \rightarrow T((Y + X) + X)$ \end{itemize} \end{definition} +\pause \begin{block}{Remark} Strong Elgot Monads are regarded as minimal semantic structures for interpreting effectful while-languages. \end{block} @@ -209,6 +223,7 @@ Strong Elgot Monads are regarded as minimal semantic structures for interpreting 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} + \pause \begin{theorem} Every Elgot monad is pre-Elgot \end{theorem} @@ -216,15 +231,33 @@ Strong Elgot Monads are regarded as minimal semantic structures for interpreting \begin{frame}[t, fragile]{Partiality from iteration}{The initial pre-Elgot Monad~\cite{uniformelgot}} \begin{itemize}[<+->] - \item By defining $KX$ as the free Elgot algebra over $X$ we get a monad $K$ + \item By defining $KX$ as the free Elgot algebra over $X$ we get a monad $K$ (that we assume is stable) \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} -\begin{frame}[t, fragile]{Partiality from iteration}{Closing the gap} - ... +\begin{frame}[t, fragile]{Partiality from iteration}{Closing the gap~\cite{uniformelgot}} + Let's look at $\mathbf{K}$ under various assumptions: + \begin{itemize}[<+->] + \item \textbf{Assuming excluded middle:} + + \begin{itemize}[<+->] + \item The initial pre-Elgot monad and the initial Elgot monad coincide + \item $DX \cong X \times \mathbb{N} + 1$ + \item $D_\approx X \cong X + 1$ + \item $X + 1$ is the initial (pre-)Elgot monad ($\Rightarrow K \cong (-)+1 \cong D_\approx$) + \end{itemize} + + % \\$\Rightarrow$ $X+1$ is the initial pre-Elgot Monad and also the initial Elgot Monad. + \item \textbf{Assuming countable choice:} + \begin{itemize}[<+->] + \item The initial pre-Elgot monad and the initial Elgot monad coincide + \item $D_\approx$ is the initial (pre-)Elgot Monad ($\Rightarrow K \cong D_\approx$). + \end{itemize} + + \end{itemize} \end{frame} diff --git a/slides/sections/02_goals.tex b/slides/sections/02_goals.tex index 2587f22..0c8e7c2 100644 --- a/slides/sections/02_goals.tex +++ b/slides/sections/02_goals.tex @@ -1,7 +1,7 @@ \section{Implementation in Agda} \begin{frame}[t, fragile]{Goals} - \begin{itemize} + \begin{itemize}[<+->] \item Formalize the delay monad categorically and show that it is.. \begin{itemize} \item strong @@ -13,15 +13,27 @@ \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 + \item Take the category of setoids and show that $K$ instantiates to $D_\approx$ \end{itemize} \end{frame} -\begin{frame}[t, fragile]{Category theory in Agda} - agda-categories -\end{frame} +\begin{frame}[t, fragile, blank]{Category Theory in Agda}{Setoid-enriched Categories} + \begin{minted}{agda} +record Category (o ℓ e : Level) : Set (suc (o ⊔ ℓ ⊔ e)) where + field + Obj : Set o + _⇒_ : Obj → Obj → Set ℓ + _≈_ : ∀ {A B} → (A ⇒ B) → (A ⇒ B) → Set e -\begin{frame}[t, fragile]{Resumee} - On doing category theory in agda - (pro/con) + id : ∀ {A} → (A ⇒ A) + _∘_ : ∀ {A B C} → (B ⇒ C) → (A ⇒ B) → (A ⇒ C) + + field + assoc : ∀ {A B C D} {f : A ⇒ B} {g : B ⇒ C} {h : C ⇒ D} + → (h ∘ g) ∘ f ≈ h ∘ (g ∘ f) + identityˡ : ∀ {A B} {f : A ⇒ B} → id ∘ f ≈ f + identityʳ : ∀ {A B} {f : A ⇒ B} → f ∘ id ≈ f + equiv : ∀ {A B} → IsEquivalence (_≈_ {A} {B}) + ∘-resp-≈ : ∀ {A B C} {f h : B ⇒ C} {g i : A ⇒ B} → f ≈ h → g ≈ i → f ∘ g ≈ h ∘ i + \end{minted} \end{frame} \ No newline at end of file