An exercise involving call/cc.

1 files changed, 42 insertions, 0 deletions

diff --git a/exercices-inf110.tex b/exercices-inf110.tex
index 14cf4cf..3e988db 100644
--- a/exercices-inf110.tex
+++ b/exercices-inf110.tex
@@ -1814,6 +1814,48 @@ tous les trois équivalents (en logique intuitionniste).
 \end{corrige}
 
 
+\exercice\ (${\star}{\star}{\star}$)\par\nobreak
+
+En utilisant une fonction call/cc (typé comme la loi de Peirce),
+construire un terme de type $(A\land B \Rightarrow C) \Rightarrow
+(A\Rightarrow C) \lor (B\Rightarrow C)$ dont le comportement en tant
+que programme est décrit informellement comme suit : donné $f$ de type
+$A\land B \Rightarrow C$, pour construire une valeur de type
+$(A\Rightarrow C) \lor (B\Rightarrow C)$, on capture une continuation
+(disons $k$) et on renvoie « provisoirement » une fonction
+$A\Rightarrow C$ qui attend un paramètre $x$ de type $A$ et qui, quand
+elle le reçoit, invoque la contination $k$ pour « revenir en arrière
+dans le temps » renvoyer finalement une fonction $B\Rightarrow C$ qui
+prend en entrée $y$ de type $B$ et renvoie $f\langle x,y\rangle$.
+
+\begin{corrige}
+Posons $D := (A\Rightarrow C) \lor (B\Rightarrow C)$ pour abréger les
+notations.
+
+La fonction qu'on va finalement renvoyer une fois capturé le $x$ est
+$\iota_2^{(A\Rightarrow C, B\Rightarrow C)}(\lambda (y:B).\,f\langle
+x,y\rangle)$ (de type $D$) : on va donc invoquer la continuation
+(appelons-la $k$) sur cette valeur.  La fonction provisoirement
+renvoyée est donc $\iota_1^{(A\Rightarrow C, B\Rightarrow C)}(\lambda
+(x:A).\,k(\cdots))$ où les points de suspension sont remplacés par la
+valeur qu'on vient de dire (ce terme est de type $D$ et on voit que la
+continuation fait semblant de renvoyer un type $C$ — sachant qu'en
+fait elle ne renverra jamais rien puisque c'est une continuation).
+
+Il n'y a donc plus qu'à appliquer call/cc de type $((D\Rightarrow
+C)\Rightarrow D)\Rightarrow D$ à tout ça, ce qui donne :
+\[
+\lambda(f:A\land B \Rightarrow C).\;
+\texttt{callcc}~(
+\lambda(k:D \Rightarrow C).\;\iota_1^{(A\Rightarrow C, B\Rightarrow C)}(\lambda
+(x:A).\,k(\iota_2^{(A\Rightarrow C, B\Rightarrow C)}(\lambda (y:B).\,f\langle
+x,y\rangle))))
+\]
+terme de type $(A\land B \Rightarrow C) \Rightarrow D$ (où on rappelle
+$D = (A\Rightarrow C) \lor (B\Rightarrow C)$).
+\end{corrige}
+
+
 %
 %
 %