From 250a143e0c24361e910d56871427e966ff47a54c Mon Sep 17 00:00:00 2001
From: "David A. Madore" <david+git@madore.org>
Date: Wed, 13 Dec 2023 13:45:41 +0100
Subject: Systematization of continuation-passing-style.

---
 transp-inf110-02-typage.tex | 85 +++++++++++++++++++++++++++++++++++++++++++++
 1 file changed, 85 insertions(+)

(limited to 'transp-inf110-02-typage.tex')

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}
@@ -3525,6 +3526,90 @@ callcc\_cps (fun kf -> fun k -> kf 42 (fun v -> sum\_cps v 1 k)) (fun x -> x) ;;
 {\color{purple}- : int = 42}
 \par}
 
+\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:
-- 
cgit v1.2.3