Some properties of derivation in simply-typed lambda-calculus.

1 files changed, 111 insertions, 0 deletions

diff --git a/transp-inf110-02-typage.tex b/transp-inf110-02-typage.tex
index 03bc64b..eb53cfd 100644
--- a/transp-inf110-02-typage.tex
+++ b/transp-inf110-02-typage.tex
@@ -849,4 +849,115 @@ explique qu'on écrive rarement de tels arbres complètement.
 
 \end{frame}
 %
+\begin{frame}
+\frametitle{Propriétés de la dérivation}
+
+Les propriétés suivantes sont faciles mais utiles :
+
+\medskip
+
+\itempoint \textbf{Affaiblissement :} si $\Gamma \subseteq \Gamma'$
+sont deux contextes et $\Gamma \vdash M:\sigma$ alors $\Gamma' \vdash
+M:\sigma$ aussi.
+
+\smallskip
+
+{\footnotesize On pouvait présenter les règles en limitant la règle
+  « variable » à « $x:\sigma \vdash x:\sigma$ » et en prenant
+  l'affaiblissement comme règle.  C'est peut-être préférable.\par}
+
+\smallskip
+
+{\footnotesize \emph{Remarque :} Le typage linéaire supprime notamment
+  l'affaiblissement.\par}
+
+\medskip
+
+\itempoint \textbf{Variables libres :} si
+$x_1:\sigma_1,\ldots,x_k:\sigma_k \vdash E:\tau$ alors toute variable
+libre de $E$ est une des $x_1,\ldots,x_k$.
+
+\medskip
+
+\itempoint \textbf{Variables inutiles :} si $\Gamma \vdash E:\tau$
+alors $\Gamma|_{\operatorname{free}(E)} \vdash E:\tau$ où
+$\Gamma|_{\operatorname{free}(E)}$ est la partie de $\Gamma$
+concernant les variables libres de $E$.
+
+\end{frame}
+%
+\begin{frame}
+\frametitle{Construction de la dérivation}
+
+La dérivation du jugement de typage $\Gamma \vdash M : \sigma$ d'un
+(pré)terme $M$ du $\lambda$CST se construit systématiquement et
+évidemment à partir de $M$ (\alert{aucun choix} à faire !) :
+\begin{itemize}
+\item si $M = x$ est une variable, alors un $x:\sigma$ doit être dans
+  le contexte $\Gamma$ (sinon : échouer), et la dérivation est par la
+  règle « variable » ;
+\item si $M = PQ$ est une application, construire des dérivations de
+  jugements $\Gamma \vdash P : \rho$ et $\Gamma \vdash Q : \sigma$, on
+  doit avoir $\rho = (\sigma\to\tau)$ (sinon : échouer), et la
+  dérivation est par la règle « application » ;
+\item si $M = \lambda(v:\sigma).E$ est une abstraction, construire une
+  dérivation de jugement $\Gamma' \vdash E : \tau$ dans $\Gamma' :=
+  \Gamma \cup \{v:\sigma\}$ {\footnotesize (quitte à renommer $v$)},
+  et la dérivation est par la règle « abstraction ».
+\end{itemize}
+
+\bigskip
+
+\itempoint \textbf{Donc :} aussi bien la vérification de type
+(vérifier $\Gamma \vdash M : \sigma$) que l'assignation de type
+(trouver $\sigma$ à partir de $\Gamma,M$) sont (très facilement)
+\alert{décidables} dans le $\lambda$CST.  De plus, $\sigma$ est
+\alert{unique} (donnés $\Gamma$ et $M$).
+
+\end{frame}
+%
+\begin{frame}
+\frametitle{Problèmes faciles et moins faciles}
+
+\itempoint Facile (transp. précédent) : donné un (pré)terme $M$,
+trouver son (seul possible) type $\sigma$ est facile (notamment :
+vérifier que $M$ est un terme = bien typé, ou vérifier un jugement de
+type).
+
+\smallskip
+
+\textcolor{blue}{Le terme donne directement l'arbre de dérivation.}
+
+\bigskip
+
+\itempoint Facile aussi : réciproquement, donné un arbre de dérivation
+où on a effacé les termes pour ne garder que les types, retrouver le
+terme (transp. suivant).
+
+\smallskip
+
+\textcolor{blue}{L'arbre de dérivation redonne directement le terme.}
+
+\bigskip
+
+\itempoint Moins facile : donné un terme « désannoté », i.e., un terme
+du $\lambda$-calcul non typé, savoir s'il correspond à un terme
+(typable) du $\lambda$CST.  P.ex. : $\lambda xyz.xz(yz)$ ?
+
+\smallskip
+
+\textcolor{brown}{$\rightarrow$ Algorithme de Hindley-Milner.}
+
+\bigskip
+
+\itempoint Moins facile : donné un type, savoir s'il existe un terme
+ayant ce type.
+
+\smallskip
+
+\textcolor{brown}{$\rightarrow$ Décidabilité du calcul propositionnel
+  intuitionniste.}
+
+\end{frame}
+%
 \end{document}