summaryrefslogtreecommitdiffstats
diff options
context:
space:
mode:
authorDavid A. Madore <david+git@madore.org>2023-12-14 13:02:08 +0100
committerDavid A. Madore <david+git@madore.org>2023-12-14 13:02:08 +0100
commit8658f79341e546996382a31223091db753f9fab0 (patch)
tree18b085730a0089245bd68111101dceeb89ec52b5
parent9cc1ae80001a8cdfe61112942615ea7aa6f901b2 (diff)
downloadinf110-lfi-8658f79341e546996382a31223091db753f9fab0.tar.gz
inf110-lfi-8658f79341e546996382a31223091db753f9fab0.tar.bz2
inf110-lfi-8658f79341e546996382a31223091db753f9fab0.zip
More remarks about CPS.
-rw-r--r--transp-inf110-02-typage.tex56
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}
%