diff options
| -rw-r--r-- | transp-inf110-02-typage.tex | 46 |
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} |