diff options
| -rw-r--r-- | controle-20240126.tex | 63 |
1 files changed, 63 insertions, 0 deletions
diff --git a/controle-20240126.tex b/controle-20240126.tex index 343c58c..7911a5c 100644 --- a/controle-20240126.tex +++ b/controle-20240126.tex @@ -176,6 +176,69 @@ x. B(x))$, i.e., elle représente une preuve de cette affirmation. \end{corrige} +% +% +% + +\exercice + +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 f.\,\lambda z.\,fz(\lambda g.gz) +\] +(autrement dit, \texttt{fun f -> fun z -> f z (fun g -> g z)} en +syntaxe OCaml). Quel théorème du calcul propositionnel intuitionniste +obtient-on de ceci ? + +\begin{corrige} +Dans une première phase, on collecte les types et contraintes +suivants : $f:\eta_1$, $z:\eta_2$, $fz : \eta_3$ avec $\eta_1 = +(\eta_2\to\eta_3)$, $g : \eta_4$, $g z : \eta_5$ avec $\eta_4 = +(\eta_2\to\eta_5)$ donc $\lambda g.gz : \eta_4\to\eta_5$ et enfin +$fz(\lambda g.gz) : \eta_6$ avec $\eta_3 = +((\eta_4\to\eta_5)\to\eta_6)$ ; et le type final est $\eta_1 \to +\eta_2 \to \eta_6$. On a donc les contraintes suivantes : +\[ +\begin{aligned} +\eta_1 &= (\eta_2\to\eta_3)\\ +\eta_4 &= (\eta_2\to\eta_5)\\ +\eta_3 &= ((\eta_4\to\eta_5)\to\eta_6)\\ +\end{aligned} +\] +On examine d'abord la contrainte $\eta_1 = (\eta_2\to\eta_3)$ : il n'y +a rien à faire à part enregistrer $\eta_1 \mapsto (\eta_2\to\eta_3)$ +dans la substitution. On examine ensuite la contrainte $\eta_4 = +(\eta_2\to\eta_5)$ : on enregistre $\eta_4 \mapsto (\eta_2\to\eta_5)$ +dans la substitution, et on l'applique à la dernière contrainte, qui +devient $\eta_3 = (((\eta_2\to\eta_5)\to\eta_5)\to\eta_6)$. Enfin, on +examine la contrainte $\eta_3 = +(((\eta_2\to\eta_5)\to\eta_5)\to\eta_6)$ : on enregistrer $\eta_3 +\mapsto (((\eta_2\to\eta_5)\to\eta_5)\to\eta_6)$ dans la substitution +et on l'applique à $\eta_1 \mapsto (\eta_2\to\eta_3)$. Finalement, on +a trouvé la substitution : +\[ +\begin{aligned} +\eta_1 &\mapsto (\eta_2\to((\eta_2\to\eta_5)\to\eta_5)\to\eta_6)\\ +\eta_4 &\mapsto (\eta_2\to\eta_5)\\ +\eta_3 &\mapsto (((\eta_2\to\eta_5)\to\eta_5)\to\eta_6)\\ +\end{aligned} +\] +qu'on applique à tous les types intermédiaires et au type final, ce +qui donne +\[ +\begin{aligned} +&\lambda (f:\eta_2\to((\eta_2\to\eta_5)\to\eta_5)\to\eta_6).\,\lambda (z:\eta_2).\,fz(\lambda (g:\eta_2\to\eta_5).gz)\\ +:\quad& (\eta_2\to((\eta_2\to\eta_5)\to\eta_5)\to\eta_6) \to \eta_2 \to \eta_6 +\end{aligned} +\] +En particulier, on voit que $(H_2\Rightarrow((H_2\Rightarrow +H_5)\Rightarrow H_5)\Rightarrow H_6) \Rightarrow H_2 \Rightarrow H_6$ +est un théorème du calcul propositionnel intuitionniste. +\end{corrige} + + % % |