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