\documentclass[serif]{beamer}
\usepackage{amsmath}
\usepackage{amsfonts}
\usepackage{amssymb}
\usepackage{graphicx}
\usepackage{stmaryrd}
\usepackage{csquotes}
\usepackage{listings}
\usepackage{unicode-math}
\usepackage{polyglossia}

\setmainlanguage{french}

\usetheme{Boadilla}

\setmainfont[Mapping=tex-text,
BoldFont=texgyrepagella-bold.otf,
ItalicFont=texgyrepagella-italic.otf]{texgyrepagella-regular.otf}
\setmathfont{Asana-Math.otf}
\usefonttheme{serif}

\usepackage{tikz}
\usetikzlibrary{shapes,arrows}
\usepackage{tikz-cd}

% Arbres de preuves de séquents
\usepackage{bussproofs}

\newtheorem{théorème}[theorem]{Théorème}
\theoremstyle{definition}
\newtheorem{définition}[theorem]{Définition}
\newcommand{\parr}{\mathbin{⅋}}
\newcommand{\impl}{\Rightarrow}
\newcommand{\denot}[1]{\left\llbracket #1 \right\rrbracket}

\AtBeginSection{\frame{\sectionpage}}


\title[Control categories and duality]{
Présentation d'article :\\
\textit{Control categories and duality}\\
Peter Selinger}
\author[$\lambda \mu$]{Nguyễn Lê Thành Dũng (M1 MPRI, ENS Ulm)}
\date{14 février 2014}

\begin{document}

\begin{frame}
  \titlepage
\end{frame}


\begin{frame}{Aperçu}
  \begin{itemize}
  \item Étendre la correspondance de Curry-Howard à la logique classique
  \item Calcul de termes de preuves classiques : le $\lambda \mu$-calcul de Parigot
    \begin{itemize}
    \item Opérateurs de contrôle / continuations
    \end{itemize}
  \item Interprétations calculatoires
    \begin{itemize}
    \item Appel par nom / par valeur
    \end{itemize}
  \item Résultat : la dualité de De Morgan échange CBN et CBV !
  % pour obtenir ça, détour par les catégories où on obtient une
  % dualité syntax-free
  \item Dualité révélée par une sémantique catégorique 
  \item Interprétation catégorique la logique classique
    \begin{itemize}
    \item Non dégénérée !
    \end{itemize}
  \end{itemize}
\end{frame}

\begin{frame}{Plan}
  \tableofcontents
\end{frame}

\section{Le \texorpdfstring{$\lambda \mu$}{lambda-mu}-calcul}

\begin{frame}{Séquents à plusieurs conclusions}
  \begin{itemize}
  \item Plusieurs formules à droite $\rightarrow$ logique classique
  \item $A_1, \ldots, A_n \vdash B_1, \ldots, B_n$ signifie \\
    \enquote{
      $A_1$ \emph{et} \ldots \emph{et} $A_n$ entraîne 
      $B_1$ \emph{ou} \ldots \emph{ou} $B_n$
    }
  \item Tiers exclu en calcul des séquents LK :
  \end{itemize}
  \begin{prooftree}
    \def\fCenter{\ \vdash\ }
    \Axiom$A \fCenter A$
    \UnaryInf$\fCenter \lnot A, A$
    \UnaryInf$\fCenter \lnot A \lor A$
  \end{prooftree}
  \begin{itemize}
  \item Typage du $\lambda \mu$-calcul : déduction naturelle classique
  \end{itemize}
\end{frame}


\begin{frame}{Le $\lambda \mu$-calcul (Parigot, 1992)}
  \begin{itemize}
  \item Termes :
    \begin{itemize}
    \item $x, y, \ldots$ : variables de termes
    \item $\alpha, \beta, \ldots$ : variables de contrôle
      % note : omission des constantes
    \item $M, N, \ldots ::= x \mid * \mid M\ N \mid \lambda x . M \mid [\alpha]M \mid \mu \alpha . M$
    \end{itemize}
  \item Types du $\lambda$-calcul simplement typé avec $\bot$ et $\top$ : $A, B, \ldots$
  \item Jugements de typage : $\Gamma \vdash M : A \mid \Delta$
    \begin{itemize}
    \item $\Gamma = x_1 : A_1, \ldots, x_n : A_n$
    \item $\Delta = \alpha_1 : B_1, \ldots, \alpha_m : B_m$
    \end{itemize}
  \end{itemize}
\end{frame}

\begin{frame}{Sémantique informelle}
  \begin{itemize}
  \item Variables de contrôle = continuations
  \item $\mu \alpha. M \approx \mathcal{C}\ (\lambda \alpha. M)$
  \item $[\alpha]M \approx \mathtt{throw/cc}\ \alpha \ M$
  \item $\mu \alpha.[\alpha]M \approx \mathtt{call/cc}\ (\lambda \alpha. M)$
  \item Pour $x : A, y : B \vdash M : C \mid \alpha : D, \beta : E$
    \begin{itemize}
    \item $x, y$ : entrées de $M$
    \item Sortie principale de $M$ de type $C$
    \item $\alpha, \beta$ : sorties \enquote{exceptionnelles} de $M$
    \end{itemize}
  \end{itemize}
\end{frame}


\newcommand{\judgement}[3]{#1 \vdash #2 \mid #3}
\newcommand{\genericctx}[1]{\judgement{\Gamma}{#1}{\Delta}}
\newcommand{\genericctxl}[2]{\judgement{\Gamma}{#1}{#2}}
\newcommand{\genericctxr}[2]{\judgement{#1}{#2}{\Delta}}
\newcommand{\rulename}[1]{\LeftLabel{(#1)}}

\newcommand{\pair}[2]{\langle #1 , #2 \rangle}
\newcommand{\case}[2]{\lbrack #1 , #2 \rbrack}


\begin{frame}{Règles de typage}

  \begin{center}
    \begin{tabular}{c c}

      \AxiomC{}
      \rulename{$var$}
      \UnaryInfC{$\genericctxr{\Gamma, x : A}{x : A}$}
      \DisplayProof

      &

      \AxiomC{}
      \rulename{$*$}
      \UnaryInfC{$\genericctx{* : \top}$}
      \DisplayProof

    \end{tabular}
  \end{center}

    \begin{prooftree}
      \AxiomC{$\genericctx{M : A \rightarrow B}$}
      \AxiomC{$\genericctx{N : A}$}
      \rulename{$app$}
      \BinaryInfC{$\genericctx{M N : B}$}
    \end{prooftree}

    \begin{prooftree}
      \AxiomC{$\genericctxr{\Gamma, x : A}{M : B}$}
      \rulename{$abs$}
      \UnaryInfC{$\genericctx{\lambda(x : A).M : A \rightarrow B}$}
    \end{prooftree}

    \begin{prooftree}
      \AxiomC{$\genericctxl{M : A}{\alpha : A, \Delta}$}
      \rulename{$name$}
      \UnaryInfC{$\genericctxl{[\alpha]M : \bot}{\alpha : A, \Delta}$}
    \end{prooftree}

    \begin{prooftree}
      \AxiomC{$\genericctxl{M : \bot}{\alpha : A, \Delta}$}
      \rulename{$\mu$}
      \UnaryInfC{$\genericctx{\mu(\alpha : A).M : A}$}
    \end{prooftree}

\end{frame}


% on veut des produits pour avoir une CCC
\begin{frame}{Conjonction / type produit}
  \begin{itemize}
  \item $A, B, \ldots ::= \ldots \mid A \land B$
  \item $M, N, \ldots ::= \ldots \mid \pair{M}{N} \mid \pi_1\ M \mid \pi_2\ M$
  \item Règles usuelles de typage
  \end{itemize}
  \begin{prooftree}
    \AxiomC{$\genericctx{M : A}$}
    \AxiomC{$\genericctx{N : B}$}
    \rulename{$pair$}
    \BinaryInfC{$\genericctx{\pair{M}{N} : A \land B}$}
  \end{prooftree}
  \begin{center}
  \begin{tabular}{c c}
    \AxiomC{$\genericctx{M : A \land B}$}
    \rulename{$\pi_1$}
    \UnaryInfC{$\genericctx{\pi_1\ M : A}$}
    \DisplayProof
    &
    \AxiomC{$\genericctx{M : A \land B}$}
    \rulename{$\pi_2$}
    \UnaryInfC{$\genericctx{\pi_2\ M : B}$}
    \DisplayProof
  \end{tabular}    
  \end{center}
\end{frame}

\begin{frame}{Ajout de la disjonction au $\lambda \mu$-calcul}
  \begin{itemize}
  \item $\lor$ intuitionniste : type somme
    \begin{itemize}
    \item $\iota_1$, $\iota_2$, $\mathtt{case}$ \ldots
    \item Pas la solution retenue
    \end{itemize}
  \item $\lor$ classique : agit à droite du séquent
    \begin{itemize}
    \item 2 sorties de types $A$ et $B$ $\approx$ 1 sortie de type $A \lor B$
    \end{itemize}
  \end{itemize}
\end{frame}

\begin{frame}{Disjonction classique (Pym et Ritter, 1998)}
  \begin{itemize}
  \item $A, B, \ldots ::= \ldots \mid A \lor B$
  \item $M, N, \ldots ::= \ldots \mid \case{\alpha}{\beta}M \mid \mu(\alpha, \beta).M$
  \item Règles de typage à droite
  \end{itemize}
  \begin{prooftree}
    \AxiomC{$\genericctxl{M : A \lor B}{\alpha : A, \beta : B, \Delta}$}
    \rulename{$name'$}
    \UnaryInfC{$\genericctxl{\case{\alpha}{\beta}M : \bot}{\alpha : A, \beta : B, \Delta}$}
  \end{prooftree}
  \begin{prooftree}
    \AxiomC{$\genericctxl{M : \bot}{\alpha : A, \beta : B, \Delta}$}
    \rulename{$\mu'$}
    \UnaryInfC{$\genericctxl{\mu(\alpha,\beta).M : A \lor B}{\Delta}$}
  \end{prooftree}
\end{frame}


\begin{frame}{Tiers exclu en $\lambda \mu$-calcul}
  \[ \mu(\alpha : A, \beta : \lnot A). [\beta]\lambda x.[\alpha]x \]
  \begin{prooftree}
    \AxiomC{$\judgement{x : A}{x : A}{\alpha : A, \beta : \lnot A}$}
    \UnaryInfC{$\judgement{x : A}{[\alpha]x : \bot}{\alpha : A, \beta : \lnot A}$}
    \UnaryInfC{$\judgement{}{\lambda(x : A).[\alpha]x : \lnot A}{\alpha : A, \beta : \lnot A}$}
    \UnaryInfC{$\judgement{}{[\beta]\lambda(x : A).[\alpha]x : \bot}{\alpha : A, \beta : \lnot A}$}
    \UnaryInfC{$\judgement{}{\mu(\alpha : A, \beta : \lnot A).[\beta]\lambda(x : A).[\alpha]x
        : A \lor \lnot A}{}$}
  \end{prooftree}
\end{frame}

\section{Sémantique par traduction CPS}

\newcommand{\trcbn}[1]{\underline{#1}}
\newcommand{\trcbv}[1]{\overline{#1}}

\begin{frame}{Traduction CPS\footnote{\emph{continuation-passing style}} : vue d'ensemble}
  \begin{itemize}
  \item Définir la sémantique du $\lambda \mu$-calcul par traduction
    \begin{itemize}
    \item $M \simeq N$ dans $\lambda \mu$ ssi $\mathrm{trad}(M) =_{\beta \eta} \mathrm{trad}(N)$
    \end{itemize}
  \item Langage cible : $\lambda$-calcul simplement typé avec $+$ et $\times$
  \item On fixe un un type des \emph{réponses} $R$
  \item 2 choix non équivalents :
    \begin{itemize}
    \item Appel par valeur (CBV) : $M \rightsquigarrow \trcbv{M}$
    \item Appel par nom (CBN) : $M \rightsquigarrow \trcbn{M}$ (Hoffman et Streicher, 1997)
    \end{itemize}
  \item 2 notions d'équivalences
    \begin{itemize}
    \item $M =_v N \Leftrightarrow \trcbv{M} =_{\beta \eta} \trcbv{N}$
    \item $M =_n N \Leftrightarrow \trcbn{M} =_{\beta \eta} \trcbn{N}$
    \end{itemize}
  \end{itemize}
\end{frame}

\begin{frame}{Traduction des types en CBN}
  \begin{itemize}
  \item On définit, pour $A$ type de $\lambda \mu$ :
    \begin{itemize}
    \item $K_A$ : type des \emph{continuations} associé à $A$
    \item $C_A$ : type des \emph{calculs} associé à $A$
    \end{itemize}
  \item Par induction structurelle :
  \end{itemize}
  % Pourquoi K_{A \land B} = K_A + K_B ??? Réfléchir !!!
  \begin{align*}
    K_\top &= 0 \\
    K_{A \land B} &= K_A + K_B \\
    K_\bot &= 1 \\
    K_{A \lor B} &= K_A \times K_B \\
    K_{A \rightarrow B} &= C_A \times K_B \\
    C_A &= K_A \rightarrow R
  \end{align*}
\end{frame}

\begin{frame}{Traduction des termes en CBN (1)}
  \begin{itemize}
  \item Par induction structurelle :
  \end{itemize}
  \begin{align*}
    \trcbn{x} &= \lambda(k : K_A).\ \tilde{x}\ k
    & (x : A) \\
    % voir ça comme une pile avec des cons (voir aussii la machine de Krivine)
    \trcbn{M \ N} &= \lambda(k : K_B).\ \trcbn{M}\ \pair{\trcbn{N}}{k}
    & (M : A \rightarrow B, N : A) \\
    \trcbn{\lambda(x:A).\ M} &= \lambda(\pair{\tilde{x}}{k} : K_{A \rightarrow B}).\ \trcbn{M}\ k
    & (M : B) \\
    \trcbn{[\alpha]M} &= \lambda(k : 1).\ \trcbn{M}\ \tilde\alpha
    & (M : A, \alpha : A) \\
    \trcbn{\mu(\alpha : A).\ M} &= \lambda(\tilde\alpha : K_A).\ \trcbn{M}\ * 
    & (M : \bot) \\
  \end{align*}
  \begin{itemize}
  \item Abréviation $\lambda\pair{x}{y}.\ t = \lambda z.\ t\{x \backslash \pi_1 z\}\{y \backslash \pi_2 z\}$
  \end{itemize}
\end{frame}

\begin{frame}{Traduction des termes en CBN (2)}
  \begin{itemize}
  \item Abr. $[t,u] = \mathtt{function}\ \mid (\iota_1\ x) \Rightarrow t\ x \mid (\iota_2\ y) \Rightarrow u\ y$
  \end{itemize}
  \begin{align*}
    \trcbn{\pair{M}{N}} &= \lambda(k : K_{A \land B}).\ \left[\trcbn{M},\trcbn{N}\right]\ k
    & (M : A, N : B) \\
    \trcbn{\pi_1\ M} &= \lambda(k : K_{A}).\ \trcbn{M}\ (\iota_1\ k)
    & (M : A \land B) \\    
    \trcbn{\pi_2\ M} &= \lambda(k : K_{B}).\ \trcbn{M}\ (\iota_2\ k)
    & (M : A \land B) \\    
    \trcbn{[\alpha, \beta]M} &= \lambda(k : 1).\ \trcbn{M}\ \pair{\tilde\alpha}{\tilde\beta}
    & (M : A \lor B, \alpha : A, \beta : B) \\
    \trcbn{\mu(\alpha : A, \beta : B).\ M} &=
    \lambda(\pair{\tilde\alpha}{\tilde\beta} : K_{A \lor B}).\ \trcbn{M}\ *
    & (M : \bot) \\
  \end{align*}
\end{frame}

\begin{frame}{Traduction des jugements de typage en CBN}
  \begin{théorème}[préservation du typage en CBN]
    Si $\judgement{x_1 : B_1, \ldots, x_n : B_n}{M : A}{\alpha_1 : A_1, \ldots, \alpha_m : A_m}$,
    alors $\tilde{x}_1 : C_{B_1}, \ldots, \tilde{x}_n : C_{B_n}, \tilde\alpha_1 : K_{A_1}, \ldots, \tilde\alpha_m : K_{A_m} \vdash \trcbn{M} : C_A$
  \end{théorème}
  \begin{itemize}
  \item Traduction des jugements : $\trcbn{\genericctx{M : A}}$
  \end{itemize}
\end{frame}

% La même chose...

\begin{frame}{Traduction des types en CBV}
  \begin{itemize}
  \item On définit, pour $A$ type de $\lambda \mu$ :
    \begin{itemize}
    \item $K_A$ : type des \emph{continuations} associé à $A$
    \item $C_A$ : type des \emph{calculs} associé à $A$
    \item $V_A$ : type des \emph{valeurs} associé à $A$
    \end{itemize}
  \end{itemize}
  \begin{align*}
    V_\top &= 1 \\
    V_{A \land B} &= V_A \times V_B \\
    V_\bot &= 0 \\
    V_{A \lor B} &= V_A + V_B \\
    V_{A \rightarrow B} &= V_A \times K_B \rightarrow R \quad (\cong V_A \rightarrow C_B) \\
    K_A &= V_A \rightarrow R \\
    C_A &= K_A \rightarrow R
  \end{align*}
\end{frame}

\begin{frame}{Traduction des termes en CBV (1)}
  \begin{itemize}
  \item Par induction structurelle :
  \end{itemize}
  \begin{align*}
    \trcbv{x} &= \lambda(k : K_A).\ k\ \tilde{x}
    & (x : A) \\
    \trcbv{M \ N} &= \lambda(k : K_B).\ \trcbv{M}\ (\lambda m.\ \trcbv{N}\ (\lambda n.\ k\ \pair{m}{n}))
    & (M : A \rightarrow B, N : A) \\
    \trcbv{\lambda(x:A).\ M} &= \lambda(\pair{\tilde{x}}{k} : K_{A \rightarrow B}).
    \ k\ (\lambda\pair{\tilde{x}}{c}.\ \trcbv{M}\ c)
    & (M : B) \\
    \trcbv{[\alpha]M} &= \lambda(k : K_\bot).\ \trcbv{M}\ \tilde\alpha
    & (M : A, \alpha : A) \\
    \trcbv{\mu(\alpha : A).\ M} &= \lambda(\tilde\alpha : K_A).\ \trcbv{M}\ * 
    & (M : \bot) \\
  \end{align*}
  \begin{itemize}
  \item Etc.
  \end{itemize}
\end{frame}

\begin{frame}{Traduction des jugements de typage en CBV}
  \begin{théorème}[préservation du typage en CBV]
    Si $\judgement{x_1 : B_1, \ldots, x_n : B_n}{M : A}{\alpha_1 : A_1, \ldots, \alpha_m : A_m}$,
    alors $\tilde{x}_1 : V_{B_1}, \ldots, \tilde{x}_n : V_{B_n}, \tilde\alpha_1 : K_{A_1}, \ldots, \tilde\alpha_m : K_{A_m} \vdash \trcbv{M} : C_A$
  \end{théorème}
  \begin{itemize}
  \item Traduction des jugements : $\trcbv{\genericctx{M : A}}$
  \end{itemize}
\end{frame}

\newcommand{\lambdarpt}{\lambda^{R+\times}}

\begin{frame}{Remarques sur l'image de la traduction}
  \begin{itemize}
  \item Dans les termes élaborés, toutes les abstractions ont un type de la forme
    $A \rightarrow R$ ($R$ type des réponses)
    \begin{itemize}
    \item On peut se restreindre au fragment $\lambdarpt$ où \\
      $t, u, \ldots ::= \ldots \mid \lambda x . (t : R) \mid \ldots$
    \end{itemize}
  \item En CBN, $K_A$ et $C_A$ sont de la forme $B \rightarrow R$
  \item En CBV, $K_A$ et $C_A$ sont de la forme $B \rightarrow R$, mais pas $V_A$
  \end{itemize}
\end{frame}


\section{De \texorpdfstring{$\lambdarpt$}{lambda-R-plus-fois} aux catégories de contrôle}

\begin{frame}{Modèle catégorique de $\lambdarpt$}
  \begin{itemize}
  \item Interprétation du $\lambda$-calcul avec $+$ et $\times$ : catégories bicartésiennes closes
  \item Pour interpréter $\lambdarpt$, on a besoin de
    \begin{itemize}
    \item $+$ : coproduit
    \item $\times$ : produit
    \item $R$ : choix d'objet distingué
    \item $\_ \rightarrow R$ : exponentielle
    \end{itemize}
  \end{itemize}
\end{frame}

\begin{frame}{Catégories de réponses}
  \begin{définition}
    Une \emph{catégorie de réponses} est une catégorie $\mathbf{C}$ admettant
    \begin{itemize}
    \item des produits finis
    \item des coproduits finis
    \item un \emph{objet des réponses} $R \in \mathbf{C}$
    \item pour tout $A \in \mathbf{C}$, une exponentielle $A \Rightarrow R$ (ou $R^A$)
      % équivalent à l'existence d'un adjoint à _ \times R
    \end{itemize}
    tels que
    \begin{itemize}
    \item $\times$ distribue sur $+$
    \item le morphisme canonique $A \rightarrow (A \Rightarrow R) \Rightarrow R$
      soit un monomorphisme
    \end{itemize}
  \end{définition}
  \begin{itemize}
  \item $\lambdarpt$ s'interprète naturellement dans une catégorie de réponses
  \end{itemize}
\end{frame}

\begin{frame}
  \frametitle{Catégories de continuations}
  \begin{définition}
    Soit $\mathbf{C}$ une catégorie de réponses. La \emph{catégorie des continuations}
    de $\mathbf{C}$ est la sous-catégorie pleine dont les objets
    sont de la forme $A \Rightarrow R$. Elle est notée $R^{\mathbf{C}}$.
  \end{définition}
  \begin{théorème}
    Une catégorie de continuations est cartésienne close.
  \end{théorème}
  \begin{itemize}
  \item $1 \cong R^0$
  \item $R^A \times R^B \cong R^{A+B}$
  \item $(R^B)^{R^A} \cong R^{B \times R^A}$
  \end{itemize}
\end{frame}

\begin{frame}
  \frametitle{Structure prémonoïdale symétrique}
  \begin{définition}[$\parr$]
    On définit sur $R^{\mathbf{C}}$ le connecteur
    $(A \Rightarrow R) \parr (B \Rightarrow R) 
    \overset{\mbox{\tiny{déf}}}{=}(A \times B \Rightarrow R)$
  \end{définition}
  \begin{itemize}
  \item $A_1 \times \ldots \times A_n \Rightarrow R =
    (A_1 \Rightarrow R) \parr \ldots \parr (A_n \Rightarrow R)$
  \item $\parr$ est associatif et commutatif (à $\cong$ près)
  \item $R \cong 1 \Rightarrow R$ est un neutre, noté aussi $\bot$
  \item $A \parr (B \times C) \cong (A \parr B) \times (A \parr C)$
  \item structure \emph{prémonoïdale} :
    \begin{itemize}
    \item $(A \Rightarrow R) \parr (B \Rightarrow R) \cong B \Rightarrow (A \Rightarrow R)$ :
      fonctoriel en $(A \Rightarrow R)$
    \item $ \_ \parr R^B$ et $R^A \parr \_$ endofoncteurs de $R^{\mathbf{C}}$
    \item $ \_ \parr \_$ n'est pas un bifoncteur
    \end{itemize}
  \end{itemize}
\end{frame}

\begin{frame}
  \frametitle{Quelques mots sur les catégories de contrôle}
  \begin{itemize}
  \item Catégories de contrôle : axiomatisation \enquote{algébrique} des catégories de continuations
  \item Étudiées en profondeur dans l'article
  \item Catégorie $\mathbf{P}$ avec $1, \times, \bot, \parr$
  \item Axiomes :
    \begin{itemize}
    \item $(\mathbf{P}, 1, \times)$ cartésienne close
    \item $(\mathbf{P}, \bot, \parr)$ prémonoïdale symétrique
    \item distributivité
    \item autre condition technique (codiagonales)
    \end{itemize}
  \end{itemize}
\end{frame}

\begin{frame}
  \frametitle{Théorème de structure des catégories de contrôle}
  \begin{théorème}
    Toute catégorie de continuations est une catégorie de contrôle.
  \end{théorème}
  \begin{itemize}
  \item Vérification mécanique des axiomes
  \end{itemize}
  \begin{théorème}[de structure]
    Toute catégorie de contrôle est équivalente à une catégorie de continuations.
  \end{théorème}
  \begin{itemize}
  \item Gros résultat de l'article !
  \item Non traité ici
  \end{itemize}
\end{frame}

\begin{frame}
  \frametitle{Structure co-close faible}
  \begin{itemize}
  \item On pose $A \multimapinv B = (B \Rightarrow A) \Rightarrow \bot$
  \item Il existe $coapp : B \rightarrow (B \multimapinv A) \parr A$
  \item $\forall f : B \to C \parr A, \exists! cocurry(f) : (B \multimapinv A) \rightarrow C$\\
    satisfaisant une propriété universelle
  \end{itemize}
\end{frame}

\begin{frame}
  \frametitle{Catégories de co-contrôle}
  \begin{itemize}
  \item Dual d'une catégorie de contrôle
  \end{itemize}
  \begin{center}
  \begin{tabular}{c | c}
    Contrôle & Co-contrôle \\
    \hline
    1 & 0 \\
    $A \times B$ & $A + B$ \\
    $\bot$ & $\top$ \\
    $A \parr B$ & $A \otimes B$ \\
    $B \multimapinv A$ & $A \multimap B$
  \end{tabular}
  \end{center}
  \begin{itemize}
  \item Structure close faible sur une catégorie de co-contrôle :
    \begin{itemize}
    \item $app : (A \multimap B) \otimes A \rightarrow B$
    \item $curry(f) : C \rightarrow (A \multimap B)$
    \end{itemize}
  \end{itemize}
\end{frame}


\section{Interprétation catégorique de \texorpdfstring{$\lambda \mu$}{lambda-mu} et dualité}

\begin{frame}
  \frametitle{Interprétation de $\lambda \mu$ dans une catégorie}
  \begin{itemize}
  \item $\mathbf{C}$ une catégorie de réponses
  \item On passe par l'interprétation \enquote{naturelle} de $\lambdarpt$, \\
    et par la traduction CPS en CBN
  \item $\denot{\_}$ : jugements de typage $\rightarrow$ morphismes dans $\mathbf{C}$
  \item Rappel :
    \begin{prooftree}
      \AxiomC{$\judgement{x_1 : B_1, \ldots, x_n : B_n}{M : A}{\alpha_1 : A_1, \ldots, \alpha_m : A_m}$}
      \UnaryInfC{$\tilde{x}_1 : C_{B_1}, \ldots, \tilde{x}_n : C_{B_n}, \tilde\alpha_1 : K_{A_1}, \ldots, \tilde\alpha_m : K_{A_m} \vdash \trcbn{M} : C_A$}
    \end{prooftree}
  \item $\denot{\tilde{x}_1 : C_{B_1}, \ldots, \tilde{x}_n : C_{B_n}, \tilde\alpha_1 : K_{A_1}, \ldots, \tilde\alpha_m : K_{A_m} \vdash \trcbn{M} : C_A}_{\lambdarpt} = \phi : C_{B_1} \times \ldots \times C_{B_n} \times K_{A_1}\times \ldots \times K_{A_m} \rightarrow C_A$

  \end{itemize}
\end{frame}

\begin{frame}
  \frametitle{Interprétation de $\lambda \mu$ (bis)}
  \begin{itemize}
  \item Rappel : $C_A = (K_A \Rightarrow R)$
  \item On réécrit
    \begin{itemize}
    \item $\phi : C_{B_1} \times \ldots \times C_{B_n} \times K_{A_1}\times \ldots \times K_{A_m} \rightarrow K_A \Rightarrow R$
    \item en $\hat\phi : C_{B_1} \times \ldots \times C_{B_n} \rightarrow K_A \times K_{A_1}\times \ldots \times K_{A_m} \Rightarrow R$
    \end{itemize}
  \item Rappel :  $(A \Rightarrow R) \parr (B \Rightarrow R) = (A \times B \Rightarrow R)$
  \item $\hat\phi : C_{B_1} \times \ldots \times C_{B_n} \rightarrow C_A \parr C_{A_1}\parr \ldots \parr C_{A_m}$
  \item $\denot{\judgement{x_1 : B_1, \ldots, x_n : B_n}{M : A}{\alpha_1 : A_1, \ldots, \alpha_m : A_m}} \overset{\mbox{\tiny{déf}}}{=} \hat\phi$
  \item L'image de l'interprétation est dans $R^{\mathbf{C}}$ !
  \end{itemize}
\end{frame}

\begin{frame}
  \frametitle{Interprétation directe en CBN}
  \begin{itemize}
  \item Définir directement la sémantique dénotationelle dans une catégorie de contrôle, sans passer par la traduction CPS
  \item $\denot{\judgement{x_1 : B_1, \ldots, x_n : B_n}{M : A}{\alpha_1 : A_1, \ldots, \alpha_m : A_m}}_n : \denot{B_1}_n \times \ldots \times \denot{B_n}_n \rightarrow \denot{A}_n \parr \denot{A_1}_n \parr \ldots \parr \denot{A_m}_n$
  \item Interprétation des types :
    \begin{itemize}
    \item $\denot{\top}_n = 1$
    \item $\denot{A \land B}_n = \denot{A}_n \times \denot{B}_n$
    \item $\denot{A \rightarrow B}_n = \denot{A}_n \Rightarrow \denot{B}_n$
    \item $\denot{\bot}_n = \bot$
    \item $\denot{A \lor B}_n = \denot{A}_n \parr \denot{B}_n$
    \end{itemize}
  \item Interprétation des termes :
    \begin{itemize}
    \item utiliser les morphismes structurels d'une catégorie de contrôle
    \end{itemize}
  \end{itemize}
\end{frame}

\begin{frame}
  \frametitle{Sémantique obtenue}
  \begin{théorème}
    En appel par nom, l'interprétation directe du $\lambda\mu$-calcul dans $R^{\mathbf{C}}$ coïncide avec l'interprétation de la traduction CPS dans $\mathbf{C}$.
  \end{théorème}
  \begin{théorème}[correction et complétude de la sémantique]
    $M =_n N$ si et seulement si $\denot{M}_n = \denot{N}_n$.
  \end{théorème}
\end{frame}


\begin{frame}
  \frametitle{Interprétation CBV (par traduction CPS) (1)}
  \begin{itemize}
  \item Rappel :
    \begin{prooftree}
      \AxiomC{$\judgement{x_1 : B_1, \ldots, x_n : B_n}{M : A}{\alpha_1 : A_1, \ldots, \alpha_m : A_m}$}
      \UnaryInfC{$\tilde{x}_1 : V_{B_1}, \ldots, \tilde{x}_n : V_{B_n}, \tilde\alpha_1 : K_{A_1}, \ldots, \tilde\alpha_m : K_{A_m} \vdash \trcbv{M} : C_A$}

    \end{prooftree}
  \item $\denot{\tilde{x}_1 : V_{B_1}, \ldots, \tilde{x}_n : V_{B_n}, \tilde\alpha_1 : K_{A_1}, \ldots, \tilde\alpha_m : K_{A_m} \vdash \trcbn{M} : C_A}_{\lambdarpt} = \psi : V_{B_1} \times \ldots \times V_{B_n} \times K_{A_1}\times \ldots \times K_{A_m} \rightarrow C_A$
  \item Remarques :
    \begin{itemize}
    \item $K_A = V_A \Rightarrow R$ et $C_A = K_A \Rightarrow R$ sont dans $R^{\mathbf{C}}$
    \item $V_A$ n'est pas forcément dans $R^{\mathbf{C}}$ !
    \end{itemize}
  \end{itemize}
\end{frame}

\begin{frame}
  \frametitle{Interprétation CBV (par traduction CPS) (2)}
  \begin{itemize}
  \item On réécrit
    \begin{itemize}
    \item $\psi : V_{B_1} \times \ldots \times V_{B_n} \times K_{A_1}\times \ldots \times K_{A_m} \rightarrow K_A \Rightarrow R$
    \item en $\hat\psi :  K_A \times K_{A_1}\times \ldots \times K_{A_m} \rightarrow V_{B_1} \times \ldots \times V_{B_n} \Rightarrow R$
    \end{itemize}
  \item $\hat\psi : K_A \times K_{A_1} \times \ldots \times K_{A_m} \rightarrow K_{B_1}\parr \ldots \parr K_{B_n}$
  \item La flèche est dans le \enquote{mauvais sens}
    \begin{itemize}
    \item On prend la catégorie duale !
    \end{itemize}
  \item $\hat\psi^{\mathrm{op}} : K_{B_1} \otimes \ldots \otimes K_{B_n} \rightarrow K_A + K_{A_1} + \ldots + K_{A_m}$
  \item $\denot{\judgement{x_1 : B_1, \ldots, x_n : B_n}{M : A}{\alpha_1 : A_1, \ldots, \alpha_m : A_m}} \overset{\mbox{\tiny{déf}}}{=} \hat\psi^{\mathrm{op}}$
  \end{itemize}
\end{frame}

\begin{frame}
  \frametitle{Interprétation CBV (directe)}
  \begin{itemize}
  \item Dans une catégorie de co-contrôle
  \item $\denot{\judgement{x_1 : B_1, \ldots, x_n : B_n}{M : A}{\alpha_1 : A_1, \ldots, \alpha_m : A_m}}_v : \denot{B_1}_v \otimes \ldots \otimes \denot{B_n}_v \rightarrow \denot{A}_v + \denot{A_1}_v + \ldots + \denot{A_m}_v$
  \item Interprétation des types :
    \begin{itemize}
    \item $\denot{\top}_v = \top$
    \item $\denot{A \land B}_v = \denot{A}_v \otimes \denot{B}_v$
    \item $\denot{A \rightarrow B}_v = \denot{A}_v \multimap \denot{B}_v$
    \item $\denot{\bot}_v = 0$
    \item $\denot{A \lor B}_v = \denot{A}_v + \denot{B}_v$
    \end{itemize}
  \item Utilise la structure close faible
  \item Interprétation des termes :
    \begin{itemize}
    \item utiliser les morphismes structurels d'une catégorie de co-contrôle
    \end{itemize}
  \end{itemize}
\end{frame}

\begin{frame}
  \frametitle{Sémantique obtenue}
  \begin{théorème}
    En appel par valeur, l'interprétation directe du $\lambda\mu$-calcul dans $R^{\mathbf{C}}$ coïncide avec l'interprétation de la traduction CPS dans $\mathbf{C}$.
  \end{théorème}
  \begin{théorème}[correction et complétude de la sémantique]
    $M =_ N$ si et seulement si $\denot{M}_v = \denot{N}_v$.
  \end{théorème}
\end{frame}

\begin{frame}
  \frametitle{Dualité CBN/CBV}
  \begin{itemize}
  \item Dualité \enquote{syntax-free} entre catégories de contrôle et catégories de co-contrôle
    \begin{itemize}
    \item Échange $\times$ et $+$, $\parr$ et $\otimes$
    \item Parfaitement involutive
    \end{itemize}
  \item Dualité syntaxique entre $\lambda\mu$-termes en CBN et $\lambda\mu$-termes en CBV
    \begin{itemize}
    \item Sur les types : De Morgan ; involutive à isomorphisme de type près
    \item Sur les termes : échange fonctionnel pur et effets de bord
    \end{itemize}
  \item Passage sémantique $\to$ syntaxique : langages internes
  \end{itemize}
\end{frame}

\section{Bonus : pourquoi c'est prémonoïdal ?}

\begin{frame}
  \frametitle{Non-commutativité : exemple}
  \begin{itemize}
  \item En appel par valeur, les 2 termes suivants sont différents :
    \begin{itemize}
    \item \texttt{let $x = M$ in let $y = N$ in $P$}
    \item \texttt{let $y = N$ in let $x = M$ in $P$}
    \end{itemize}
  \item Problème quand $M$ ou $N$ produit un effet de bord
  \item Par contre, ils sont équivalents en appel par nom
  \end{itemize}
\end{frame}

\begin{frame}
  \frametitle{Non-commutativité : version catégorique}
  \begin{itemize}
  \item Dans une catégorie de co-contrôle, les 2 morphismes suivants sont différents
    \begin{itemize}
    \item $\denot{\Gamma} \otimes \denot{\Gamma} 
      \xrightarrow{\denot{M} \otimes \denot{\Gamma}}
      \denot{A} \otimes \denot{\Gamma}
      \xrightarrow{\denot{A} \otimes \denot{N}}
      \denot{A} \otimes \denot{B} = \denot{A \land B}_v$
    \item $\denot{\Gamma} \otimes \denot{\Gamma} 
      \xrightarrow{\denot{\Gamma} \otimes \denot{N}}
      \denot{\Gamma} \otimes \denot{B}
      \xrightarrow{\denot{M} \otimes \denot{B}}
      \denot{A} \otimes \denot{B} = \denot{A \land B}_v$
    \end{itemize}
  \item $\otimes$ n'est pas bifonctoriel !
  \item Dans une catégorie de contrôle, $\times$ est bifonctoriel
  \end{itemize}
\end{frame}

\begin{frame}
  \frametitle{Non-commutativité : exemple dual}
  \begin{itemize}
  \item En appel par nom, les 2 termes suivants sont différents :
    \begin{itemize}
    \item \texttt{let $x = \mu\alpha.$(let $y = \mu\beta.P$ in $N$) in $M$}
    \item \texttt{let $y = \mu\beta.$(let $x = \mu\alpha.P$ in $M$) in $N$}
    \end{itemize}
  \item $\parr$ n'est pas bifonctoriel
  \end{itemize}
\end{frame}

\begin{frame}
  \frametitle{Et si $\parr$ était bifonctoriel ?}
  \begin{théorème}
    Une catégorie de contrôle dans laquelle $\parr$ est bifonctoriel
    est une algèbre de Boole.
  \end{théorème}
  \begin{itemize}
  \item La logique classique est dégénérée\ldots
  \end{itemize}
\end{frame}

\end{document}
