diff options
| -rw-r--r-- | exercices-inf110.tex | 42 |
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} + + % % % |