summaryrefslogtreecommitdiffstats
diff options
context:
space:
mode:
authorDavid A. Madore <david+git@madore.org>2023-12-13 13:45:41 +0100
committerDavid A. Madore <david+git@madore.org>2023-12-13 13:45:41 +0100
commit250a143e0c24361e910d56871427e966ff47a54c (patch)
tree6385ed6648c192639dd202c20a3859e68b26122c
parent3264fc74f818d3b92de4d490d59a0ae69edc3944 (diff)
downloadinf110-lfi-250a143e0c24361e910d56871427e966ff47a54c.tar.gz
inf110-lfi-250a143e0c24361e910d56871427e966ff47a54c.tar.bz2
inf110-lfi-250a143e0c24361e910d56871427e966ff47a54c.zip
Systematization of continuation-passing-style.
-rw-r--r--transp-inf110-02-typage.tex85
1 files changed, 85 insertions, 0 deletions
diff --git a/transp-inf110-02-typage.tex b/transp-inf110-02-typage.tex
index 4a033df..60705f6 100644
--- a/transp-inf110-02-typage.tex
+++ b/transp-inf110-02-typage.tex
@@ -31,6 +31,7 @@
\renewcommand{\thefootnote}{\textdagger}
\newcommand{\dbllangle}{\mathopen{\langle\!\langle}}
\newcommand{\dblrangle}{\mathclose{\rangle\!\rangle}}
+\newcommand{\cps}{\mathrm{CPS}}
\mathchardef\emdash="07C\relax
\newcommand{\mpdotsabove}[1]{\inferrule*{\vdots}{#1}}
\setlength{\derivskip}{4pt}
@@ -3527,6 +3528,90 @@ 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}
+
+\textcolor{blue}{Définissons la transformation CPS de façon
+ systématique.}
+
+\medskip
+
+{\footnotesize Prenons les notations logiques pour les types.\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) :
+\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$.
+\end{itemize}
+
+\medskip
+
+\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 ».
+
+\medskip
+
+\itempoint Noter que $x:A \;\vdash\; \lambda(k:\mathop{\sim}A).kx :
+\mathop{\sim}\mathop{\sim}A$ (transformation d'une valeur « directe »
+en valeur passée par continuation).
+
+\end{frame}
+%
+\begin{frame}
+\frametitle{Continuation Passing Style : transformation des termes}
+
+{\footnotesize
+
+\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)$) :
+\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} =
+ \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é)
+\item $(\pi_i z)^{\cps} = \lambda k.\, z^{\cps}(\lambda z_0.\, k(\pi_i
+ z))$ (abrégé, 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\}$)
+\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
+ 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))$
+\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}$.
+
+\par}
+
+\end{frame}
+%
% TODO:
% - Kripke
% - CPS et fragment négatif