summaryrefslogtreecommitdiffstats
diff options
context:
space:
mode:
authorDavid A. Madore <david+git@madore.org>2023-12-13 13:54:45 +0100
committerDavid A. Madore <david+git@madore.org>2023-12-13 13:54:45 +0100
commit5fd56f4040d6cee45ca87600fa73f5efbce17b2b (patch)
treeeac5f849504f3e4d3f2907b290ad8883390513a6
parent250a143e0c24361e910d56871427e966ff47a54c (diff)
downloadinf110-lfi-5fd56f4040d6cee45ca87600fa73f5efbce17b2b.tar.gz
inf110-lfi-5fd56f4040d6cee45ca87600fa73f5efbce17b2b.tar.bz2
inf110-lfi-5fd56f4040d6cee45ca87600fa73f5efbce17b2b.zip
Additional remark.
-rw-r--r--transp-inf110-02-typage.tex16
1 files changed, 14 insertions, 2 deletions
diff --git a/transp-inf110-02-typage.tex b/transp-inf110-02-typage.tex
index 60705f6..3ded562 100644
--- a/transp-inf110-02-typage.tex
+++ b/transp-inf110-02-typage.tex
@@ -3552,18 +3552,30 @@ $\mathop{\sim}A := (A\Rightarrow Z)$, puis (inductivement) :
\quad\itempoint $\bot^{\cps} = \mathop{\sim}\mathop{\sim}\bot$.
\end{itemize}
-\medskip
+\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 ».
-\medskip
+\smallskip
\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).
+\smallskip
+
+{\footnotesize
+
+\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}$.
+
+\par}
+
\end{frame}
%
\begin{frame}