summaryrefslogtreecommitdiffstats
diff options
context:
space:
mode:
authorDavid A. Madore <david+git@madore.org>2023-12-14 11:50:48 +0100
committerDavid A. Madore <david+git@madore.org>2023-12-14 11:50:48 +0100
commit9cc1ae80001a8cdfe61112942615ea7aa6f901b2 (patch)
tree8a36a807b5eb57c1d739b28e1f1988f5211f3905
parentfa6269a195752adf2a4a1adfd9240401ef1e87ba (diff)
downloadinf110-lfi-9cc1ae80001a8cdfe61112942615ea7aa6f901b2.tar.gz
inf110-lfi-9cc1ae80001a8cdfe61112942615ea7aa6f901b2.tar.bz2
inf110-lfi-9cc1ae80001a8cdfe61112942615ea7aa6f901b2.zip
Hopefully unfsck the whole situation with CPS translation and typing.
-rw-r--r--transp-inf110-02-typage.tex180
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}