% Author: Florian Guthmann <florian.guthmann@fau.de>
% URL:    https://wwwcip.cs.fau.de/~oc45ujef/talks/combinators/talk.tex
\def\RCS$#1: #2 ${\expandafter\def\csname RCS#1\endcsname{\mbox{\$#1: #2 \$}}}\RequirePackage[l2tabu, orthodox]{nag}
\RCS$Id: talk.tex,v 1.9 2025/01/09 15:16:16 flo Exp $
\documentclass[12pt,ratio=43, dvipsnames]{beamer}
\usepackage[utf8]{inputenc}
\usepackage{fontspec, unicode-math}
\setmainfont{EB Garamond}

\usepackage[ngerman, english]{babel}

\usepackage{amsmath, amssymb, amsthm}
\usepackage{stmaryrd}
\usepackage{mathtools}
\usepackage{ebproof}

\usepackage{graphicx}
\graphicspath{./img/}

\usepackage[backend=biber, style=authortitle, maxnames=10]{biblatex}
\addbibresource{lit.bib}

\usetheme{default}
\beamertemplatenavigationsymbolsempty{}
\usefonttheme{serif}
\usefonttheme{structurebold}

\definecolor[named]{foreground}{HTML}{303030}
\definecolor[named]{foreground-alt}{HTML}{505050}
\colorlet{background}{white}
\definecolor[named]{background-alt}{HTML}{f0f0f0}
\definecolor[named]{primary}{HTML}{2a9d8f}
\definecolor[named]{secondary}{HTML}{e76f51}
\definecolor[named]{hl-primary}{HTML}{f4a261}
\definecolor[named]{hl-secondary}{HTML}{e9c46a}
\definecolor[named]{hl-tertiary}{HTML}{3acbba}
\colorlet{accent}{primary}

\setbeamercolor{normal text}{bg=background, fg=foreground}
\setbeamercolor{titlelike}{fg=primary}
\setbeamercolor{block title}{fg=primary}
\setbeamercolor{subtitle}{fg=foreground}
\setbeamercolor{itemize item}{fg=primary}
\setbeamercolor{emph}{fg=accent}
\renewcommand<>{\emph}[1]{{\usebeamercolor[fg]{emph}\only#2{\itshape}#1}}

\setbeamertemplate{footline}{%
  \raisebox{5pt}{\makebox[\paperwidth]{
      {\color{gray} \insertsection}\hfill
      \makebox[20pt]{\color{gray}
        \scriptsize\insertframenumber}}}\hspace*{5pt}}

\setbeamertemplate{itemize items}[circle]
\setbeamertemplate{caption}{\raggedright\insertcaption\par}

\newcommand{\hl}[2]{\tikz[scale=.8, baseline=(hl.base)]
  \node[fill=#1, rounded corners, rectangle] (hl) {#2};}
\newcommand<>\hlbox[2]{\alt#3{\hl{#1}{\(\displaystyle #2\)}}{#2}}
\newcommand{\undefined}{\hlbox{hl-secondary}{?}}
\newsavebox{\hslogobox}
\sbox{\hslogobox}{%
  \includegraphics[height=.5em]{img/haskell-logo.pdf}%
}
\newcommand{\hsbox}[1]{
  \begin{tikzpicture}[baseline=(hl.base)]
    \node[fill=background-alt, rounded corners, rectangle, inner sep=.5em] (T) {#1};
    \node[draw= background-alt, fill=white, circle, inner sep=.1em,] at (T.north east) {\usebox{\hslogobox}};
  \end{tikzpicture}
}

\usepackage{tikz}
\usetikzlibrary{babel, cd, shapes.geometric, shapes.callouts, decorations.markings, positioning}

\tikzset{
  input/.style = {
    semicircle,
    fill=foreground,
    inner sep=.5ex,
    shape border rotate=90,
    anchor=east
  },
  output/.style = {
    semicircle,
    fill=foreground,
    inner sep=.5ex,
    shape border rotate=270,
    anchor=west
  },
  dlabel/.style = {
    draw,
    circle,
    fill=white,
    inner sep=2pt
  }
}

\usepackage[framemethod=TikZ]{mdframed}
\mdfsetup{roundcorner=5pt, backgroundcolor=background-alt, innertopmargin=10pt}

\newcommand{\of}[2]{#1\colon{}#2}
\newcommand*{\CL}{\mathrm{CL}}
\newcommand*{\Sk}{\mathrm{S}}
\newcommand*{\Kk}{\mathrm{K}}
\newcommand*{\Ik}{\mathrm{I}}
\newcommand*{\Mk}{\mathrm{M}}
\newcommand*{\Bk}{\mathrm{B}}
\newcommand*{\Ck}{\mathrm{C}}
\newcommand*{\Wk}{\mathrm{W}}
\DeclareMathOperator{\pure}{pure}
\DeclareMathOperator{\id}{id}
\newcommand*{\app}[2]{#1\,#2}
\newcommand*{\lbds}[2]{\lambda^\star #1\ldotp #2}
\newcommand*{\lbd}[2]{\lambda #1\ldotp #2}
\newcommand*{\otherwise}{\text{otherwise}}
\newcommand*{\ap}{\mathrel{\varoast}}

\newcommand*{\step}{\rightarrow}
\newcommand*{\mstep}{\twoheadrightarrow}
\newcommand*{\subst}[3]{#1~\left[{#2}/{#3}\right]}
\newcommand*{\gvert}{\ \big\vert\ }

\newcommand*{\MPrule}{\hlbox{hl-tertiary}{\mathrm{MP}}}
\newcommand*{\Srule}{\hlbox{hl-primary}{\mathrm{S}}}
\newcommand*{\Krule}{\hlbox{hl-secondary}{\mathrm{K}}}

\newcommand*{\weq}{=_{\textrm{w}}}

\renewcommand{\implies}{\Rightarrow}

\title{Proofs as Combinators}
\subtitle{A Simple Desultory Philippic}
\author{Florian Guthmann}
\date{2025-01-09}

\titlegraphic{\begin{tikzpicture}[remember picture, overlay]
    \node[anchor= south east] at (current page.south east)
    {
      \includegraphics[width=0.25\textwidth]{img/mockingbird}
    };
  \end{tikzpicture}
}

\begin{document}
{
  \setbeamertemplate{footline}{\color{gray}\quad\RCSId}
  \frame{\titlepage}
}

\begin{frame}
  \centering
  \begin{tikzpicture}[>={Stealth[round,sep]}]
    \node[draw, rounded corners, fill=background-alt, minimum width=10em, minimum height=4em] at (0,0) (H) {Hilbert-Style Proofs};
    \node[draw, rounded corners, fill=background-alt, minimum width=10em, minimum height=4em, align=center] at (-3, -3) (C) {Equational\\ Combinators};
    \node[draw, rounded corners, fill=background-alt, minimum width=10em, minimum height=4em] at (3, -3) (S) {\(\mathrm{SKI}\)-Calculus};
    \draw[<->, very thick, rounded corners] (H) -| (S);
    \draw[<->, very thick, rounded corners] (H) -| (C);
    \draw[<->, very thick] (C) to (S);
  \end{tikzpicture}
\end{frame}

\part{Hilbert-Style Proofs}
\frame{\partpage}
\begin{frame}
  \frametitle{Axiom Schemas or Inference Rules?}
  \begin{tikzpicture}[remember picture, overlay]
    \draw[very thick, draw=lightgray] ([yshift=-5em]current page.north) to ([yshift=2em]current page.south);
    \node[anchor=east, draw, inner sep=1em, rounded corners, fill=background-alt] at ([xshift=-5em]current page.center) {Axiom Schemas};
    \node[anchor=west, draw, inner sep=1em, rounded corners, fill=background-alt] at ([xshift=5em]current page.center) {Inference Rules};
  \end{tikzpicture}
\end{frame}
\begin{frame}
  \frametitle{The Implicational Fragment}
  \begin{minipage}{\textwidth}
    \centering
    \begin{prooftree}
      \hypo{\Gamma \vdash \varphi \implies \psi}
      \hypo{\Gamma \vdash \varphi}
      \infer2[\MPrule]{\Gamma \vdash \psi}
    \end{prooftree}
  \end{minipage}
  \vspace{1em}

  \begin{mdframed}
    \begin{minipage}{\textwidth}
      \centering
      \begin{prooftree}
        \infer0[\Srule]{\Gamma \vdash (\varphi \implies \psi \implies \vartheta) \implies (\varphi \implies \psi) \implies \varphi \implies \vartheta}
      \end{prooftree}
    \end{minipage}
    \vspace{2em}

    \begin{minipage}{\textwidth}
      \centering
      \begin{prooftree}
        \infer0[\Krule]{\Gamma \vdash \varphi \implies \psi \implies \varphi}
      \end{prooftree}
    \end{minipage}
  \end{mdframed}
\end{frame}

\begin{frame}
  \frametitle{Identity}
  \begin{center}
    \begin{prooftree}[separation=.75em]
      \fontsize{10pt}{10pt}
      \infer0[\Srule]{\mathsf{Q} \implies \mathsf{P} \implies \varphi \implies \varphi}
      \infer0[\Krule]{\varphi \implies (\psi \implies \varphi) \implies \varphi}
      \infer2[\MPrule]{\mathsf{P} \implies \varphi \implies \varphi}
      \infer0[\Krule]{\varphi \implies \psi \implies \varphi}
      \infer2[\MPrule]{\varphi \implies \varphi}
    \end{prooftree}
  \end{center}
  \begin{align*}
    \mathsf{Q} &\coloneq \varphi \implies (\psi \implies \varphi) \implies \varphi\\
    \mathsf{P} &\coloneq \varphi \implies \psi \implies \varphi
  \end{align*}
\end{frame}

\begin{frame}
  \frametitle{tbd}
  \begin{theorem}[Deduction]
    \[
      \Gamma, \varphi \vdash \psi \iff \Gamma \vdash \varphi \implies \psi
    \]
  \end{theorem}
\end{frame}

\begin{frame}
  \frametitle{Adding more Axioms}
  \begin{mdframed}
    \begin{minipage}{\textwidth}
      \centering
      \begin{prooftree}
        \infer0{\Gamma \vdash \bot \implies \varphi}
      \end{prooftree}
    \end{minipage}
    \vspace{2em}

    \begin{minipage}{.45\textwidth}
      \centering
      \begin{prooftree}
        \infer0{\Gamma \vdash \varphi \implies \varphi \lor \psi}
      \end{prooftree}
    \end{minipage}
    \begin{minipage}{.45\textwidth}
      \centering
      \begin{prooftree}
        \infer0{\Gamma \vdash \psi \implies \varphi \lor \psi}
      \end{prooftree}
    \end{minipage}
    \vspace{2em}

    \begin{minipage}{\textwidth}
      \centering
      \begin{prooftree}
        \infer0{\Gamma \vdash (\varphi \implies \vartheta) \implies (\psi \implies \vartheta) \implies \varphi \lor \psi \implies \vartheta}
      \end{prooftree}
    \end{minipage}
    \vspace{2em}

    \begin{minipage}{.45\textwidth}
      \centering
      \begin{prooftree}
        \infer0{\Gamma \vdash \varphi \land \psi \implies \varphi}
      \end{prooftree}
    \end{minipage}
    \begin{minipage}{.45\textwidth}
      \centering
      \begin{prooftree}
        \infer0{\Gamma \vdash \varphi \land \psi \implies \psi}
      \end{prooftree}
    \end{minipage}
    \vspace{2em}

    \begin{minipage}{\textwidth}
      \centering
      \begin{prooftree}
        \infer0{\Gamma \vdash (\vartheta \implies \varphi) \implies (\vartheta \implies \psi) \implies \vartheta \implies \varphi \land \psi}
      \end{prooftree}
    \end{minipage}
  \end{mdframed}
\end{frame}

\part{To Mock a Mockingbird}
\frame{\partpage}

\begin{frame}
  \frametitle{Forests}
  \centering
  \begin{tikzpicture}
    \node (Img) at (2,0) {\includegraphics[width=0.3\textwidth]{img/mockingbird}};
    \node[circle, fill=white, inner sep=.2em] at ([shift={(1em,-1em)}]Img) {\(A\)};
    \node[cloud callout, callout relative pointer= {(-1em,-1em)}, draw, inner sep=.2em, aspect=2] at (-1,0) {\(B\)};
    \node[cloud callout, draw, inner sep=.2em, aspect=2] at (.3,2) {\(\app{A}{B}\)};
  \end{tikzpicture}
\end{frame}

\section{Some Birds}
\begin{frame}
  \frametitle{Kestrel}
  \begin{tikzpicture}[remember picture, overlay]
    \node[anchor= north east] at (current page.north east)
    {
      \reflectbox{\includegraphics[width=0.25\textwidth]{img/kestrel}}
    };
  \end{tikzpicture}

  \centering
  \[
    \app{\app{\Kk}{x}}{y} = x
  \]

  \begin{tikzpicture}
    \draw[dotted, fill=background-alt, rounded corners] (0,0) rectangle (2.5,1.5);
    \node[input] (I) at (0,1) {};
    \node[output] (O) at (2.5,1) {};
    \draw[dotted, rounded corners] (.5,.2) rectangle (2,1.3);
    \node[input] at (.5,.5) {};
    \node[output] (OO) at (2,.5) {};
    \draw[very thick, in=180, out=0] (I) to (OO);
    \draw[very thick, in=0, out=180] (O) to (OO);
    \node[dlabel] at (1.25,1.5) {\(\Kk\)};
  \end{tikzpicture}
  \vspace{1em}

  \hsbox{\texttt{const}}
\end{frame}

\begin{frame}
  \frametitle{Starling}
  \begin{tikzpicture}[remember picture, overlay]
    \node[anchor=north east] at (current page.north east)
    {
      \reflectbox{\includegraphics[width=0.25\textwidth]{img/starling}}
    };
  \end{tikzpicture}

  \centering
  \[
    \app{\app{\app{\Sk}{x}}{y}}{z} = \app{\app{x}{z}}{(\app{y}{z})}
  \]
  \begin{tikzpicture}
    \draw[dotted, fill=background-alt, rounded corners] (0,0) rectangle (4,2.6);
    \node[input] (I) at (0,2) {};
    \node[output] (O) at (4,2) {};
    \draw[dotted, rounded corners] (.5,.2) rectangle (3.5,2.4);
    \node[input] (II) at (.5,1.2) {};
    \node[output] (OO) at (3.5,1.2) {};
    \draw[dotted, rounded corners] (1,.4) rectangle (3,2.2);
    \node[input] (III) at (1,.8) {};
    \node[output] (OOO) at (3,.8) {};

    \node[circle, fill=secondary] (M) at (2,1.6) {};
    \node[circle, fill=secondary] (MM) at (2,.8) {};
    \node[circle, fill=secondary] (MMM) at (2.6,.8) {};

    \draw[very thick, in=0, out=180] (O) to (OO);
    \draw[very thick, in=0, out=180] (OO) to (OOO);

    \draw[very thick] (MMM) to (OOO);
    \draw[very thick] (MM) to (MMM);
    \draw[very thick] (III) to (MM);
    \draw[very thick, rounded corners] (II) -| (MM);
    \draw[very thick, in=180, out=0] (III) to (M);
    \draw[very thick, rounded corners] (I) -| (M);
    \draw[very thick, rounded corners] (M) -| (MMM);
    \node[dlabel] at (2,2.6) {\(\Sk\)};
  \end{tikzpicture}
  \vspace{1em}

  \hsbox{\texttt{\textbackslash{}x y z -> x z (y z)}\footnote{More on this later}}
\end{frame}

\begin{frame}
  \frametitle{Identity Bird}
  \centering
  \[
    \app{\Ik}{x} = x
  \]

  \begin{tikzpicture}
    \draw[dotted] (0,0) rectangle (2,1);
    \node[input] (I) at (0,.5) {};
    \node[output] (O) at (2,.5) {};
    \draw[very thick] (I) to (O);
    \node[dlabel] at (1,1) {\(\Ik\)};
  \end{tikzpicture}
  \vspace{1em}

  \hsbox{\texttt{id}}
\end{frame}
\begin{frame}
  \frametitle{Identity Defined}
  \begin{block}{Hilbert Style}
    \centering
    \begin{prooftree}[separation=.75em]
      \fontsize{10pt}{10pt}
      \infer0[\Srule]{\mathsf{Q} \implies \mathsf{P} \implies \varphi \implies \varphi}
      \infer0[\Krule]{\varphi \implies (\psi \implies \varphi) \implies \varphi}
      \infer2[\MPrule]{\mathsf{P} \implies \varphi \implies \varphi}
      \infer0[\Krule]{\varphi \implies \psi \implies \varphi}
      \infer2[\MPrule]{\varphi \implies \varphi}
    \end{prooftree}
  \end{block}
  \vspace{1em}

  \[
    \Ik = \app{(\app{\Sk}{\Kk})}{\Kk} = \app{\app{\Sk}{\Kk}}{\Kk}
  \]
\end{frame}

\begin{frame}
  \frametitle{Mockingbird}
  \begin{tikzpicture}[remember picture, overlay]
    \node[anchor=north east] at (current page.north east)
    {
      \includegraphics[width=0.25\textwidth]{img/mockingbird}
    };
  \end{tikzpicture}

  \centering
  \[
    \app{\Mk}{x} = \app{x}{x}
  \]
  \[
    \Mk = \app{\app{\Sk}{\Ik}}{\Ik}
  \]
  \begin{tikzpicture}
    \draw[dotted, fill=background-alt, rounded corners] (0,0) rectangle (2,1.3);
    \node[input] (I) at (0,.5) {};
    \node[output] (O) at (2,.5) {};
    \node[circle, fill=secondary] (M) at (1,.5) {};
    \draw[very thick] (I) to (M);
    \draw[very thick, in=90, out=0] (I) to (M);
    \draw[very thick] (M) to (O);
    \node[dlabel] at (1,1.3) {\(\Mk\)};
  \end{tikzpicture}

\end{frame}

\begin{frame}
  \frametitle{Cardinal}
  \begin{tikzpicture}[remember picture, overlay]
    \node[anchor=north east] at (current page.north east)
    {
      \reflectbox{\includegraphics[width=0.25\textwidth]{img/cardinal}}
    };
  \end{tikzpicture}

  \centering
  \[
    \app{\app{\app{\Ck}{x}}{y}}{z} = \app{\app{x}{z}}{y}
  \]

  \begin{tikzpicture}
    \draw[dotted, fill=background-alt, rounded corners] (0,0) rectangle (4,2.6);
    \node[input] (I) at (0,2) {};
    \node[output] (O) at (4,2) {};
    \draw[dotted, rounded corners] (.5,.2) rectangle (3.5,2.4);
    \node[input] (II) at (.5,1.2) {};
    \node[output] (OO) at (3.5,1.2) {};
    \draw[dotted, rounded corners] (1,.4) rectangle (3,2.2);
    \node[input] (III) at (1,.8) {};
    \node[output] (OOO) at (3,.8) {};

    \node[circle, fill=secondary] (A) at (1.8,1.6) {};
    \draw[very thick, rounded corners] (I) -| (A);
    \draw[very thick, in=180, out=0] (III) to (A);

    \node[circle, fill=secondary] (AA) at (1.8,.8) {};
    \draw[very thick, rounded corners] (A) to (AA);
    \draw[very thick, in=180, out=0] (II) to (AA);
    \draw[very thick, in=180, out=0] (AA) to (OOO);
    \draw[very thick, in=0, out=180] (O) to (OO);
    \draw[very thick, in=0, out=180] (OO) to (OOO);
    \node[dlabel] at (2,2.6) {\(\Ck\)};
  \end{tikzpicture}
  \vspace{1em}

  \hsbox{\texttt{flip}}
\end{frame}

\begin{frame}
  \frametitle{Warbler}
  \begin{tikzpicture}[remember picture, overlay]
    \node[anchor=north east] at (current page.north east)
    {
      \includegraphics[width=0.25\textwidth]{img/warbler}
    };
  \end{tikzpicture}
  \centering
  \[
    \app{\app{\Wk}{x}}{y} = \app{\app{x}{y}}{y}
  \]
  \begin{tikzpicture}
    \draw[dotted, fill=background-alt, rounded corners] (0,0) rectangle (3,2.5);
    \node[input] (I) at (0,1.5) {};
    \node[output] (O) at (3,1.5) {};
    \draw[dotted, rounded corners] (.5,.2) rectangle (2.5,2.3);
    \node[input] (II) at (.5,.5) {};
    \node[output] (OO) at (2.5,.5) {};

    \node[circle, fill=secondary] (A) at (1.2,1.1) {};
    \node[circle, fill=secondary] (AA) at (2,.5) {};

    \draw[very thick] (II) to (AA);
    \draw[very thick, rounded corners] (A) -| (AA);
    \draw[very thick, rounded corners] (I) -| (A);
    \draw[very thick, in=180, out=0] (II) to (A);
    \draw[very thick] (AA) to (OO);

    \draw[very thick, in=0, out=180] (O) to (OO);
    \node[dlabel] at (1.5,2.5) {\(\Wk\)};
  \end{tikzpicture}
  \vspace{1em}

  \hsbox{\texttt{\textbackslash{}x y -> x y y}\footnote{Again, more on this later}}
\end{frame}

\begin{frame}
  \frametitle{Bluebird}
  \begin{tikzpicture}[remember picture, overlay]
    \node[anchor=north east] at (current page.north east)
    {
      \reflectbox{\includegraphics[width=0.25\textwidth]{img/bluebird}}
    };
  \end{tikzpicture}
  \centering
  \[
    \app{\app{\app{\Bk}{x}}{y}}{z} = \app{x}{(\app{y}{z})}
  \]

  \begin{tikzpicture}
    \draw[dotted, fill=background-alt, rounded corners] (0,0) rectangle (4,2.6);
    \node[input] (I) at (0,2) {};
    \node[output] (O) at (4,2) {};
    \draw[dotted, rounded corners] (.5,.2) rectangle (3.5,2.4);
    \node[input] (II) at (.5,1.2) {};
    \node[output] (OO) at (3.5,1.2) {};
    \draw[dotted, rounded corners] (1,.4) rectangle (3,2.2);
    \node[input] (III) at (1,.8) {};
    \node[output] (OOO) at (3,.8) {};

    \node[circle, fill=secondary] (A) at (1.6,.8) {};
    \node[circle, fill=secondary] (AA) at (2.4,.8) {};

    \draw[very thick, rounded corners] (I) -| (AA);
    \draw[very thick, rounded corners] (II) -| (A);
    \draw[very thick] (III) to (A);
    \draw[very thick] (A) to (AA);


    \draw[very thick, in=180, out=0] (AA) to (OOO);
    \draw[very thick, in=0, out=180] (O) to (OO);
    \draw[very thick, in=0, out=180] (OO) to (OOO);
    \node[dlabel] at (2,2.6) {\(\Bk\)};
  \end{tikzpicture}
  \vspace{1em}

  \hsbox{\texttt{(.)}}
\end{frame}

\begin{frame}
  \frametitle{Blackbird}
  \begin{tikzpicture}[remember picture, overlay]
    \node[rotate= 5] at ([shift={(10em, -5em)}]current page)
    {
      \sffamily{}\color{lightgray}\bfseries{}The Beatles
    };
  \end{tikzpicture}
  \centering
  \[
    \app{\app{\app{\app{\Bk_{1}}{x}}{y}}{z}}{m} = \app{x}{(\app{\app{y}{z}}{m})}
  \]
  \[
    \Bk_{1} = \app{\app{\Bk}{\Bk}}{\Bk}
  \]
  \begin{tikzpicture}
    \draw[dotted, fill=background-alt, rounded corners] (0,0) rectangle (4,2.6);
    \node[input] (I) at (0,2) {};
    \node[output] (O) at (4,2) {};
    \draw[dotted, rounded corners] (.3,.2) rectangle (3.7,2.4);
    \node[input] (II) at (.3,1.6) {};
    \node[output] (OO) at (3.7,1.2) {};
    \draw[dotted, rounded corners] (.6,.4) rectangle (3.4,2.2);
    \node[input] (III) at (.6,1.2) {};
    \node[output] (OOO) at (3.4,.8) {};
    \draw[dotted, rounded corners] (1,.4) rectangle (3,2.2);
    \node[input] (IIII) at (1,.8) {};
    \node[output] (OOOO) at (3,.8) {};

    \node[circle, fill=secondary] (A) at (1.4,1.2) {};
    \node[circle, fill=secondary] (AA) at (2.6,.8) {};
    \node[circle, fill=secondary] (AAA) at (2,.8) {};

    \draw[very thick, rounded corners] (I) -| (AA);
    \draw[very thick, rounded corners] (II) -| (A);
    \draw[very thick] (III) to (A);
    \draw[very thick, rounded corners] (A) -| (AAA);
    \draw[very thick] (IIII) to (AAA);
    \draw[very thick] (AAA) to (AA);


    \draw[very thick, in=180, out=0] (AA) to (OOO);
    \draw[very thick, in=0, out=180] (O) to (OO);
    \draw[very thick, in=0, out=180] (OO) to (OOO);
    \node[dlabel] at (2,2.6) {\(\Bk_{1}\)};
  \end{tikzpicture}
  \vspace{1em}

\end{frame}

\section{Some Forests}
\begin{frame}
  \frametitle{The \(\mathrm{BCKW}\)-Forest}
  \begin{block}{}
    The forest containing a \emph{Bluebird}, \emph{Cardinal}, \emph{Kestrel} and \emph{Warbler}.
  \end{block}
  \begin{block}{}
    Each bird represents a unique capability:
    \vspace{1em}

    \begin{tabular}{c|c}
      \(\Bk\) & parenthesising\\
      \hline
      \(\Ck\) & reordering\\
      \hline
      \(\Kk\) & discarding\\
      \hline
      \(\Wk\) & duplication
    \end{tabular}
    \quad
    {\Large\(\rightsquigarrow\)} interesting subforests!
  \end{block}

  \begin{onlyenv}<2->
    \begin{align*}
      \mathrm{BCK} &\leftrightsquigarrow \text{a fragment of affine logic}\\
      \mathrm{BC} &\leftrightsquigarrow \text{a fragment of linear logic}
    \end{align*}
  \end{onlyenv}
\end{frame}

\begin{frame}
  \frametitle{The \(\mathrm{SK}\)-Forest}
  \begin{block}{}
    The forest containing a \emph{Starling} and \emph{Kestrel}.
  \end{block}
  \begin{block}{}
    \(\Sk\) represents multiple capabilities at once:
    \vspace{1em}

    \begin{tabular}{c|c}
      \(\Sk\) & parenthesising, reordering, duplication\\
      \hline
      \(\Kk\) & discarding
    \end{tabular}
  \end{block}
\end{frame}

\begin{frame}
  \frametitle{Comparison}
  \centering
  \Large
  \begin{tabular}{c|c|c}
    &\(\mathrm{SK}\)&\(\mathrm{BCKW}\)\\
    \hline
    \(\Sk\) & \(\Sk\) & \(\app{\app{\Bk}{(\app{\Bk}{\Wk})}}{(\app{\app{\Bk}{\Bk}}{\Ck})}\) \\
    \(\Bk\) & \(\app{\app{\Sk}{(\app{\Kk}{\Sk})}}{\Kk}\) & \(\Bk\) \\
    \(\Ck\) & \(\app{\app{\Sk}{(\app{\app{\Bk}{\Bk}}{\Sk})}}{(\app{\Kk}{\Kk})}\) & \(\Ck\)\\
    \(\Kk\) & \(\Kk\) & \(\Kk\) \\
    \(\Wk\) & \(\app{\app{\Sk}{\Sk}}{(\app{\Kk}{\Ik})}\) & \(\Wk\)\\
  \end{tabular}
\end{frame}

\part{Combinatory Logic}
\frame{\partpage}

\begin{frame}
  \frametitle{Syntax}
  \[
    F, G :\coloneqq v \gvert \Kk \gvert \Sk \gvert \app{F}{G}
  \]
  where \(v \in \mathcal{V}\)

\end{frame}

\begin{frame}
  \frametitle{Small-Step Operational Semantics}

  \begin{minipage}{\textwidth}
    \centering
    \begin{prooftree}
      \infer0[\Krule]{\app{\app{\Kk}{F}}{G} \step F}
    \end{prooftree}
  \end{minipage}
  \vspace{1em}

  \begin{minipage}{\textwidth}
    \centering
    \begin{prooftree}
      \infer0[\Srule]{\app{\app{\app{\Sk}{F}}{G}}{H} \step \app{\app{F}{H}}{(\app{G}{H})}}
    \end{prooftree}
  \end{minipage}
  \vspace{1em}

  \begin{minipage}{.45\textwidth}
    \centering
    \begin{prooftree}
      \hypo{F \step F'}
      \infer1[app\textsubscript{l}]{\app{F}{G} \step \app{F'}{G}}
    \end{prooftree}
  \end{minipage}
  \begin{minipage}{.45\textwidth}
    \centering
    \begin{prooftree}
      \hypo{G \step G'}
      \infer1[app\textsubscript{r}]{\app{F}{G} \step \app{F}{G'}}
    \end{prooftree}
  \end{minipage}
\end{frame}

\begin{frame}
  \frametitle{Weak equality}
  Let \(\weq\) be the least equivalence relation containing \(\step\):
  \vspace{2em}

  \begin{minipage}{.45\textwidth}
    \centering
    \begin{prooftree}
      \infer0{F \weq F}
    \end{prooftree}
  \end{minipage}
  \begin{minipage}{.45\textwidth}
    \centering
    \begin{prooftree}
      \hypo{G \weq F}
      \infer1{F \weq G}
    \end{prooftree}
  \end{minipage}
  \vspace{1em}

  \begin{minipage}{.45\textwidth}
    \centering
    \begin{prooftree}
      \hypo{F \step G}
      \infer1{F \weq G}
    \end{prooftree}
  \end{minipage}
  \begin{minipage}{.45\textwidth}
    \centering
    \begin{prooftree}
      \hypo{G \step F}
      \infer1{F \weq G}
    \end{prooftree}
  \end{minipage}
\end{frame}

\begin{frame}
  \frametitle{Multi Step Relation}
  Let \(\mstep\) be the reflexive transitive closure of \(\step\):
  \vspace{2em}

  \begin{minipage}{.45\textwidth}
    \centering
    \begin{prooftree}
      \infer0{F \mstep F}
    \end{prooftree}
  \end{minipage}
  \begin{minipage}{.45\textwidth}
    \centering
    \begin{prooftree}
      \hypo{F \step G}
      \hypo{G \mstep H}
      \infer2{F \mstep H}
    \end{prooftree}
  \end{minipage}
\end{frame}

\begin{frame}
  \frametitle{Church-Rosser}
  \centering
  \Large
  \begin{tikzpicture}
    \node at (0,0) (F) {\(F\)};
    \node at (-2, -2) (F1) {\(F_{1}\)};
    \node at (2, -2) (F2) {\(F_{2}\)};
    \node at (0, -4) (G) {\(G\)};
    \draw[->>] (F) to (F1);
    \draw[->>] (F) to (F2);
    \draw[->>, dashed] (F1) to (G);
    \draw[->>, dashed] (F2) to (G);
  \end{tikzpicture}
\end{frame}

\section{Combinators and \texorpdfstring{\(\lambda\)}{Lambda}-terms}
\begin{frame}
  \frametitle{Combinators as \(\lambda\)-terms}
  \Large
  \begin{align*}
    &(-)_{\Lambda} \colon \CL \to \Lambda\\
    &(v)_{\Lambda} = v\\
    & (\Kk)_{\Lambda} = \lbd{x}{\lbd{y}{x}}\\
    & (\Sk)_{\Lambda} = \lbd{x}{\lbd{y}{\lbd{z}{\app{\app{x}{z}}{(\app{y}{z})}}}}\\
    & (\app{F}{G})_{\Lambda} = \app{(F)_{\Lambda}}{(G)_{\Lambda}}
  \end{align*}
\end{frame}

\begin{frame}
  \frametitle{\(\lambda\)-terms as Combinators?}
  \Large
  \begin{align*}
    &(-)_{\CL} \colon \Lambda \to \CL\\
    &(v)_{\CL} = v\\
    & (\app{s}{t})_{\CL} = \app{(s)_{\CL}}{(t)_{\CL}}\\
    & (\lbd{v}{t})_{\CL} = \undefined
  \end{align*}
\end{frame}

\begin{frame}
  \frametitle{Combinatory Abstraction}
  \Large
  \begin{align*}
    &\lbds{(-)}{(-)} \colon \mathcal{V} \times \CL \to \CL\\
    &\lbds{v}{x} =
      \begin{cases}
        \Ik & v = x\\
        \app{\Kk}{x} & \otherwise
      \end{cases}\\
    &\lbds{v}{\Kk} = \app{\Kk}{\Kk}\\
    &\lbds{v}{\Sk} = \app{\Kk}{\Sk}\\
    &\lbds{v}{(\app{B}{C})} = \app{\Sk}{\app{(\lbds{v}{B})}{(\lbds{v}{C})}}
  \end{align*}
\end{frame}

\begin{frame}
  \frametitle{\(\lambda^{\star}\) is \(\beta\)-reductive}
  \begin{theorem}
    \[
      (\app{\lbds{x}{A}}{B}) \mstep \left(\subst{A}{B}{x}\right)
    \]
  \end{theorem}

\end{frame}

\section{Typed Combinators}
\begin{frame}
  \frametitle{Typing Relation (à la Curry)}
  \begin{minipage}{\textwidth}
    \centering
    \begin{prooftree}
      \infer0[\Krule]{\Gamma \vdash \Kk \colon \sigma \to \tau \to \sigma}
    \end{prooftree}
  \end{minipage}
  \vspace{1em}

  \begin{minipage}{\textwidth}
    \centering
    \begin{prooftree}
      \infer0[\Srule]{\Gamma \vdash \Sk \colon (\sigma \to \tau \to \varrho) \to (\sigma \to \tau) \to \sigma \to \varrho}
    \end{prooftree}
  \end{minipage}
  \vspace{1em}

  \begin{minipage}{\textwidth}
    \centering
    \begin{prooftree}
      \hypo{\Gamma \vdash M \colon \sigma \to \tau}
      \hypo{\Gamma \vdash N \colon \sigma}
      \infer2[\MPrule]{\Gamma \vdash \app{M}{N} \colon \tau}
    \end{prooftree}
  \end{minipage}
\end{frame}

\begin{frame}
  \frametitle{Church-Style Typing}
  \begin{block}{Reminder}
    In the \(\lambda\)-calculus, church style typing is done by annotating
    \(\lambda\)-abstractions with the type of the bound variable.
  \end{block}
  \vspace{2em}

  Instead, index \(\Sk\) and \(\Kk\) with the choices of types:
  \[
    F, G :\coloneqq v \gvert \Kk_{\sigma,\tau} \gvert \Sk_{\sigma,\tau,\varrho} \gvert \app{F}{G}
  \]
  where \(\sigma, \tau, \varrho \in \mathrm{Type}\)

\end{frame}

\begin{frame}
  \frametitle{Curry-Howard}
  \centering
  \Large
  \begin{tabular}{c|c}
    Hilbert-Style & Typed Combinatory Logic\\
    \hline
    Modus Ponens & Application \\
    Assumption & Variable\\
    Axiom Schemes & \(\Kk\) and \(\Sk\)
  \end{tabular}
\end{frame}

\part{Golfing, for Fun and Profit}
\frame{\partpage{}}

\begin{frame}
  \frametitle{Combinators in Haskell}
  \begin{block}{}
    Remember \hsbox{\(\Sk\)\texttt{\ = \textbackslash{}x y z -> x z (y z)}}?
  \end{block}
  \begin{block}{}
    Surely we shouldn't be churning butter with a toothpick like that!
  \end{block}
  \begin{block}<2->{}
    The \texttt{Prelude} comes to our rescue!
  \end{block}
\end{frame}

\section{Some Category Theory}

\begin{frame}
  \frametitle{Applicative Functors{\footnote{with a grain of salt}\footcite{applicative}}}
  An endofunctor \(\of{F}{\mathcal{C} \to \mathcal{C}}\) is called \emph{applicative}, if there exist
  \begin{itemize}
  \item \(\of{\pure}{A \to FA}\)
  \item \(\of{\ap}{F(B^{A}) \times FA \to FB}\)
  \end{itemize}
  such that
  \begin{align*}
    \pure(\id_{A}) \ap Fa &= a\\
    \pure(\circ) \ap u \ap v \ap w &= u \ap (v \ap w)\\
    \pure(f) \ap \pure(a) &= \pure (f(a)) \\
    u \ap \pure(a) &= \pure (\lbd{f}{f(a)}) \ap u
  \end{align*}
\end{frame}

\begin{frame}[fragile]
  \frametitle{Environment Functor is Applicative}
  \begin{center}
    \begin{tikzpicture}[commutative diagrams/every diagram]
      \node (D) {\(\of{(-)^{A}}{\mathcal{C} \to \mathcal{C}}\)};
      \node [matrix of math nodes, below = 0ex of D, commutative diagrams/every cell] (M) {
        X & X^A\\
        Y & Y^A\\
      };
      \draw[commutative diagrams/.cd, every label]
      (M-1-1) edge[|->] (M-1-2)
      (M-2-1) edge[|->] (M-2-2)
      (M-1-1) edge[->] node (f) {\(f\)} (M-2-1)
      (M-1-2) edge[->] node (Ff) {\(g \mapsto f \circ g\)} (M-2-2);
    \end{tikzpicture}
  \end{center}
  \begin{overprint}
    \begin{align*}
      &\of{\pure}{X \to \alt<2->{A \to X}{X^A}}\\
      &\visible<2->{\pure = \Kk}\\
      &\of{\varoast}{\alt<3->{(A \to X\to Y)}{Y^{X^A}} \alt<3->{\to}{\times} \alt<3->{(A \to X)}{X^A} \to \alt<3->{A \to Y}{Y^A}}\\
      &\visible<3->{\varoast = \Sk}\\
    \end{align*}
  \end{overprint}
\end{frame}

\begin{frame}
  \frametitle{Combinators in Haskell}
  \hsbox{\(\Kk\)\texttt{\ = pure}}

  \hsbox{\(\Sk\)\texttt{\ = (<*>)}}

  \hsbox{\(\Bk\)\texttt{\ = pure (<*>) <*> pure}}

  \hsbox{\(\Ck\)\texttt{\ = ((.) . (<*>)) <*> pure pure}}

  \hsbox{\(\Wk\)\texttt{\ = (<*>) <*> pure id = join }}
\end{frame}

\part{Appendix}
\nocite{*}
\frame{\printbibliography{}}

\section{Applicative Functors without Salt}

\begin{frame}
  \frametitle{Monoidal Categories}
  A \emph{monoidal} category is a category \(\mathcal{C}\) with a
  bifunctor
  \(\of{\otimes}{\mathcal{C} \times \mathcal{C} \to \mathcal{C}}\) and
  an object \(1 \in \mathcal{C}\) such that there exist natural
  isomorphisms
  \begin{itemize}
  \item \(\of{\alpha_{A,B,C}}{A \otimes (B \otimes C) \cong (A \otimes B) \otimes C}\)
  \item \(\of{\rho_{A}}{A \otimes 1 \cong A}\)
  \item \(\of{\lambda_{B}}{1 \otimes B \cong B}\)
  \end{itemize}
\end{frame}

\begin{frame}[fragile]
  \frametitle{Lax Monoidal Endofunctors}
  Let \((\mathcal{C}, \otimes, 1)\) be a monoidal category\footnote{e.g. \((\mathsf{Set}, \times, \{\bullet\})\)}. A \emph{lax
    monoidal} endofunctor on \(\mathcal{C}\) is a functor
  \(\of{F}{\mathcal{C} \to \mathcal{C}}\) with
  \begin{itemize}
  \item a morphism \(1 \to F1\)
  \item a natural transformation \(\of{\mu_{X,Y}}{FX \otimes FY \to F(X \otimes Y)}\)
  \end{itemize}
  such that
  \small
  \begin{center}
    \begin{onlyenv}<1>
      \begin{tikzcd}
        (FA \otimes FB) \otimes FC \arrow[r, "\alpha_{FA, FB, FC}"{yshift=1ex}] \arrow[d, "\mu_{A,B} \otimes \id"] & FA \otimes (FB \otimes FC) \arrow[d, "\id \otimes \mu_{B,C}"]\\
        F(A \otimes B) \otimes F C \arrow[d, "\mu_{A \otimes B, C}"] & FA \otimes F(B \otimes C) \arrow[d, "\mu_{A, B \otimes C}"]\\
        F((A \otimes B) \otimes C) \arrow[r, "F(\alpha_{A,B,C})"{yshift=1ex}]& F(A \otimes (B \otimes C))
      \end{tikzcd}
    \end{onlyenv}
    \begin{onlyenv}<2>
      \begin{tikzcd}
        FA \otimes 1 \arrow[r, "\id \otimes \eta"] \arrow[d, "\rho_{A}"] & FA \otimes F1 \arrow[d, "\mu_{A, 1}"]\\
        FA & F(A \otimes 1) \arrow[l, "F(\rho_A)"]
      \end{tikzcd}
      \quad
      \begin{tikzcd}
        1 \otimes FB \arrow[r, "\eta \otimes \id"] \arrow[d, "\lambda_{B}"] & F1 \otimes FB \arrow[d, "\mu_{1, B}"]\\
        FB & F(1 \otimes B) \arrow[l, "F(\lambda_B)"]
      \end{tikzcd}
    \end{onlyenv}
  \end{center}
\end{frame}
\begin{frame}
  \frametitle{Applicative Functors}
  Let \((\mathcal{C}, \otimes, 1)\) be a monoidal category. A lax
  monoidal functor \(\of{F}{\mathcal{C} \to \mathcal{C}}\) is called
  \emph{strong} if there is a natural transformation
  \[
    \of{\tau_{A, B}}{A \otimes FB \to F(A \otimes B)}
  \]
  such that

  % TODO
\end{frame}



\end{document}

%%% Local Variables:
%%% mode: LaTeX
%%% TeX-engine: xetex
%%% TeX-master: t
%%% End: