summaryrefslogtreecommitdiffstats
path: root/transp-inf110-02-typage.tex
diff options
context:
space:
mode:
Diffstat (limited to 'transp-inf110-02-typage.tex')
-rw-r--r--transp-inf110-02-typage.tex21
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