diff options
| -rw-r--r-- | transp-inf110-02-typage.tex | 16 |
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} |