Give some examples of terms and types in the STLC before formalizing.

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) :