diff options
| -rw-r--r-- | transp-inf110-02-typage.tex | 47 |
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} % |