Brief summary of Tait's proof of normalization of the STLC.

1 files changed, 42 insertions, 5 deletions

diff --git a/transp-inf110-02-typage.tex b/transp-inf110-02-typage.tex
index e150b3e..4fdb8da 100644
--- a/transp-inf110-02-typage.tex
+++ b/transp-inf110-02-typage.tex
@@ -859,8 +859,8 @@ de terme \alert{distinctes}.  On le note
 \itempoint Un \textbf{jugement} de typage est la donnée d'un contexte
 $\Gamma$ et d'un typage $E:\tau$, sujet aux règles ci-dessous.  On
 note $\Gamma \vdash E:\tau$ (ou juste $\vdash E:\tau$ si $\Gamma =
-\varnothing$), et on dit que $E$ est un « \textbf{terme} de type
-$\tau$ dans le contexte $\Gamma$ ».
+\varnothing$), et on dit que $E$ est un « \textbf{terme} (= bien typé)
+de type $\tau$ dans le contexte $\Gamma$ ».
 
 \medskip
 
@@ -1158,8 +1158,8 @@ X'$ et $\Gamma \vdash X:\tau$ alors $\Gamma \vdash X':\tau$.
 \bigskip
 
 \textcolor{blue}{\textbf{Moralité :}} le typage est compatible avec
-l'évaluation du $\lambda$-calcul (le type d'un terme ne change pas
-quand on effectue la $\beta$-réduction).
+l'évaluation du $\lambda$-calcul (un terme bien typé reste bien typé
+quand on effectue la $\beta$-réduction et le type ne change pas).
 
 \end{frame}
 %
@@ -1169,7 +1169,44 @@ quand on effectue la $\beta$-réduction).
 \itempoint\textbf{Théorème} (Turing, Tait, Girard) : le
 $\lambda$-calcul simplement typé est \textbf{fortement normalisant},
 c'est-à-dire que toute suite de $\beta$-réductions sur un terme
-(bien-typé !) termine.
+(bien typé !) termine.
+
+\bigskip
+
+{\footnotesize
+
+\textcolor{blue}{Idée cruciale de la preuve :} une induction directe
+échoue ($P,Q$ fortement normalisables $\not\Rightarrow$ $PQ$ fortement
+normalisable).  À la place, on introduit une notion \emph{plus forte}
+permettant l'induction :
+
+\smallskip
+
+\itempoint\textbf{Définition} technique : un terme $P$ de type $\rho$
+est dit « fortement calculable » lorsque :
+\begin{itemize}
+\item si $\rho = \alpha$ est une variable de type (type
+  « atomique ») : $P$ est fortement normalisable,
+\item si $\rho = (\sigma\to\tau)$ est un type fonction : pour
+  \alert{tout} $Q$ de type $\sigma$ fortement calculable, $PQ$ est
+  fortement calculable.
+\end{itemize}
+
+\smallskip
+
+On prouve alors successivement :
+\begin{itemize}
+\item tout terme fortement calculable est fortement normalisable
+  (induction facile sur le type),
+\item si $x_1:\sigma_1,\ldots,x_k:\sigma_k \vdash E:\tau$ et si
+  $v_1,\ldots,v_k$ sont de types $\sigma_1,\ldots,\sigma_k$, fortement
+  calculables et n'impliquant pas $x_1,\ldots,x_k$, alors la
+  substitution de $v_i$ pour $x_i$ dans $E$ est fortement calculable
+  (preuve par induction sur la dérivation du jugement, i.e., induction
+  sur $E$ : le cas délicat est l'abstraction).
+\end{itemize}
+
+\par}
 
 \end{frame}
 %