diff options
| -rw-r--r-- | transp-inf110-02-typage.tex | 21 |
1 files changed, 12 insertions, 9 deletions
diff --git a/transp-inf110-02-typage.tex b/transp-inf110-02-typage.tex index 9337c80..f3e8b1d 100644 --- a/transp-inf110-02-typage.tex +++ b/transp-inf110-02-typage.tex @@ -1042,16 +1042,18 @@ La dérivation du jugement de typage $\Gamma \vdash M : \sigma$ d'un évidemment à partir de $M$ (\alert{aucun choix} à faire !) : \begin{itemize} \item si $M = x$ est une variable, alors un $x:\sigma$ doit être dans - le contexte $\Gamma$ (sinon : échouer), et la dérivation finit par la - règle « variable » ; + le contexte $\Gamma$ (sinon : échouer), et la dérivation consiste en + la règle « variable » ; \item si $M = PQ$ est une application, construire des dérivations de jugements $\Gamma \vdash P : \rho$ et $\Gamma \vdash Q : \sigma$, on doit avoir $\rho = (\sigma\to\tau)$ (sinon : échouer), et la - dérivation finit par la règle « application » ; + dérivation finit par la règle « application » et donne $\Gamma + \vdash M : \tau$ ; \item si $M = \lambda(v:\sigma).E$ est une abstraction, construire une dérivation de jugement $\Gamma' \vdash E : \tau$ dans $\Gamma' := \Gamma \cup \{v:\sigma\}$ {\footnotesize (quitte à renommer $v$)}, - et la dérivation finit par la règle « abstraction ». + et la dérivation finit par la règle « abstraction » et donne $\Gamma + \vdash M : \sigma\to\tau$. \end{itemize} \bigskip @@ -1094,7 +1096,8 @@ correspond à un terme (typable) du $\lambda$CST. \smallskip -\textcolor{brown}{$\rightarrow$ Algorithme de Hindley-Milner.} +\textcolor{brown}{$\rightarrow$ Algorithme de Hindley-Milner + (\emph{inférence} de type).} \bigskip @@ -1152,13 +1155,13 @@ chaque règle « variable ». \itempoint\textbf{Lemme :} Si $\Gamma, v:\sigma \vdash E : \tau$ et $\Gamma \vdash T : \sigma$ alors $\Gamma \vdash E[v\backslash T] : \tau$, où $E[v\backslash T]$ désigne le terme obtenu par substitution -correcte de $v$ par $v$ dans $E$. +correcte de $v$ par $T$ dans $E$. \bigskip \underline{Esquisse de preuve :} reprendre l'arbre de dérivation de $\Gamma, v:\sigma \vdash E : \tau$ en supprimant $v:\sigma$ du -contexte et en substituant $v$ par $E$ partout à droite du ‘$\vdash$’. +contexte et en substituant $v$ par $T$ partout à droite du ‘$\vdash$’. Les règles s'appliquent à l'identique, sauf la règle « variable » introduisant $v:\sigma$, qui est remplacée par l'arbre de dérivation de $\Gamma \vdash T : \sigma$.\qed @@ -2150,8 +2153,8 @@ règle \textsc{Intro} immédiatement suivie par sa règle \textsc{Élim} \medskip -\itempoint Le $\lambda$-calcul simplement typé reste fortement -normalisant avec ces extensions par types produits et sommes et les +\itempoint Le $\lambda$-calcul simplement typé \alert{reste fortement + normalisant} avec ces extensions par types produits et sommes et les réductions ci-dessus {\footnotesize (et types $1$ et $0$ après)}. \medskip |