Beta-reduction and strong normalization (to be continued).

1 files changed, 41 insertions, 0 deletions

diff --git a/transp-inf110-02-typage.tex b/transp-inf110-02-typage.tex
index 181784f..55c5de1 100644
--- a/transp-inf110-02-typage.tex
+++ b/transp-inf110-02-typage.tex
@@ -1051,4 +1051,45 @@ et
 
 \end{frame}
 %
+\begin{frame}
+\frametitle{Typage et $\beta$-réduction}
+
+On rappelle que la « $\beta$-réduction » désigne le remplacement en
+sous-expression d'un « redex » $(\lambda (v:\sigma). E)T$ par son
+« réduit » $E[v\backslash T]$.
+
+\medskip
+
+On note $X \rightarrow_\beta X'$ pour une $\beta$-réduction, et $X
+\twoheadrightarrow_\beta X'$ pour une suite de $\beta$-réductions.
+
+\bigskip
+
+\itempoint D'après le lemme de substitution, si $\Gamma \vdash
+(\lambda (v:\sigma). E)T : \tau$ alors on a aussi $\Gamma \vdash
+E[v\backslash T] : \tau$.
+
+\bigskip
+
+\itempoint Toujours d'après ce lemme, si $X \twoheadrightarrow_\beta
+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).
+
+\end{frame}
+%
+\begin{frame}
+\frametitle{Normalisation forte}
+
+\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.
+
+\end{frame}
+%
 \end{document}