More remarks about CPS.

1 files changed, 45 insertions, 11 deletions

diff --git a/transp-inf110-02-typage.tex b/transp-inf110-02-typage.tex
index 380d40d..eacec62 100644
--- a/transp-inf110-02-typage.tex
+++ b/transp-inf110-02-typage.tex
@@ -3781,30 +3781,64 @@ 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.
+\itempoint La conversion vers CPS fixe l'ordre d'évaluation des
+valeurs.  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
 
+{\footnotesize
+
+\itempoint La conversion vers CPS fixe même une stratégie
+d'évaluation : on a choisi « call-by-value » ici, mais on aurait pu
+prendre « call-by-name » :
+
+\begin{tabular}{c|c}
+« call-by-value »&« call-by-name »\\\hline
+$v^{\cps} = \lambda k.kv$&$v^{\cps} = \lambda k.vk$ (ou juste $v$)\\
+&mais pour une \emph{valeur} : $x^{\cps} = \lambda k.kx$\\
+$(\lambda v.t)^{\cps} = \lambda k.\, k(\lambda v.\, t^{\cps})$
+&$(\lambda v.t)^{\cps} = \lambda k.\, k(\lambda v.\, t^{\cps})$\\
+$(fx)^{\cps} = \lambda
+  k.\,f^{\cps}(\lambda f_0.\, x^{\cps}(\lambda x_0.\, f_0 x_0 k))$
+&$(fx)^{\cps} = \lambda
+  k.\,f^{\cps}(\lambda f_0.\, f_0 x^{\cps} k)$\\
+$(P\Rightarrow Q)^\diamond = (P^\diamond\Rightarrow \mathop{\sim}\mathop{\sim}Q^\diamond)$
+&$(P\Rightarrow Q)^\diamond = (\mathop{\sim}\mathop{\sim}P^\diamond\Rightarrow \mathop{\sim}\mathop{\sim}Q^\diamond)$
+\end{tabular}
+
+\par}
+
+\end{frame}
+%
+\begin{frame}
+\frametitle{Continuation Passing Style : remarques informatiques (suite)}
+
 \itempoint Le CPS donne le call/cc « pour rien ».  En fait, en style
 CPS, chaque fonction a contrôle complet sur l'exécution de tout le
 programme (il n'y a plus de pile !).
 
 \medskip
 
-\itempoint Ceci peut servir de point de départ pour la compilation
+\itempoint Le CPS 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.
+\itempoint On peut concevoir un langage où chaque fonction a
+p.ex. \alert{deux} continuations : une « continuation de succès » et
+une « continuation d'échec », qu'on chaîne avec des opérateurs « et »
+et « ou » : c'est essentiellement le Prolog (où ces opérateurs sont
+notés ‘\texttt{,}’ et ‘\texttt{;}’).
+
+\medskip
+
+\itempoint Le CPS est utile pour séquencer explicit\textsuperscript{t}
+les évaluations.  Voir notamment les promesses de JavaScript, et la
+monade \texttt{Control.Monad.Cont} de Haskell.
 
 \end{frame}
 %