Try to fix CPS transformation, but this is still broken. :-(

1 files changed, 39 insertions, 35 deletions

diff --git a/transp-inf110-02-typage.tex b/transp-inf110-02-typage.tex
index 25305e4..3d44a81 100644
--- a/transp-inf110-02-typage.tex
+++ b/transp-inf110-02-typage.tex
@@ -3590,45 +3590,54 @@ callcc\_cps (fun kf -> fun k -> kf 42 (fun v -> sum\_cps v 1 k)) (fun x -> x) ;;
 
 \medskip
 
-{\footnotesize Prenons les notations logiques pour les types.\par}
+{\footnotesize Prenons ici les notations logiques pour les types :
+  notamment, $\Rightarrow$ désigne le type fonction.\par}
 
 \smallskip
 
 \itempoint Fixons un type $Z$ de « retour ultime ».  On définit une
-traduction $P \mapsto P^{\cps}$ des types (=propositions) en posant
-$\mathop{\sim}A := (A\Rightarrow Z)$, puis (inductivement) :
+transformation $P \mapsto P^\diamond$ des types (=propositions) en posant
+$\mathop{\sim}P := (P\Rightarrow Z)$, puis (inductivement) :
 \begin{itemize}
-\item $A^{\cps} = \mathop{\sim}\mathop{\sim}A$ si $A$ est une variable de type,
-\item $(P\Rightarrow Q)^{\cps} = \mathop{\sim}\mathop{\sim}(P^{\cps} \Rightarrow Q^{\cps})$,
-\item $(P\land Q)^{\cps} = \mathop{\sim}\mathop{\sim}(P^{\cps} \land Q^{\cps})$,
-\item $(P\lor Q)^{\cps} = \mathop{\sim}\mathop{\sim}(P^{\cps} \lor Q^{\cps})$,
-\item $\top^{\cps} = \mathop{\sim}\mathop{\sim}\top$,
-\quad\itempoint $\bot^{\cps} = \mathop{\sim}\mathop{\sim}\bot$.
+\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)$,
+\item $(P\land Q)^\diamond = P^\diamond \land Q^\diamond$,
+\quad\itempoint $(P\lor Q)^\diamond = P^\diamond \lor Q^\diamond$,
+\item $\top^\diamond = \top$,
+\quad\itempoint $\bot^\diamond = \bot$.
 \end{itemize}
 
 \smallskip
 
-\itempoint Il faut comprendre $\mathop{\sim}A$ comme « une
-continuation qui attend un type $A$ » et $\mathop{\sim}\mathop{\sim}A$
-comme « une valeur $A$ passée par continuation ».
+\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:A \;\vdash\; \lambda(k:\mathop{\sim}A).kx :
-\mathop{\sim}\mathop{\sim}A$ (transformation d'une valeur « directe »
+\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).
 
 \smallskip
 
-{\footnotesize
+{\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}
+
+\smallskip
 
-\itempoint On vérifie : $\mathop{\sim} A \Leftrightarrow
-\mathop{\sim}\mathop{\sim}\mathop{\sim} A$, donc $P^{\cps}
-\Leftrightarrow \mathop{\sim}\mathop{\sim} P^{\cps}$ ; remarquer
-aussi : $\bot^{\cps} \Leftrightarrow Z$ et $(\neg P)^{\cps}
-\Leftrightarrow \mathop{\sim} P^{\cps}$.
+\itempoint On pose $P^{\cps} := \mathop{\sim}\mathop{\sim}P^\diamond$.
 
-\par}
+%% {\footnotesize
+%% 
+%% \itempoint On vérifie : $\mathop{\sim} P \Leftrightarrow
+%% \mathop{\sim}\mathop{\sim}\mathop{\sim} P$, donc $P^{\cps}
+%% \Leftrightarrow \mathop{\sim}\mathop{\sim} P^{\cps}$ ; remarquer
+%% aussi : $\bot^{\cps} \Leftrightarrow Z$ et $(\neg P)^{\cps}
+%% \Leftrightarrow \mathop{\sim} P^{\cps}$.
+%% 
+%% \par}
 
 \end{frame}
 %
@@ -3640,25 +3649,20 @@ aussi : $\bot^{\cps} \Leftrightarrow Z$ et $(\neg P)^{\cps}
 \itempoint On définit maintenant la transformation $t \mapsto
 t^{\cps}$ sur les termes du $\lambda$CST de manière à ce que si
 $\vdash t:P$ alors $\vdash t^{\cps}:P^{\cps}$ (rappel :
-$\mathop{\sim}A := (A\Rightarrow Z)$) :
+$\mathop{\sim}P := (P\Rightarrow Z)$ et $P^{\cps} :=
+\mathop{\sim}\mathop{\sim}P^\diamond$) :
 \begin{itemize}
-\item $x^{\cps} = \lambda(k:\mathop{\sim}A).kx$ si $\vdash x : A$
-\item $(fx)^{\cps} =
-  \lambda(k:\mathop{\sim}Q^{\cps}).\,f^{\cps}(\lambda(f_0:P^{\cps}\Rightarrow
-  Q^{\cps}).\, x^{\cps}(\lambda(x_0:P^{\cps}).\, k(f_0 x_0)))$ si
-  $\vdash f : P\Rightarrow Q$ et $\vdash x : P$ ; en abrégé :
-  $(fx)^{\cps} = \lambda k.\,f^{\cps}(\lambda f_0.\, x^{\cps}(\lambda
-  x_0.\,k(f_0 x_0)))$
-\item $(\lambda(v:P).t)^{\cps} =
-  \lambda(k:\mathop{\sim}(P^{\cps}\Rightarrow Q^{\cps})).\, k(\lambda
-  (v:P^{\cps}).\, t^{\cps})$ abrégé $(\lambda(v:P).t)^{\cps} =
+\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))$ (abrégé)
+  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))$ (abrégé, pour $i\in\{1,2\}$)
+  z_0))$ (pour $i\in\{1,2\}$)
 \item $(\iota_i z)^{\cps} = \lambda k.\, z^{\cps}(\lambda z_0.\,
-  k(\iota_i z))$ (abrégé, pour $i\in\{1,2\}$)
+  k(\iota_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