Rules of the simply-typed lambda-calculus.

1 files changed, 122 insertions, 3 deletions

diff --git a/transp-inf110-02-typage.tex b/transp-inf110-02-typage.tex
index af96c40..1c3a778 100644
--- a/transp-inf110-02-typage.tex
+++ b/transp-inf110-02-typage.tex
@@ -639,12 +639,12 @@ Lean…).
 
 \itempoint Dans tous les cas il s'agit de langages assurant la
 terminaison des programmes (cf. transp. \ref{typing-and-termination}),
-ou, dans le contexte du $\lambda$-calcul, la \emph{normalisation
-forte}.  Le type vide doit être inhabité !
+ou, puisqu'il s'agit de variantes du $\lambda$-calcul, la
+\emph{normalisation forte}.  Le type vide doit être inhabité !
 
 \bigskip
 
-Principales grandes familles (chacune avec énormément de variantes) :
+Quelques grandes familles (chacune avec énormément de variantes) :
 \begin{itemize}
 \item théories des types à la Martin-Löf (« MLTT ») : suit jusqu'au
   bout la correspondance de Curry-Howard (\emph{aucune} distinction
@@ -691,4 +691,123 @@ n'a aucune des trois, CoC a les trois) :
 
 \end{frame}
 %
+\section{Le \texorpdfstring{$\lambda$}{lambda}-calcul simplement typé}
+\begin{frame}
+\frametitle{Le $\lambda$-calcul simplement typé : description sommaire}
+
+\itempoint Le $\lambda$-calcul simplement typé (=: $\lambda$CST ou
+$\lambda_\rightarrow$) est une variante typée du $\lambda$-calcul,
+assurant la propriété de terminaison (normalisation forte).
+
+\medskip
+
+\itempoint Il a une seule opération sur les types, le type
+\textbf{fonction} : donnés deux types $\sigma,\tau$, on a un type
+$\sigma\to\tau$ pour les fonctions de l'un vers l'autre.
+
+\medskip
+
+\itempoint L'application et l'abstraction doivent respecter le
+typage :
+\begin{itemize}
+\item si $P$ a pour type $\sigma\to\tau$ et $Q$ a type $\sigma$ alors $PQ$
+  a pour type $\tau$,
+\item si $E$ a pour type $\tau$ en faisant intervenir une variable $v$
+  libre de type $\sigma$ alors $\lambda(v:\sigma).E$ a pour type
+  $\sigma\to\tau$.
+\end{itemize}
+
+\medskip
+
+\itempoint On notera « $x_1:\sigma_1,\ldots,x_k:\sigma_k \vdash
+E:\tau$ » pour dire « $E$ est bien typé avec pour type $\tau$ lorsque
+$x_1,\ldots,x_k$ sont des variables libres de types
+$\sigma_1,\ldots,\sigma_k$ :
+\begin{itemize}
+\item $x_1:\sigma_1,\ldots,x_k:\sigma_k$ s'appelle un
+  \textbf{contexte} de typage (souvent $\Gamma$),
+\item $\Gamma \vdash E:\tau$ s'appelle un \textbf{jugement} de typage.
+\end{itemize}
+
+\end{frame}
+%
+\begin{frame}
+\frametitle{Types et prétermes}
+
+\itempoint Un \textbf{type} du $\lambda$CST est (inductivement) :
+\begin{itemize}
+\item une \textbf{variable de type} ($\alpha$, $\beta$, $\gamma$... en nombre illimité),
+\item un \textbf{type fonction} $(\sigma\to\tau)$ où $\sigma$ et $\tau$
+  sont deux types.
+\end{itemize}
+
+\bigskip
+
+\itempoint Un \textbf{préterme} du $\lambda$CST est (inductivement) :
+\begin{itemize}
+\item une \textbf{variable de terme} ($a$, $b$, $c$... en nombre illimité),
+\item une \textbf{application} $(PQ)$ où $P$ et $Q$ sont deux termes,
+\item une \textbf{abstraction} $\lambda(v:\sigma).E$ où $v$ est une
+  variable, $\sigma$ un type et $E$ un terme.
+\end{itemize}
+
+\medskip
+
+\itempoint Conventions d'écriture :
+\begin{itemize}
+\item « $\rho\to\sigma\to\tau$ » signifie
+  « $(\rho\to(\sigma\to\tau))$ » ; « $xyz$ » signifie
+  « $((xy)z)$ » ;
+\item on note « $\lambda (x:\sigma,t:\tau).E$ » pour « $\lambda
+  (x:\sigma). \lambda (t:\tau). E$ » ;
+\item l'abstraction est moins prioritaire que l'application ;
+\item on considère les termes à renommage près des variables liées
+  {\footnotesize ($\alpha$-conversion)}.
+\end{itemize}
+
+\end{frame}
+%
+\begin{frame}
+\frametitle{Règles de typage}
+
+\itempoint Un \textbf{typage} est la donnée d'un préterme $M$ et d'un
+type $\sigma$.  On note « $M:\sigma$ ».
+
+\medskip
+
+\itempoint Un \textbf{contexte} est un ensemble fini $\Gamma$ de
+typages $x_i:\sigma_i$ où $x_1,\ldots,x_k$ sont des \alert{variables}
+de terme \alert{distinctes}.  On le note
+« $x_1:\sigma_1,\ldots,x_k:\sigma_k$ ».
+
+\medskip
+
+\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$ ».
+
+\medskip
+
+\textbf{Règles} de typage du $\lambda$CST : {\footnotesize (quels que
+  soient $\Gamma,x,\sigma,\ldots$,)}
+\begin{itemize}
+\item \textcolor{olive}{(« variable »)} si $(x:\sigma) \in \Gamma$
+  alors $\Gamma \vdash x:\sigma$ ;
+\item \textcolor{olive}{(« application »)} si $\Gamma \vdash
+  P:\sigma\to\tau$ et $\Gamma \vdash Q:\sigma$ alors $\Gamma \vdash
+  PQ:\tau$ ;
+\item \textcolor{olive}{(« abstraction »)} si $\Gamma, v:\sigma \vdash
+  E:\tau$ alors $\Gamma \vdash \lambda(v:\sigma).E : \sigma\to\tau$.
+\end{itemize}
+
+\smallskip
+
+{\footnotesize (Comprendre : l'ensemble des jugements de typage est
+  l'ensemble engendré par les règles ci-dessus, i.e., le plus petit
+  ensemble qui les respecte.)\par}
+
+\end{frame}
+%
 \end{document}