diff options
| -rw-r--r-- | transp-inf110-02-typage.tex | 48 |
1 files changed, 44 insertions, 4 deletions
diff --git a/transp-inf110-02-typage.tex b/transp-inf110-02-typage.tex index 9040312..c33784d 100644 --- a/transp-inf110-02-typage.tex +++ b/transp-inf110-02-typage.tex @@ -730,8 +730,9 @@ n'a aucune des trois, CoC a les trois) : \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). +$\lambda_\rightarrow$) est une \alert{variante typée} du +$\lambda$-calcul, assurant la propriété de terminaison (normalisation +forte). \medskip @@ -747,12 +748,18 @@ typage : \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$. + libre de type $\sigma$ alors $\lambda(v:\sigma).E$ {\footnotesize + (« fonction prenant $v$ de type $\sigma$ et renvoyant $E$ »)} a + pour type $\sigma\to\tau$. \end{itemize} \medskip +\itempoint Typage \textbf{annoté} (=« à la Church ») : on écrit +$\lambda(v:\sigma).E$ pas juste $\lambda v.E$. + +\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 @@ -766,6 +773,39 @@ $\sigma_1,\ldots,\sigma_k$ : \end{frame} % \begin{frame} +\frametitle{Exemples de termes et de typages} + +{\footnotesize On donnera les règles précises plus tard, commençons + par quelques exemples.\par} + +\begin{itemize} +\item $f:\alpha\to\beta,\; x:\alpha \;\vdash\; fx:\beta$\\ Lire : « dans le + contexte où $f$ est une variable de type $\alpha\to\beta$ et $x$ une + variable de type $\alpha$, alors $fx$ est de type $\beta$ ». +\item $f:\beta\to\alpha\to\gamma,\; x:\alpha,\; y:\beta \;\vdash\; fyx + : \gamma$\\ {\footnotesize (Parenthéser $\beta\to\alpha\to\gamma$ + comme $\beta\to(\alpha\to\gamma)$ et $fyx$ comme $(fy)x$.)} +\item $f:\beta\to\alpha\to\gamma,\; x:\alpha \;\vdash\; + \lambda(y:\beta).fyx \;:\; \beta\to\gamma$\\ {\footnotesize + Comprendre $\lambda(y:\beta).fyx$ comme « fonction prenant $y$ de + type $\beta$ et renvoyant $fyx$ ».} +\item $x:\alpha \;\vdash\; + \lambda(f:\alpha\to\beta).fx\;:\;(\alpha\to\beta)\to\beta$\\ « Si + $x$ est de type $\alpha$ alors le terme + $\lambda(f:\alpha\to\beta).fx$ est de type + $(\alpha\to\beta)\to\beta$. » +\item $\vdash\; \lambda(x:\alpha). + \lambda(f:\alpha\to\beta).fx\;:\;\alpha\to(\alpha\to\beta)\to\beta$\\ « Le + terme $\lambda(x:\alpha).\lambda(f:\alpha\to\beta).fx$ a type + $\alpha\to(\alpha\to\beta)\to\beta$ dans le contexte + vide. »\\ {\footnotesize (Parenthéser + $\alpha\to(\alpha\to\beta)\to\beta$ comme + $\alpha\to((\alpha\to\beta)\to\beta)$.)} +\end{itemize} + +\end{frame} +% +\begin{frame} \frametitle{Types et prétermes} \itempoint Un \textbf{type} du $\lambda$CST est (inductivement) : |