diff options
| -rw-r--r-- | transp-inf110-02-typage.tex | 180 |
1 files changed, 135 insertions, 45 deletions
diff --git a/transp-inf110-02-typage.tex b/transp-inf110-02-typage.tex index 3d44a81..380d40d 100644 --- a/transp-inf110-02-typage.tex +++ b/transp-inf110-02-typage.tex @@ -3583,7 +3583,7 @@ 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} +\frametitle{Continuation Passing Style : systématisation} \textcolor{blue}{Définissons la transformation CPS de façon systématique.} @@ -3593,11 +3593,85 @@ callcc\_cps (fun kf -> fun k -> kf 42 (fun v -> sum\_cps v 1 k)) (fun x -> x) ;; {\footnotesize Prenons ici les notations logiques pour les types : notamment, $\Rightarrow$ désigne le type fonction.\par} +\medskip + +\itempoint Fixons un type $Z$ de « retour ultime ». On pose +\alert{$\mathop{\sim}P := (P\Rightarrow Z)$} pour le type d'« une +continuation qui attend une valeur de type $P$ » et +$\mathop{\sim}\mathop{\sim}P$ pour « une valeur $P$ passée par +continuation ». + +\medskip + +\itempoint Noter que $x:P \;\vdash\; \lambda(k:\mathop{\sim}P).kx : +\mathop{\sim}\mathop{\sim}P$ (transformation d'une valeur « directe » +en valeur passée par continuation). + +\medskip + +{\footnotesize On si on préfère voir ça comme une fonction : + $\lambda(x:P).\,\lambda(k:\mathop{\sim}P).\,kx$ a pour type $P + \Rightarrow \mathop{\sim}\mathop{\sim}P$.\par} + +\medskip + +\itempoint On va passer \alert{toutes} les valeurs par continuation : +tous les types transformés prendront la forme +$\mathop{\sim}\mathop{\sim}T$. + \smallskip -\itempoint Fixons un type $Z$ de « retour ultime ». On définit une -transformation $P \mapsto P^\diamond$ des types (=propositions) en posant -$\mathop{\sim}P := (P\Rightarrow Z)$, puis (inductivement) : +Mais en plus de ça, les fonctions renvoient leur valeur par +continuation : une fonction de type $P \Rightarrow Q$ va devenir $P +\Rightarrow \mathop{\sim}Q \Rightarrow Z$, c'est-à-dire $P \Rightarrow +\mathop{\sim}\mathop{\sim}Q$, et sera elle-même passée par +continuation, donc $\mathop{\sim}\mathop{\sim}(P \Rightarrow +\mathop{\sim}\mathop{\sim}Q)$ {\footnotesize (sans compter que $P$ et + $Q$ peuvent eux-mêmes changer)}. + +\end{frame} +% +\begin{frame} +\frametitle{Continuation Passing Style : l'essence de la transformation} + +\itempoint Définissons la transformation CPS d'abord dans le +$\lambda$-calcul \alert{non typé} : par induction sur la complexité du +terme : +\begin{itemize} +\item $v^{\cps} = \lambda k.kv$ si $v$ est une variable (c'est la + transformation de $P$ en $\mathop{\sim}\mathop{\sim}P$ définie + ci-dessus). +\item $(\lambda v.t)^{\cps} = \lambda k.\, k(\lambda v.\, t^{\cps})$ + (idem pour une fonction, dont le corps est CPS-ifié). +\item pour l'application : \[(fx)^{\cps} = \lambda + k.\,f^{\cps}(\lambda f_0.\, x^{\cps}(\lambda x_0.\, f_0 x_0 k))\] ce + code se comprend ainsi : on invoque $f^{\cps}$ pour recevoir sa + valeur « directe » $f_0$ (qui est quand même une fonction dans le + style CPS), puis $x^{\cps}$ pour recevoir sa valeur « directe » + $x_0$, puis on appelle la fonction $f_0$ avec la valeur $x_0$ et la + continuation $k$ de l'ensemble de l'expression, +\item $\texttt{callcc}^{\cps} = \lambda \ell.\, \ell(\lambda g.\, + \lambda k.\, g(\lambda v.\, \lambda k_0.\, kv)\,k)$ +\end{itemize} + +\medskip + +\itempoint Ce code \alert{porte les graines d'un interpréteur} +(eval/apply) du $\lambda$-calcul dans le $\lambda$-calcul : il impose +d'ailleurs l'évaluation en appel-par-valeurs. + +\end{frame} +% +\begin{frame} +\frametitle{Continuation Passing Style : transformation des types} + +{\footnotesize Il reste à typer tout ça !\par} + +\smallskip + +\itempoint Rappelons qu'on a fixé $Z$ et posé $\mathop{\sim}P := +(P\Rightarrow Z)$. On définit une transformation $P \mapsto +P^\diamond$ des types (=propositions) par (inductivement) : \begin{itemize} \item $A^\diamond = A$ si $A$ est une variable de type, \item $(P\Rightarrow Q)^\diamond = (P^\diamond \Rightarrow \mathop{\sim}\mathop{\sim}Q^\diamond)$, @@ -3609,25 +3683,27 @@ $\mathop{\sim}P := (P\Rightarrow Z)$, puis (inductivement) : \smallskip -\itempoint Il faut comprendre $\mathop{\sim}P$ comme « une -continuation qui attend un type $P$ » et $\mathop{\sim}\mathop{\sim}P$ -comme « une valeur $P$ passée par continuation ». - -\smallskip - -\itempoint Noter que $x:P \;\vdash\; \lambda(k:\mathop{\sim}P).kx : -\mathop{\sim}\mathop{\sim}P$ (transformation d'une valeur « directe » -en valeur passée par continuation). +\itempoint On pose enfin $P^{\cps} := +\mathop{\sim}\mathop{\sim}P^\diamond$ {\footnotesize (comprendre : + $\mathop{\sim}\mathop{\sim}(P^\diamond)$)}. \smallskip -{\footnotesize On si on préfère voir ça comme une fonction : - $\lambda(x:P).\,\lambda(k:\mathop{\sim}P).\,kx$ a pour type $P - \Rightarrow \mathop{\sim}\mathop{\sim}P$.\par} +En gros : +\begin{itemize} +\item $P^\diamond$ est le type $P$ dans lequel toutes les fonctions + ont été réécrites en style CPS (= renvoient leurs valeurs par + continuation), +\item $P^{\cps} := \mathop{\sim}\mathop{\sim}P^\diamond$ est le type + en question lui-même passé par continuation. +\end{itemize} \smallskip -\itempoint On pose $P^{\cps} := \mathop{\sim}\mathop{\sim}P^\diamond$. +{\footnotesize \itempoint Noter : $(P\Rightarrow Q)^{\cps} = + \mathop{\sim}\mathop{\sim}(P^\diamond \Rightarrow + \mathop{\sim}\mathop{\sim}Q^\diamond) = + \mathop{\sim}\mathop{\sim}(P^\diamond \Rightarrow Q^{\cps})$.} %% {\footnotesize %% @@ -3652,31 +3728,44 @@ $\vdash t:P$ alors $\vdash t^{\cps}:P^{\cps}$ (rappel : $\mathop{\sim}P := (P\Rightarrow Z)$ et $P^{\cps} := \mathop{\sim}\mathop{\sim}P^\diamond$) : \begin{itemize} -\item $v^{\cps} = \lambda k.kv$ si $v$ est une variable -\item $(fx)^{\cps} = \lambda k.\,f^{\cps}(\lambda f_0.\, - x^{\cps}(\lambda x_0.\, f_0 x_0 k))$ -\item $(\lambda v.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))$ -\item $(\pi_i z)^{\cps} = \lambda k.\, z^{\cps}(\lambda z_0.\, k(\pi_i - z_0))$ (pour $i\in\{1,2\}$) -\item $(\iota_i z)^{\cps} = \lambda k.\, z^{\cps}(\lambda z_0.\, - k(\iota_i z_0))$ (pour $i\in\{1,2\}$) +\item $v^{\cps} = \lambda(k:\mathop{\sim}P^\diamond).\,kv$ lorsque $v$ + est une variable de type $P$, +\item $(fx)^{\cps} = \lambda (k:\mathop{\sim}Q^\diamond).\, + f^{\cps}(\lambda (f_0:P^\diamond\Rightarrow Q^{\cps}).\, + x^{\cps}(\lambda (x_0:P^\diamond).\, f_0 x_0 k))$ lorsque $f : + P\Rightarrow Q$ et $x : Q$ (rappel : $(P\Rightarrow Q)^{\cps} = + \mathop{\sim}\mathop{\sim}(P^\diamond \Rightarrow Q^{\cps})$), +\item $(\lambda (v:P).t)^{\cps} = \lambda k.\, k(\lambda + (v:P^\diamond).\, t^{\cps})$ lorsque $\Gamma, v:P \vdash t:Q$, +\item $\langle x,y\rangle^{\cps} = \lambda + (k:\mathop{\sim}(Q_1^\diamond \land Q_2^\diamond)).\, + x^{\cps}(\lambda (x_0:Q_1^\diamond).\, y^{\cps} (\lambda + (y_0:Q_2^\diamond).\, k\langle x_0,y_0\rangle))$, +\item $(\pi_i z)^{\cps} = \lambda (k:\mathop{\sim} Q_i^\diamond).\, + z^{\cps}(\lambda (z_0:Q_1^\diamond\land Q_2^\diamond).\, k(\pi_i + z_0))$ (pour $i\in\{1,2\}$), +\item $(\iota^{(Q_1,Q_2)}_i z)^{\cps} = \lambda + (k:\mathop{\sim}(Q_1^\diamond\lor Q_2^\diamond)).\, z^{\cps}(\lambda + (z_0:Q_i^\diamond).\, k(\iota^{(Q_1^\diamond,Q_2^\diamond)}_i z_0))$ + (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 + \iota_2 v_2 \mapsto t_2)^{\cps} = \lambda + (k:\mathop{\sim}Q^\diamond).\, r^{\cps}(\lambda + (r_0:P_1^\diamond\lor P_2^\diamond).\penalty0\, + (\texttt{match}\penalty500\ 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))$ +\item $\bullet^{\cps} = \lambda (k:\mathop{\sim}\top).k{\bullet}$ +\item $(\texttt{exfalso}^{(Q)} r)^{\cps} = \lambda + (k:\mathop{\sim}Q^\diamond).\, r^{\cps}(\lambda (r_0:\bot).\, + (\texttt{exfalso}^{(Q^\diamond)} 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}$ (ceci donne par exemple le call/cc). +\itempoint $\texttt{callcc}^{\cps} = \lambda (\ell:\cdots).\, +\ell(\lambda (g : (P^\diamond \Rightarrow Q^{\cps}) \Rightarrow +P^{\cps}).\, \lambda(k:\mathop{\sim}P^\diamond).\, +g(\lambda(v:P^\diamond).\, \lambda(k_0:\mathop{\sim}Q^\diamond).\, +kv)\,k)$, de type $(((P\Rightarrow Q)\Rightarrow P)\Rightarrow +P)^{\cps}$. \par} @@ -3703,8 +3792,8 @@ 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 !). +CPS, chaque fonction a contrôle complet sur l'exécution de tout le +programme (il n'y a plus de pile !). \medskip @@ -3723,8 +3812,8 @@ notamment les promesses de JavaScript, et la monade \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 : +d'avoir trouvé un terme de type $(((P\Rightarrow Q)\Rightarrow +P)\Rightarrow P)^{\cps}$, on a montré que : \[ \text{si~}\mathsf{CPC} \vdash P\text{~alors~}\mathsf{IPC} \vdash P^{\cps} \] @@ -3735,7 +3824,7 @@ 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 +ajoute simplement des $\neg\neg$ un peu partout, ce qui est équivalent en logique classique, donc on a évidemment \[ \mathsf{CPC} \vdash P\text{~ssi~}\mathsf{CPC} \vdash P^{\cps} @@ -3754,8 +3843,9 @@ traduction « double négation ». {\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. +devant les disjonctions et formules atomiques (traduction de +Gödel-Gentzen), ou bien (en calcul \alert{propositionnel} !) d'en +mettre un seul devant toute la formule (traduction de Glivenko). \par} |