From 1e96977f087cde0421cef6466e08540ac562b2dd Mon Sep 17 00:00:00 2001
From: "David A. Madore" <david+git@madore.org>
Date: Sat, 16 Dec 2023 18:15:02 +0100
Subject: Summarize properties of Hindley-Milner.

---
 transp-inf110-02-typage.tex | 46 +++++++++++++++++++++++++++++++++++++++++++++
 1 file changed, 46 insertions(+)

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
@@ -4943,6 +4943,52 @@ Finalement, on a typé : $\vdash (\lambda (x:\eta_3 \to \eta_4 \to
 (x':\eta_3).\,\lambda(y':\eta_4).\,x') \; : \penalty-1000\; \eta_2 \to
 \eta_3 \to \eta_4 \to \eta_3$.
 
+\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}
-- 
cgit v1.2.3