1 files changed, 46 insertions, 0 deletions
diff --git a/transp-inf110-02-typage.tex b/transp-inf110-02-typage.tex
index d27fac7..422ad34 100644
--- a/transp-inf110-02-typage.tex
+++ b/transp-inf110-02-typage.tex
@@ -4945,4 +4945,50 @@ Finalement, on a typé : $\vdash (\lambda (x:\eta_3 \to \eta_4 \to
 
 \end{frame}
 %
+\begin{frame}
+\frametitle{Propriétés de l'algorithme de Hindley-Milner}
+
+La difficulté concerne essentiellement la seconde phase (résolution
+des contraintes par unification).  On peut prouver :
+
+\medskip
+
+\itempoint\textbf{L'algorithme termine} (il est même p.r. et mieux).
+
+\smallskip
+
+{\footnotesize\underline{Idée de la preuve :} double récurrence, sur
+  le nombre de variables de type (récurrence principale) et sur le
+  degré total des formules dans les contraintes.\par}
+
+\medskip
+
+\itempoint\textbf{L'algorithme est correct} : s'il retourne une
+substitution, celle-ci résout les contraintes. {\footnotesize (C'est à
+  peu près évident.)\par}
+
+\medskip
+
+\itempoint (Damas) \textbf{L'algorithme est « complet » :} toute autre
+solution des contraintes $\mathscr{C}$ s'obtient en effectuant une
+substitution sur celle retournée par l'algorithme : on dit qu'il
+trouve la \textbf{solution principale} {\footnotesize (notamment,
+  celle-ci existe !)}.
+
+\smallskip
+
+{\footnotesize\underline{Idée de la preuve :} récurrence sur le nombre
+  d'appels récursifs à la fonction d'unification.\par}
+
+\medskip
+
+\centerline{*}
+
+\itempoint L'algorithme \alert{se généralise sans problème} à l'ajout
+de types produits, sommes, $1$ et $0$ ($\rightarrow$ nvx cas d'échecs
+d'unification, p.ex., si $\zeta_1 = ({?} \rightarrow {?})$ et $\zeta_2
+= ({?} \times {?})$).
+
+\end{frame}
+%
 \end{document}