From 40c488ab2a322790fe9e125e1d52ead43ee98af0 Mon Sep 17 00:00:00 2001 From: Leon Vatthauer Date: Fri, 19 Jan 2024 14:04:41 +0100 Subject: [PATCH] Work on slides --- slides/bibliography.bib | 56 ++++++++++++++++++ slides/main.tex | 3 +- slides/quiver.sty | 40 +++++++++++++ slides/sections/01_abstracting.tex | 91 +++++++++++++++++++++++------- 4 files changed, 168 insertions(+), 22 deletions(-) create mode 100644 slides/quiver.sty diff --git a/slides/bibliography.bib b/slides/bibliography.bib index 2a44711..825ed34 100644 --- a/slides/bibliography.bib +++ b/slides/bibliography.bib @@ -1,3 +1,45 @@ +@article{delay, + author = {Venanzio Capretta}, + title = {General Recursion via Coinductive Types}, + journal = {CoRR}, + volume = {abs/cs/0505037}, + year = {2005}, + url = {http://arxiv.org/abs/cs/0505037}, + eprinttype = {arXiv}, + eprint = {cs/0505037}, + timestamp = {Mon, 13 Aug 2018 16:46:14 +0200}, + biburl = {https://dblp.org/rec/journals/corr/abs-cs-0505037.bib}, + bibsource = {dblp computer science bibliography, https://dblp.org} +} + +@article{elgotalgebras, + author = {Jir{\'{\i}} Ad{\'{a}}mek and + Stefan Milius and + Jir{\'{\i}} Velebil}, + title = {Elgot Algebras}, + journal = {CoRR}, + volume = {abs/cs/0609040}, + year = {2006}, + url = {http://arxiv.org/abs/cs/0609040}, + eprinttype = {arXiv}, + eprint = {cs/0609040}, + timestamp = {Mon, 04 Sep 2023 12:29:24 +0200}, + biburl = {https://dblp.org/rec/journals/corr/abs-cs-0609040.bib}, + bibsource = {dblp computer science bibliography, https://dblp.org} +} + +@article{elgotmonad, + title = {Elgot theories: a new perspective on the equational properties of iteration}, + volume = {21}, + doi = {10.1017/S0960129510000496}, + number = {2}, + journal = {Mathematical Structures in Computer Science}, + publisher = {Cambridge University Press}, + author = {ADÁMEK, JIŘÍ and MILIUS, STEFAN and VELEBIL, JIŘÍ}, + year = {2011}, + pages = {417–480} +} + @article{eqlm, author = {Bucalo, Anna and F\"{u}hrmann, Carsten and Simpson, Alex}, title = {An Equational Notion of Lifting Monad}, @@ -65,4 +107,18 @@ month = {1}, pages = {223–259}, numpages = {37} +} + +@article{uniformelgot, + author = {Sergey Goncharov}, + title = {Uniform Elgot Iteration in Foundations}, + journal = {CoRR}, + volume = {abs/2102.11828}, + year = {2021}, + url = {https://arxiv.org/abs/2102.11828}, + eprinttype = {arXiv}, + eprint = {2102.11828}, + timestamp = {Fri, 26 Feb 2021 14:31:25 +0100}, + biburl = {https://dblp.org/rec/journals/corr/abs-2102-11828.bib}, + bibsource = {dblp computer science bibliography, https://dblp.org} } \ No newline at end of file diff --git a/slides/main.tex b/slides/main.tex index bffe254..3ffe3a6 100644 --- a/slides/main.tex +++ b/slides/main.tex @@ -7,7 +7,7 @@ % of the GNU Public License, version 2. % % ------------------------------------------------------------------------------ -\documentclass[final]{beamer} +\documentclass[final, handout]{beamer} % ======================================================================================== % Theme: inner, outer, font and colors @@ -159,6 +159,7 @@ Leon Vatthauer%\inst{1} \usepackage{tikz} \usepackage{tikz-cd} +\usepackage{quiver} \usetikzlibrary{shapes.callouts} \usepackage{mathpartir} diff --git a/slides/quiver.sty b/slides/quiver.sty new file mode 100644 index 0000000..34df960 --- /dev/null +++ b/slides/quiver.sty @@ -0,0 +1,40 @@ +% *** quiver *** +% A package for drawing commutative diagrams exported from https://q.uiver.app. +% +% This package is currently a wrapper around the `tikz-cd` package, importing necessary TikZ +% libraries, and defining a new TikZ style for curves of a fixed height. +% +% Version: 1.4.2 +% Authors: +% - varkor (https://github.com/varkor) +% - AndréC (https://tex.stackexchange.com/users/138900/andr%C3%A9c) + +\NeedsTeXFormat{LaTeX2e} +\ProvidesPackage{quiver}[2021/01/11 quiver] + +% `tikz-cd` is necessary to draw commutative diagrams. +\RequirePackage{tikz-cd} +% `amssymb` is necessary for `\lrcorner` and `\ulcorner`. +\RequirePackage{amssymb} +% `calc` is necessary to draw curved arrows. +\usetikzlibrary{calc} +% `pathmorphing` is necessary to draw squiggly arrows. +\usetikzlibrary{decorations.pathmorphing} + +% A TikZ style for curved arrows of a fixed height, due to AndréC. +\tikzset{curve/.style={settings={#1},to path={(\tikztostart) + .. controls ($(\tikztostart)!\pv{pos}!(\tikztotarget)!\pv{height}!270:(\tikztotarget)$) + and ($(\tikztostart)!1-\pv{pos}!(\tikztotarget)!\pv{height}!270:(\tikztotarget)$) + .. (\tikztotarget)\tikztonodes}}, + settings/.code={\tikzset{quiver/.cd,#1} + \def\pv##1{\pgfkeysvalueof{/tikz/quiver/##1}}}, + quiver/.cd,pos/.initial=0.35,height/.initial=0} + +% TikZ arrowhead/tail styles. +\tikzset{tail reversed/.code={\pgfsetarrowsstart{tikzcd to}}} +\tikzset{2tail/.code={\pgfsetarrowsstart{Implies[reversed]}}} +\tikzset{2tail reversed/.code={\pgfsetarrowsstart{Implies}}} +% TikZ arrow styles. +\tikzset{no body/.style={/tikz/dash pattern=on 0 off 1mm}} + +\endinput diff --git a/slides/sections/01_abstracting.tex b/slides/sections/01_abstracting.tex index c798a64..01e5903 100644 --- a/slides/sections/01_abstracting.tex +++ b/slides/sections/01_abstracting.tex @@ -12,27 +12,48 @@ Goal: interpret an effectul programming language in a category $\mathcal{C}$ 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: - \begin{multicols}{2} - \begin{minted}{haskell} - do x <- p - y <- q - return (x, y) - \end{minted} + \item<5-> Commutativity (also entails strength) + % , i.e. the following programs should yield equal results: + % \begin{multicols}{2} + % \begin{minted}{haskell} + % do x <- p + % y <- q + % return (x, y) + % \end{minted} - \begin{minted}{haskell} - do y <- q - x <- p - return (x, y) - \end{minted} - \end{multicols} - where p and q are programs. + % \begin{minted}{haskell} + % do y <- q + % x <- p + % return (x, y) + % \end{minted} + % \end{multicols} + % where p and q are programs. \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} +\begin{frame}[t, fragile]{Capturing Partiality Categorically}{Preliminaries} + We work in category $\mathcal{C}$ that + \begin{itemize} + \item has finite products + \item has finite coproducts + \item is distributive, i.e. the following is an iso: + % https://q.uiver.app/#q=WzAsMixbMCwwLCIoWCBcXHRpbWVzIFkpICsgKFggXFx0aW1lcyBaKSJdLFs0LDAsIlggXFx0aW1lcyAoWSArIFopIl0sWzAsMSwiZHN0bF57LTF9ICA6PSBbIFxcbGFuZ2xlIGlkICwgaW5sIFxccmFuZ2xlICwgXFxsYW5nbGUgaWQgLCBpbnIgXFxyYW5nbGVdIl1d + \[\begin{tikzcd} + {(X \times Y) + (X \times Z)} &&&& {X \times (Y + Z)} + \arrow["{dstl^{-1} := [ \langle id , inl \rangle , \langle id , inr \rangle]}", from=1-1, to=1-5] + \end{tikzcd}\] + % https://q.uiver.app/#q=WzAsMixbMCwwLCJYIFxcdGltZXMgKFkgKyBaKSJdLFs0LDAsIihYIFxcdGltZXMgWSkgKyAoWCBcXHRpbWVzIFopIl0sWzAsMSwiZHN0bCJdXQ== + \[\begin{tikzcd} + {X \times (Y + Z)} &&&& {(X \times Y) + (X \times Z)} + \arrow["dstl", from=1-1, to=1-5] + \end{tikzcd}\] + \end{itemize} + +\end{frame} + \newcommand{\tdom}{\text{dom}\;} \begin{frame}[t, fragile]{Capturing Partiality Categorically}{Restriction Categories~\cite{restriction}} @@ -48,7 +69,7 @@ What properties should a monad $T$ for modelling partiality have? \end{definition} \onslide<2-> -Intuitively $\tdom f$ captures the domain of definiteness of $f$. +Intuitively $\tdom f$ captures the domain of definedness of $f$. \begin{block}{Remark}<3-> Every category has a trivial restriction structure $\tdom f = id$, we call categories with a non-trivial restriction structure \textit{restriction categories}. @@ -80,7 +101,7 @@ Intuitively $\tdom f$ captures the domain of definiteness of $f$. % 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{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: @@ -102,7 +123,7 @@ Intuitively $\tdom f$ captures the domain of definiteness of $f$. \end{itemize} \end{frame} -\begin{frame}[t, fragile]{The Delay Monad} +\begin{frame}[t, fragile]{Capturing Partiality Categorically}{Capretta's Delay Monad~\cite{delay}} \begin{itemize}[<+->] \item Recall the delay codatatype: @@ -140,7 +161,7 @@ Intuitively $\tdom f$ captures the domain of definiteness of $f$. % \end{frame} %%%%%%% -\begin{frame}[t, fragile]{Partiality from Iteration}{Elgot Algebras} +\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{definition} A (unguarded) Elgot Algebra consists of: @@ -162,14 +183,38 @@ The following is an adaptation of Ad\'amek, Milius and Velebil's \textit{complet \end{block} \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}: + \end{itemize} +\end{definition} +\begin{block}{Remark} +Strong Elgot Monads are regarded as minimal semantic structures for interpreting effectful while-languages. +\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 +\begin{frame}[t, fragile]{Partiality from Iteration}{pre-Elgot Monads~\cite{uniformelgot}} + Relaxing the requirements for Elgot monads we get the following weaker concept: + \begin{definition} + 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{theorem} + Every Elgot monad is pre-Elgot + \end{theorem} \end{frame} -\begin{frame}[t, fragile]{Partiality from iteration}{The K Monad} +\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 $K$ is strong and commutative @@ -178,6 +223,10 @@ The following is an adaptation of Ad\'amek, Milius and Velebil's \textit{complet \end{itemize} \end{frame} +\begin{frame}[t, fragile]{Partiality from iteration}{Closing the gap} + ... +\end{frame} + %% TODOs: % cite stefan