From c721a4364dd073bbe2be70dfa74d3013bc3fd495 Mon Sep 17 00:00:00 2001
From: "David A. Madore" <david+git@madore.org>
Date: Thu, 16 Nov 2023 19:52:21 +0100
Subject: Beta-reduction and strong normalization (to be continued).

---
 transp-inf110-02-typage.tex | 41 +++++++++++++++++++++++++++++++++++++++++
 1 file changed, 41 insertions(+)

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
@@ -1049,6 +1049,47 @@ et
 }{\Gamma \vdash E[v\backslash T] : \tau}
 \]
 
+\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}
-- 
cgit v1.2.3