summaryrefslogtreecommitdiffstats
diff options
context:
space:
mode:
authorDavid A. Madore <david+git@madore.org>2023-12-16 17:52:33 +0100
committerDavid A. Madore <david+git@madore.org>2023-12-16 17:52:33 +0100
commit65c7a5fae077f4737be6de653a48f6d4234d32d9 (patch)
tree3cccc81d137d3b97ec436c8067ebdc2fdc62383a
parent10782eec65fcddacdfe7a6e1a960e947c3726f47 (diff)
downloadinf110-lfi-65c7a5fae077f4737be6de653a48f6d4234d32d9.tar.gz
inf110-lfi-65c7a5fae077f4737be6de653a48f6d4234d32d9.tar.bz2
inf110-lfi-65c7a5fae077f4737be6de653a48f6d4234d32d9.zip
An example of the full H-M algorithm.
-rw-r--r--transp-inf110-02-typage.tex63
1 files 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}
@@ -4892,4 +4911,38 @@ reste des contraintes :
\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}