Many remarks on continuation-passing-style.

1 files changed, 86 insertions, 1 deletions

diff --git a/transp-inf110-02-typage.tex b/transp-inf110-02-typage.tex
index 6f993fa..b60778b 100644
--- a/transp-inf110-02-typage.tex
+++ b/transp-inf110-02-typage.tex
@@ -3275,6 +3275,12 @@ $f$, l'invoquer revient à terminer le fil actuel et réactiver le fil
 en attente, avec en lui transmettant $v$ : il va de nouveau créer un
 fil en attente, puis considérer $v$ comme valeur de retour de $f$.
 
+\medskip
+
+\itempoint Fondement théorique : le $\lambda\mu$-calcul de Parigot
+(exten\textsuperscript{ion} du $\lambda$-calcul avec
+continuations).
+
 \par}
 
 \end{frame}
@@ -3649,7 +3655,86 @@ $\mathop{\sim}A := (A\Rightarrow Z)$) :
 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}$.
+facilement $(P\lor\neg P)^{\cps}$ (ceci donne par exemple le call/cc).
+
+\par}
+
+\end{frame}
+%
+\begin{frame}
+\frametitle{Continuation Passing Style : remarques informatiques}
+
+\itempoint Programmer en CPS fait disparaître l'utilisation de la
+pile : \alert{tous} les appels de fonctions deviennent terminaux, donc
+seront remplacés par des sauts dans un langage supportant la récursion
+terminale propre.
+
+\medskip
+
+\itempoint La conversion vers CPS impose de préciser complètement
+l'ordre d'évaluation.  Par exemple, on a défini $\langle
+x,y\rangle^{\cps} = \lambda k.\, x^{\cps}(\lambda x_0.\, y^{\cps}
+(\lambda y_0.\, k\langle x_0,y_0\rangle))$ qui évalue $x$ avant $y$,
+mais on pouvait aussi $\lambda k.\, y^{\cps} (\lambda y_0.\,
+x^{\cps}(\lambda x_0.\, k\langle x_0,y_0\rangle))$ pour inverser
+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 !).
+
+\medskip
+
+\itempoint Ceci peut servir de point de départ pour la compilation
+(Appel, \textit{Compiling with Continuations}, 1992).
+
+\medskip
+
+\itempoint Utile pour séquencer explicitement les évaluations.  Voir
+notamment les promesses de JavaScript, et la monade
+\texttt{Control.Monad.Cont} de Haskell.
+
+\end{frame}
+%
+\begin{frame}
+\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 :
+\[
+\text{si~}\mathsf{CPC} \vdash P\text{~alors~}\mathsf{IPC} \vdash P^{\cps}
+\]
+où « $\mathsf{IPC} \vdash P$ » signifie « $P$ est prouvable en logique
+intuitionniste » et « $\mathsf{CPC} \vdash P$ » signifie « $P$ est
+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
+en logique classique, donc on a évidemment
+\[
+\mathsf{CPC} \vdash P\text{~ssi~}\mathsf{CPC} \vdash P^{\cps}
+\]
+Comme par ailleurs $\mathsf{CPC} \vdash Q$ implique $\mathsf{IPC} \vdash
+Q$, on déduit des deux affirmations ci-dessus que (pour $Z=\bot$) :
+\[
+\mathsf{CPC} \vdash P\text{~\alert{ssi}~}\mathsf{IPC} \vdash P^{\cps}
+\]
+On dit qu'on a « \alert{interprété} » la logique (propositionnelle)
+classique en logique (propositionnelle) intuitionniste par la
+traduction « double négation ».
+
+\smallskip
+
+{\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.
 
 \par}