diff options
| -rw-r--r-- | transp-inf110-02-typage.tex | 74 |
1 files changed, 39 insertions, 35 deletions
diff --git a/transp-inf110-02-typage.tex b/transp-inf110-02-typage.tex index 25305e4..3d44a81 100644 --- a/transp-inf110-02-typage.tex +++ b/transp-inf110-02-typage.tex @@ -3590,45 +3590,54 @@ callcc\_cps (fun kf -> fun k -> kf 42 (fun v -> sum\_cps v 1 k)) (fun x -> x) ;; \medskip -{\footnotesize Prenons les notations logiques pour les types.\par} +{\footnotesize Prenons ici les notations logiques pour les types : + notamment, $\Rightarrow$ désigne le type fonction.\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) : +transformation $P \mapsto P^\diamond$ des types (=propositions) en posant +$\mathop{\sim}P := (P\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$. +\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)$, +\item $(P\land Q)^\diamond = P^\diamond \land Q^\diamond$, +\quad\itempoint $(P\lor Q)^\diamond = P^\diamond \lor Q^\diamond$, +\item $\top^\diamond = \top$, +\quad\itempoint $\bot^\diamond = \bot$. \end{itemize} \smallskip -\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 ». +\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:A \;\vdash\; \lambda(k:\mathop{\sim}A).kx : -\mathop{\sim}\mathop{\sim}A$ (transformation d'une valeur « directe » +\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). \smallskip -{\footnotesize +{\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} + +\smallskip -\itempoint On vérifie : $\mathop{\sim} A \Leftrightarrow -\mathop{\sim}\mathop{\sim}\mathop{\sim} A$, donc $P^{\cps} -\Leftrightarrow \mathop{\sim}\mathop{\sim} P^{\cps}$ ; remarquer -aussi : $\bot^{\cps} \Leftrightarrow Z$ et $(\neg P)^{\cps} -\Leftrightarrow \mathop{\sim} P^{\cps}$. +\itempoint On pose $P^{\cps} := \mathop{\sim}\mathop{\sim}P^\diamond$. -\par} +%% {\footnotesize +%% +%% \itempoint On vérifie : $\mathop{\sim} P \Leftrightarrow +%% \mathop{\sim}\mathop{\sim}\mathop{\sim} P$, donc $P^{\cps} +%% \Leftrightarrow \mathop{\sim}\mathop{\sim} P^{\cps}$ ; remarquer +%% aussi : $\bot^{\cps} \Leftrightarrow Z$ et $(\neg P)^{\cps} +%% \Leftrightarrow \mathop{\sim} P^{\cps}$. +%% +%% \par} \end{frame} % @@ -3640,25 +3649,20 @@ aussi : $\bot^{\cps} \Leftrightarrow Z$ et $(\neg P)^{\cps} \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)$) : +$\mathop{\sim}P := (P\Rightarrow Z)$ et $P^{\cps} := +\mathop{\sim}\mathop{\sim}P^\diamond$) : \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} = +\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))$ (abrégé) + 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))$ (abrégé, pour $i\in\{1,2\}$) + z_0))$ (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\}$) + k(\iota_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 |