Hopefully unfsck the whole situation with CPS translation and typing.

1 files changed, 135 insertions, 45 deletions

diff --git a/transp-inf110-02-typage.tex b/transp-inf110-02-typage.tex
index 3d44a81..380d40d 100644
--- a/transp-inf110-02-typage.tex
+++ b/transp-inf110-02-typage.tex
@@ -3583,7 +3583,7 @@ callcc\_cps (fun kf -> fun k -> kf 42 (fun v -> sum\_cps v 1 k)) (fun x -> x) ;;
 \end{frame}
 %
 \begin{frame}
-\frametitle{Continuation Passing Style : transformation des types}
+\frametitle{Continuation Passing Style : systématisation}
 
 \textcolor{blue}{Définissons la transformation CPS de façon
   systématique.}
@@ -3593,11 +3593,85 @@ callcc\_cps (fun kf -> fun k -> kf 42 (fun v -> sum\_cps v 1 k)) (fun x -> x) ;;
 {\footnotesize Prenons ici les notations logiques pour les types :
   notamment, $\Rightarrow$ désigne le type fonction.\par}
 
+\medskip
+
+\itempoint Fixons un type $Z$ de « retour ultime ».  On pose
+\alert{$\mathop{\sim}P := (P\Rightarrow Z)$} pour le type d'« une
+continuation qui attend une valeur de type $P$ » et
+$\mathop{\sim}\mathop{\sim}P$ pour « une valeur $P$ passée par
+continuation ».
+
+\medskip
+
+\itempoint Noter que $x:P \;\vdash\; \lambda(k:\mathop{\sim}P).kx :
+\mathop{\sim}\mathop{\sim}P$ (transformation d'une valeur « directe »
+en valeur passée par continuation).
+
+\medskip
+
+{\footnotesize On si on préfère voir ça comme une fonction :
+  $\lambda(x:P).\,\lambda(k:\mathop{\sim}P).\,kx$ a pour type $P
+  \Rightarrow \mathop{\sim}\mathop{\sim}P$.\par}
+
+\medskip
+
+\itempoint On va passer \alert{toutes} les valeurs par continuation :
+tous les types transformés prendront la forme
+$\mathop{\sim}\mathop{\sim}T$.
+
 \smallskip
 
-\itempoint Fixons un type $Z$ de « retour ultime ».  On définit une
-transformation $P \mapsto P^\diamond$ des types (=propositions) en posant
-$\mathop{\sim}P := (P\Rightarrow Z)$, puis (inductivement) :
+Mais en plus de ça, les fonctions renvoient leur valeur par
+continuation : une fonction de type $P \Rightarrow Q$ va devenir $P
+\Rightarrow \mathop{\sim}Q \Rightarrow Z$, c'est-à-dire $P \Rightarrow
+\mathop{\sim}\mathop{\sim}Q$, et sera elle-même passée par
+continuation, donc $\mathop{\sim}\mathop{\sim}(P \Rightarrow
+\mathop{\sim}\mathop{\sim}Q)$ {\footnotesize (sans compter que $P$ et
+  $Q$ peuvent eux-mêmes changer)}.
+
+\end{frame}
+%
+\begin{frame}
+\frametitle{Continuation Passing Style : l'essence de la transformation}
+
+\itempoint Définissons la transformation CPS d'abord dans le
+$\lambda$-calcul \alert{non typé} : par induction sur la complexité du
+terme :
+\begin{itemize}
+\item $v^{\cps} = \lambda k.kv$ si $v$ est une variable (c'est la
+  transformation de $P$ en $\mathop{\sim}\mathop{\sim}P$ définie
+  ci-dessus).
+\item $(\lambda v.t)^{\cps} = \lambda k.\, k(\lambda v.\, t^{\cps})$
+  (idem pour une fonction, dont le corps est CPS-ifié).
+\item pour l'application : \[(fx)^{\cps} = \lambda
+  k.\,f^{\cps}(\lambda f_0.\, x^{\cps}(\lambda x_0.\, f_0 x_0 k))\] ce
+  code se comprend ainsi : on invoque $f^{\cps}$ pour recevoir sa
+  valeur « directe » $f_0$ (qui est quand même une fonction dans le
+  style CPS), puis $x^{\cps}$ pour recevoir sa valeur « directe »
+  $x_0$, puis on appelle la fonction $f_0$ avec la valeur $x_0$ et la
+  continuation $k$ de l'ensemble de l'expression,
+\item $\texttt{callcc}^{\cps} = \lambda \ell.\, \ell(\lambda g.\,
+  \lambda k.\, g(\lambda v.\, \lambda k_0.\, kv)\,k)$
+\end{itemize}
+
+\medskip
+
+\itempoint Ce code \alert{porte les graines d'un interpréteur}
+(eval/apply) du $\lambda$-calcul dans le $\lambda$-calcul : il impose
+d'ailleurs l'évaluation en appel-par-valeurs.
+
+\end{frame}
+%
+\begin{frame}
+\frametitle{Continuation Passing Style : transformation des types}
+
+{\footnotesize Il reste à typer tout ça !\par}
+
+\smallskip
+
+\itempoint Rappelons qu'on a fixé $Z$ et posé $\mathop{\sim}P :=
+(P\Rightarrow Z)$.  On définit une transformation $P \mapsto
+P^\diamond$ des types (=propositions) par (inductivement) :
 \begin{itemize}
 \item $A^\diamond = A$ si $A$ est une variable de type,
 \item $(P\Rightarrow Q)^\diamond = (P^\diamond \Rightarrow \mathop{\sim}\mathop{\sim}Q^\diamond)$,
@@ -3609,25 +3683,27 @@ $\mathop{\sim}P := (P\Rightarrow Z)$, puis (inductivement) :
 
 \smallskip
 
-\itempoint Il faut comprendre $\mathop{\sim}P$ comme « une
-continuation qui attend un type $P$ » et $\mathop{\sim}\mathop{\sim}P$
-comme « une valeur $P$ passée par continuation ».
-
-\smallskip
-
-\itempoint Noter que $x:P \;\vdash\; \lambda(k:\mathop{\sim}P).kx :
-\mathop{\sim}\mathop{\sim}P$ (transformation d'une valeur « directe »
-en valeur passée par continuation).
+\itempoint On pose enfin $P^{\cps} :=
+\mathop{\sim}\mathop{\sim}P^\diamond$ {\footnotesize (comprendre :
+  $\mathop{\sim}\mathop{\sim}(P^\diamond)$)}.
 
 \smallskip
 
-{\footnotesize On si on préfère voir ça comme une fonction :
-  $\lambda(x:P).\,\lambda(k:\mathop{\sim}P).\,kx$ a pour type $P
-  \Rightarrow \mathop{\sim}\mathop{\sim}P$.\par}
+En gros :
+\begin{itemize}
+\item $P^\diamond$ est le type $P$ dans lequel toutes les fonctions
+  ont été réécrites en style CPS (= renvoient leurs valeurs par
+  continuation),
+\item $P^{\cps} := \mathop{\sim}\mathop{\sim}P^\diamond$ est le type
+  en question lui-même passé par continuation.
+\end{itemize}
 
 \smallskip
 
-\itempoint On pose $P^{\cps} := \mathop{\sim}\mathop{\sim}P^\diamond$.
+{\footnotesize \itempoint Noter : $(P\Rightarrow Q)^{\cps} =
+  \mathop{\sim}\mathop{\sim}(P^\diamond \Rightarrow
+  \mathop{\sim}\mathop{\sim}Q^\diamond) =
+  \mathop{\sim}\mathop{\sim}(P^\diamond \Rightarrow Q^{\cps})$.}
 
 %% {\footnotesize
 %% 
@@ -3652,31 +3728,44 @@ $\vdash t:P$ alors $\vdash t^{\cps}:P^{\cps}$ (rappel :
 $\mathop{\sim}P := (P\Rightarrow Z)$ et $P^{\cps} :=
 \mathop{\sim}\mathop{\sim}P^\diamond$) :
 \begin{itemize}
-\item $v^{\cps} = \lambda k.kv$ si $v$ est une variable
-\item $(fx)^{\cps} = \lambda k.\,f^{\cps}(\lambda f_0.\,
-  x^{\cps}(\lambda x_0.\, f_0 x_0 k))$
-\item $(\lambda v.t)^{\cps} =
-  \lambda k.\, k(\lambda v.\, t^{\cps})$
-\item $\langle x,y\rangle^{\cps} = \lambda k.\, x^{\cps}(\lambda
-  x_0.\, y^{\cps} (\lambda y_0.\, k\langle x_0,y_0\rangle))$
-\item $(\pi_i z)^{\cps} = \lambda k.\, z^{\cps}(\lambda z_0.\, k(\pi_i
-  z_0))$ (pour $i\in\{1,2\}$)
-\item $(\iota_i z)^{\cps} = \lambda k.\, z^{\cps}(\lambda z_0.\,
-  k(\iota_i z_0))$ (pour $i\in\{1,2\}$)
+\item $v^{\cps} = \lambda(k:\mathop{\sim}P^\diamond).\,kv$ lorsque $v$
+  est une variable de type $P$,
+\item $(fx)^{\cps} = \lambda (k:\mathop{\sim}Q^\diamond).\,
+  f^{\cps}(\lambda (f_0:P^\diamond\Rightarrow Q^{\cps}).\,
+  x^{\cps}(\lambda (x_0:P^\diamond).\, f_0 x_0 k))$ lorsque $f :
+  P\Rightarrow Q$ et $x : Q$ (rappel : $(P\Rightarrow Q)^{\cps} =
+  \mathop{\sim}\mathop{\sim}(P^\diamond \Rightarrow Q^{\cps})$),
+\item $(\lambda (v:P).t)^{\cps} = \lambda k.\, k(\lambda
+  (v:P^\diamond).\, t^{\cps})$ lorsque $\Gamma, v:P \vdash t:Q$,
+\item $\langle x,y\rangle^{\cps} = \lambda
+  (k:\mathop{\sim}(Q_1^\diamond \land Q_2^\diamond)).\,
+  x^{\cps}(\lambda (x_0:Q_1^\diamond).\, y^{\cps} (\lambda
+  (y_0:Q_2^\diamond).\, k\langle x_0,y_0\rangle))$,
+\item $(\pi_i z)^{\cps} = \lambda (k:\mathop{\sim} Q_i^\diamond).\,
+  z^{\cps}(\lambda (z_0:Q_1^\diamond\land Q_2^\diamond).\, k(\pi_i
+  z_0))$ (pour $i\in\{1,2\}$),
+\item $(\iota^{(Q_1,Q_2)}_i z)^{\cps} = \lambda
+  (k:\mathop{\sim}(Q_1^\diamond\lor Q_2^\diamond)).\, z^{\cps}(\lambda
+  (z_0:Q_i^\diamond).\, k(\iota^{(Q_1^\diamond,Q_2^\diamond)}_i z_0))$
+  (pour $i\in\{1,2\}$),
 \item $(\texttt{match~}r\texttt{~with~}\iota_1 v_1 \mapsto t_1,\;
-  \iota_2 v_2 \mapsto t_2)^{\cps} = \lambda k.\, r^{\cps}(\lambda
-  r_0.\, (\texttt{match~}r_0\texttt{~with~}\iota_1 v_1 \mapsto
+  \iota_2 v_2 \mapsto t_2)^{\cps} = \lambda
+  (k:\mathop{\sim}Q^\diamond).\, r^{\cps}(\lambda
+  (r_0:P_1^\diamond\lor P_2^\diamond).\penalty0\,
+  (\texttt{match}\penalty500\ r_0\ \texttt{with}\ \iota_1 v_1 \mapsto
   t_1^{\cps} k,\; \iota_2 v_2 \mapsto t_2^{\cps} k))$
-\item $\bullet^{\cps} = \lambda k.k\bullet$ \quad\itempoint
-  $(\texttt{exfalso~} r)^{\cps} = \lambda k.\, r^{\cps}(\lambda r_0.\,
-  (\texttt{exfalso~}r_0))$
+\item $\bullet^{\cps} = \lambda (k:\mathop{\sim}\top).k{\bullet}$
+\item $(\texttt{exfalso}^{(Q)} r)^{\cps} = \lambda
+  (k:\mathop{\sim}Q^\diamond).\, r^{\cps}(\lambda (r_0:\bot).\,
+  (\texttt{exfalso}^{(Q^\diamond)} r_0))$
 \end{itemize}
 
-\itempoint Ajoutons : $\lambda(k:\mathop{\sim}(P\lor \mathop{\sim}
-P)).\, k(\iota_2^{(P,\mathop{\sim}
-  P)}(\lambda(v:P).\,k(\iota_1^{(P,\mathop{\sim} P)} v)))$ de type
-$\mathop{\sim}\mathop{\sim}(P\lor \mathop{\sim} P)$, dont on tire
-facilement $(P\lor\neg P)^{\cps}$ (ceci donne par exemple le call/cc).
+\itempoint $\texttt{callcc}^{\cps} = \lambda (\ell:\cdots).\,
+\ell(\lambda (g : (P^\diamond \Rightarrow Q^{\cps}) \Rightarrow
+P^{\cps}).\, \lambda(k:\mathop{\sim}P^\diamond).\,
+g(\lambda(v:P^\diamond).\, \lambda(k_0:\mathop{\sim}Q^\diamond).\,
+kv)\,k)$, de type $(((P\Rightarrow Q)\Rightarrow P)\Rightarrow
+P)^{\cps}$.
 
 \par}
 
@@ -3703,8 +3792,8 @@ l'ordre.
 \medskip
 
 \itempoint Le CPS donne le call/cc « pour rien ».  En fait, en style
-CPS, chaque fonction a un contrôle complet sur l'exécution de tout le
-programme (puisqu'il n'y a plus de pile !).
+CPS, chaque fonction a contrôle complet sur l'exécution de tout le
+programme (il n'y a plus de pile !).
 
 \medskip
 
@@ -3723,8 +3812,8 @@ notamment les promesses de JavaScript, et la monade
 \frametitle{Continuation Passing Style : remarques logiques}
 
 \itempoint Par la transformation $t \mapsto t^{\cps}$ et le fait
-d'avoir trouvé un terme de type $(P\lor\neg P)^{\cps}$, on a montré
-que :
+d'avoir trouvé un terme de type $(((P\Rightarrow Q)\Rightarrow
+P)\Rightarrow P)^{\cps}$, on a montré que :
 \[
 \text{si~}\mathsf{CPC} \vdash P\text{~alors~}\mathsf{IPC} \vdash P^{\cps}
 \]
@@ -3735,7 +3824,7 @@ prouvable en logique classique ».
 \medskip
 
 \itempoint \alert{Si on prend $Z := \bot$}, la proposition $P^{\cps}$
-ajoute simplement des $\neg\neg$ un peu partout, ce qui ne change rien
+ajoute simplement des $\neg\neg$ un peu partout, ce qui est équivalent
 en logique classique, donc on a évidemment
 \[
 \mathsf{CPC} \vdash P\text{~ssi~}\mathsf{CPC} \vdash P^{\cps}
@@ -3754,8 +3843,9 @@ traduction « double négation ».
 {\footnotesize
 
 \itempoint En fait, on peut se contenter de mettre un $\neg\neg$
-devant les disjonctions, ou même (en calcul \alert{propositionnel} !)
-d'en mettre un seul devant toute la formule.
+devant les disjonctions et formules atomiques (traduction de
+Gödel-Gentzen), ou bien (en calcul \alert{propositionnel} !)  d'en
+mettre un seul devant toute la formule (traduction de Glivenko).
 
 \par}