diff options
| -rw-r--r-- | transp-inf110-02-typage.tex | 85 |
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 |