An exercise on Hindley-Milner.

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}
+
+
 
 %
 %