From 65c7a5fae077f4737be6de653a48f6d4234d32d9 Mon Sep 17 00:00:00 2001
From: "David A. Madore" <david+git@madore.org>
Date: Sat, 16 Dec 2023 17:52:33 +0100
Subject: An example of the full H-M algorithm.

---
 transp-inf110-02-typage.tex | 63 +++++++++++++++++++++++++++++++++++++++++----
 1 file changed, 58 insertions(+), 5 deletions(-)

diff --git a/transp-inf110-02-typage.tex b/transp-inf110-02-typage.tex
index 653b8bb..d27fac7 100644
--- a/transp-inf110-02-typage.tex
+++ b/transp-inf110-02-typage.tex
@@ -4827,35 +4827,54 @@ il renvoie un type et modifie $\Gamma,\mathscr{C}$ :
 {\footnotesize\itempoint Ceci s'adapte sans difficulté au cas où on
   dispose d'annotations de type partielles.\par}
 
+\medskip
+
+\itempoint Le typage final s'obtiendra en appliquant la substitution
+trouvée dans la deuxième phase.
+
 \end{frame}
 %
 \begin{frame}
 \frametitle{Collection des contraintes : exemples}
 
 \itempoint Soit le terme à typer $\lambda xyz.xz(yz)$.  On collecte
-successivement les types et contraintes suivants :\quad
+les types et contraintes suivants :\quad
 $x:\eta_1$,\quad $y:\eta_2$,\quad $z:\eta_3$,\quad $xz:\eta_4$ avec
 $\eta_1 = (\eta_3\to\eta_4)$,\quad $yz:\eta_5$ avec $\eta_2 =
 (\eta_3\to\eta_5)$,\quad $xz(yz):\eta_6$ avec $\eta_4 =
 (\eta_5\to\eta_6)$,\quad et on renvoie finalement le type $\eta_1 \to
 \eta_2 \to \eta_3 \to \eta_6$.
 
-\bigskip
+\medskip
 
 \itempoint Soit le terme à typer $\lambda fx.f(\lambda g.gx)$.  On
-collecte successivement les types et contraintes suivants :\quad
+collecte les types et contraintes suivants :\quad
 $f:\eta_1$,\quad $x:\eta_2$,\quad $g:\eta_3$,\quad $gx:\eta_4$ avec
 $\eta_3 = (\eta_2\to\eta_4)$,\quad $f(\lambda g.gx):\eta_5$ avec
 $\eta_1 = ((\eta_3\to\eta_4) \to \eta_5)$,\quad et on renvoie
 finalement le type $\eta_1 \to \eta_2 \to \eta_5$.
 
-\bigskip
+\medskip
 
 \itempoint Soit le terme à typer $\lambda x.xx$.  On collecte
-successivement les types et contraintes suivants :\quad
+les types et contraintes suivants :\quad
 $x:\eta_1$,\quad $xx:\eta_2$ avec $\eta_1 = (\eta_1 \to \eta_2)$,\quad
 et on renvoie finalement le type $\eta_1 \to \eta_2$.
 
+\medskip
+
+\itempoint Soit le terme à typer $t := (\lambda xy.x) (\lambda
+x'y'.x')$.  On collecte les types et contraintes suivants :\quad
+$x:\eta_1$,\quad $y:\eta_2$,\quad $x':\eta_3$,\quad $y':\eta_4$\quad
+enfin $t:\eta_5$ avec $(\eta_1 \to \eta_2 \to \eta_1) = ((\eta_3 \to
+\eta_4 \to \eta_3) \to \eta_5)$.
+
+\smallskip
+
+{\footnotesize \textcolor{orange}{Attention :} ce terme aurait pu être
+  écrit $(\lambda xy.x) (\lambda xy.x)$ : les deux $x$ \alert{ne sont
+    pas le même} !\par}
+
 \end{frame}
 %
 \begin{frame}
@@ -4890,6 +4909,40 @@ reste des contraintes :
   \xi_2), (\chi_1 = \chi_2)\}$.
 \end{itemize}
 
+\end{frame}
+%
+\begin{frame}
+\frametitle{Résolution des contraintes : exemple}
+
+Reprenons l'exemple $t := (\lambda xy.x) (\lambda x'y'.x')$.  La
+première phase a donné : $x:\eta_1$, $y:\eta_2$, $x':\eta_3$,
+$y':\eta_4$ et le type final $\eta_5$ avec la constrainte $(\eta_1 \to
+\eta_2 \to \eta_1) = ((\eta_3 \to \eta_4 \to \eta_3) \to \eta_5)$.
+
+\smallskip
+
+\begin{itemize}
+\item On examine la seule contrainte $(\eta_1 \to \eta_2 \to \eta_1) =
+  ((\eta_3 \to \eta_4 \to \eta_3) \to \eta_5)$ : ceci retire cette
+  contrainte et on rajoute $\eta_1 = (\eta_3 \to \eta_4 \to \eta_3)$
+  et $(\eta_2 \to \eta_1) = \eta_5$.
+\item On examine $\eta_1 = (\eta_3 \to \eta_4 \to \eta_3)$ : comme
+  $\eta_1$ est une variable, et n'apparaît pas à droite, on enregistre
+  la substitution $\eta_1 \mapsto (\eta_3 \to \eta_4 \to \eta_3)$ et
+  on l'applique à la contrainte restante qui devient $(\eta_2 \to
+  \eta_3 \to \eta_4 \to \eta_3) = \eta_5$.
+\item Comme $\eta_5$ est une variable et n'apparaît pas à gauche, on
+  enregistre la substitution $\eta_5 \mapsto (\eta_2 \to \eta_3 \to
+  \eta_4 \to \eta_3)$ et il ne reste plus de contrainte.
+\end{itemize}
+
+\medskip
+
+Finalement, on a typé : $\vdash (\lambda (x:\eta_3 \to \eta_4 \to
+\eta_3).\,\lambda(y:\eta_2).\,x) \; (\lambda
+(x':\eta_3).\,\lambda(y':\eta_4).\,x') \; : \penalty-1000\; \eta_2 \to
+\eta_3 \to \eta_4 \to \eta_3$.
+
 \end{frame}
 %
 \end{document}
-- 
cgit v1.2.3