diff options
| -rw-r--r-- | exercices-inf110.tex | 105 |
1 files changed, 105 insertions, 0 deletions
diff --git a/exercices-inf110.tex b/exercices-inf110.tex index 0539356..af9a1a7 100644 --- a/exercices-inf110.tex +++ b/exercices-inf110.tex @@ -2591,6 +2591,111 @@ on ne peut pas prouver $\neg C$ seul, ni $\neg\neg C$ seul, qui peut prendre l'une ou l'autre valeur de vérité). \end{corrige} +% + +\exercice\ (${\star}{\star}$)\par\nobreak + +En appliquant l'algorithme de Hindley-Milner, trouver une annotation +de type (dans le $\lambda$-calcul simplement typé) au terme suivant du +$\lambda$-calcul non typé : +\[ +\lambda k. \, k\,(k\,(\lambda x.x)\,(\lambda y.y)) +\] +(autrement dit, \texttt{fun k -> k (k (fun x -> x) (fun y -> y))} en +syntaxe OCaml). + +\begin{corrige} +On prend bien garde au fait qu'il faut parenthéser comme $\lambda +k. \, k\,((k\,(\lambda x.x))\,(\lambda y.y))$. + +Dans une première phase, on collecte les types et contraintes +suivants : $k:\eta_1$, $x:\eta_2$ donc $\lambda x.x:\eta_2\to\eta_2$, +puis $k(\lambda x.x):\eta_3$ avec $\eta_1 = +((\eta_2\to\eta_2)\to\eta_3)$, puis $y:\eta_4$ donc $\lambda +y.y:\eta_4\to\eta_4$, puis $k(\lambda x.x)(\lambda y.y):\eta_5$ avec +$\eta_3 = ((\eta_4\to\eta_4)\to\eta_5)$, puis $k(k(\lambda +x.x)(\lambda y.y)) : \eta_6$ avec $\eta_1 = (\eta_5\to\eta_6)$ ; et le +type final est $\eta_1 \to \eta_6$. On a donc les contraintes +suivantes : +\[ +\begin{aligned} +\eta_1 &= ((\eta_2\to\eta_2)\to\eta_3)\\ +\eta_3 &= ((\eta_4\to\eta_4)\to\eta_5)\\ +\eta_1 &= (\eta_5\to\eta_6)\\ +\end{aligned} +\] +On examine d'abord la contrainte $\eta_1 = +((\eta_2\to\eta_2)\to\eta_3)$ : ici, $\eta_1$ est une variable de +type, et elle n'apparaît pas dans l'autre membre de la contrainte ; il +n'y a rien à faire à part enregistrer $\eta_1 \mapsto +((\eta_2\to\eta_2)\to\eta_3)$ dans la substitution et l'appliquer aux +contraintes qui deviennent donc : +\[ +\begin{aligned} +\eta_3 &= ((\eta_4\to\eta_4)\to\eta_5)\\ +((\eta_2\to\eta_2)\to\eta_3) &= (\eta_5\to\eta_6)\\ +\end{aligned} +\] +On examine ensuite la contrainte $\eta_3 = +((\eta_4\to\eta_4)\to\eta_5)$ : de nouveau, $\eta_3$ est une variable +de type, et elle n'apparaît pas dans l'autre membre de la contrainte : +on enregistre $\eta_3 \mapsto ((\eta_4\to\eta_4)\to\eta_5)$ et on +l'applique à la substitution déjà enregistrée qui devient donc $\eta_1 +\mapsto ((\eta_2\to\eta_2)\to(\eta_4\to\eta_4)\to\eta_5)$, ainsi qu'à +la contrainte restante. Cette dernière contrainte à examiner est : +\[ +((\eta_2\to\eta_2)\to(\eta_4\to\eta_4)\to\eta_5) = (\eta_5\to\eta_6) +\] +Cette fois-ci les deux membres sont des types complexes, donc elle se +transforme en deux contraintes (attention au parenthésage !) : +\[ +\begin{aligned} +(\eta_2\to\eta_2) &= \eta_5\\ +((\eta_4\to\eta_4)\to\eta_5) &= \eta_6\\ +\end{aligned} +\] +On examine à présent $(\eta_2\to\eta_2) = \eta_5$ : ici, $\eta_5$ est +une variable de type, et elle n'apparaît pas dans l'autre membre de la +contrainte : on enregistre $\eta_5 \mapsto (\eta_2\to\eta_2)$, et on +applique cette substitution à ce qui reste de contrainte (qui devient +donc $((\eta_4\to\eta_4)\to\eta_2\to\eta_2) = \eta_6$) et à ce qu'on a +déjà déterminé comme substitution (qui devient donc $\eta_1 \mapsto +((\eta_2\to\eta_2)\to(\eta_4\to\eta_4)\to\eta_2\to\eta_2)$ et $\eta_3 +\mapsto ((\eta_4\to\eta_4)\to\eta_2\to\eta_2)$). Il reste enfin la +contrainte $((\eta_4\to\eta_4)\to\eta_2\to\eta_2) = \eta_6$ : de +nouveau, $\eta_6$ est une variable de type, et elle n'apparaît pas +dans l'autre membre de la contrainte : on enregistre donc $\eta_6 +\mapsto ((\eta_4\to\eta_4)\to\eta_2\to\eta_2)$, et on a trouvé la +substitution finale : +\[ +\begin{aligned} +\eta_1 &\mapsto ((\eta_2\to\eta_2)\to(\eta_4\to\eta_4)\to\eta_2\to\eta_2)\\ +\eta_3 &\mapsto ((\eta_4\to\eta_4)\to\eta_2\to\eta_2)\\ +\eta_5 &\mapsto (\eta_2\to\eta_2)\\ +\eta_6 &\mapsto ((\eta_4\to\eta_4)\to\eta_2\to\eta_2)\\ +\end{aligned} +\] +Il ne reste plus qu'à l'appliquer à tous les types intermédiaires et +au type final, ce qui donne +\[ +\begin{aligned} +&\lambda (k:(\eta_2\to\eta_2)\to(\eta_4\to\eta_4)\to\eta_2\to\eta_2). \, k\,(k\,(\lambda (x:\eta_2).x)\,(\lambda (y:\eta_4).y))\\ +:\quad& ((\eta_2\to\eta_2)\to(\eta_4\to\eta_4)\to\eta_2\to\eta_2) +\to (\eta_4\to\eta_4)\to\eta_2\to\eta_2 +\end{aligned} +\] +ou, si on veut renommer les variables restantes pour être un peu plus +lisible +\[ +\begin{aligned} +&\lambda (k:(\alpha\to\alpha)\to(\beta\to\beta)\to\alpha\to\alpha). \, k\,(k\,(\lambda (x:\alpha).x)\,(\lambda (y:\beta).y))\\ +:\quad& ((\alpha\to\alpha)\to(\beta\to\beta)\to\alpha\to\alpha) +\to (\beta\to\beta)\to\alpha\to\alpha +\end{aligned} +\] +comme $\lambda$-terme annoté et comme type final. +\end{corrige} + % % |