More properties of typing, incl. the substitution lemma.

1 files changed, 97 insertions, 6 deletions

diff --git a/transp-inf110-02-typage.tex b/transp-inf110-02-typage.tex
index eb53cfd..181784f 100644
--- a/transp-inf110-02-typage.tex
+++ b/transp-inf110-02-typage.tex
@@ -850,7 +850,7 @@ explique qu'on écrive rarement de tels arbres complètement.
 \end{frame}
 %
 \begin{frame}
-\frametitle{Propriétés de la dérivation}
+\frametitle{Propriétés du typage}
 
 Les propriétés suivantes sont faciles mais utiles :
 
@@ -866,10 +866,17 @@ M:\sigma$ aussi.
   « variable » à « $x:\sigma \vdash x:\sigma$ » et en prenant
   l'affaiblissement comme règle.  C'est peut-être préférable.\par}
 
+\medskip
+
+\itempoint \textbf{Duplication :} si $\Gamma, x:\rho, x':\rho \vdash
+M:\sigma$ alors $\Gamma, x:\rho \vdash M[x'\backslash x]:\sigma$ aussi
+(où $M[x'\backslash x]$ désigne la substitution correcte de $x'$
+par $x$).
+
 \smallskip
 
 {\footnotesize \emph{Remarque :} Le typage linéaire supprime notamment
-  l'affaiblissement.\par}
+  l'affaiblissement et la duplication.\par}
 
 \medskip
 
@@ -884,6 +891,11 @@ alors $\Gamma|_{\operatorname{free}(E)} \vdash E:\tau$ où
 $\Gamma|_{\operatorname{free}(E)}$ est la partie de $\Gamma$
 concernant les variables libres de $E$.
 
+\medskip
+
+\itempoint \textbf{Renommage :} si $\Gamma \vdash E:\tau$ alors ceci
+vaut encore après tout renommage des variables libres.
+
 \end{frame}
 %
 \begin{frame}
@@ -931,8 +943,8 @@ type).
 \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).
+où on a effacé les termes pour ne garder que les types, retrouver un
+terme (transp. suivant).
 
 \smallskip
 
@@ -941,8 +953,8 @@ terme (transp. suivant).
 \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)$ ?
+du $\lambda$-calcul non typé, p.ex. $\lambda xyz.xz(yz)$, savoir s'il
+correspond à un terme (typable) du $\lambda$CST.
 
 \smallskip
 
@@ -960,4 +972,83 @@ ayant ce type.
 
 \end{frame}
 %
+\begin{frame}
+\frametitle{Reconstruction du terme typé}
+
+Peut-on retrouver les termes manquants dans un arbre de dérivation
+dont on n'a donné que les types et les règles appliquées ?
+
+{\footnotesize
+\[
+\inferrule*[left=\llap{Abs}]{
+\inferrule*[left=\llap{Abs}]{
+\inferrule*[left=\llap{Abs}]{
+\inferrule*[left=\llap{App}]{
+\inferrule*[left=\llap{App}]{
+\inferrule*[left=\llap{Var}]{\relax}{\mbox{$\begin{array}{cc}\scriptscriptstyle \textbf{?}:\beta\to\alpha\to\gamma,\\ \scriptscriptstyle \textbf{?}:\alpha,\textbf{?}:\beta\\ \end{array}$} \vdash \textbf{?} : \beta\to\alpha\to\gamma}
+\\
+\inferrule*[right=\rlap{Var}]{\relax}{\mbox{$\begin{array}{cc}\scriptscriptstyle \textbf{?}:\beta\to\alpha\to\gamma,\\ \scriptscriptstyle \textbf{?}:\alpha,\textbf{?}:\beta\\ \end{array}$} \vdash \textbf{?} : \beta}
+}{\mbox{$\begin{array}{cc}\scriptscriptstyle \textbf{?}:\beta\to\alpha\to\gamma,\\ \scriptscriptstyle \textbf{?}:\alpha,\textbf{?}:\beta\\ \end{array}$} \vdash \textbf{?} : \alpha\to\gamma}
+\\
+\inferrule*[right=\rlap{Var}]{\relax}{\mbox{$\begin{array}{cc}\scriptscriptstyle \textbf{?}:\beta\to\alpha\to\gamma,\\ \scriptscriptstyle \textbf{?}:\alpha,\textbf{?}:\beta\\ \end{array}$} \vdash \textbf{?} : \alpha}
+}{\textbf{?}:\beta\to\alpha\to\gamma, \textbf{?}:\alpha, \textbf{?}:\beta \vdash \textbf{?} : \gamma}
+}{\textbf{?}:\beta\to\alpha\to\gamma, \textbf{?}:\alpha \vdash \textbf{?} : \beta\to\gamma}
+}{\textbf{?}:\beta\to\alpha\to\gamma \vdash \textbf{?} : \alpha\to\beta\to\gamma}
+}{\vdash \textbf{?} : (\beta\to\alpha\to\gamma) \to (\alpha\to\beta\to\gamma)}
+\]
+\par}
+
+\textbf{Oui} (aux noms des variables près) à condition, en cas de
+types identiques dans le contexte, d'identifier l'élément utilisé pour
+chaque règle « variable ».
+
+\bigskip
+
+\itempoint\textcolor{blue}{Le terme typé représente exactement l'arbre
+  de dérivation} du jugement le concernant.
+
+\end{frame}
+%
+\begin{frame}
+\frametitle{Lemme de substitution}
+
+\itempoint\textbf{Lemme :} Si $\Gamma, v:\sigma \vdash E : \tau$ et
+$\Gamma \vdash T : \sigma$ alors $\Gamma \vdash E[v\backslash T] :
+\tau$, où $E[v\backslash T]$ désigne le terme obtenu par substitution
+correcte de $v$ par $v$ dans $E$.
+
+\bigskip
+
+\underline{Esquisse de preuve :} reprendre l'arbre de dérivation de
+$\Gamma, v:\sigma \vdash E : \tau$ en supprimant $v:\sigma$ du
+contexte et en substituant $v$ par $E$ partout à droite du ‘$\vdash$’.
+Les règles s'appliquent à l'identique, sauf la règle « variable »
+introduisant $v:\sigma$, qui est remplacée par l'arbre de dérivation
+de $\Gamma \vdash T : \sigma$.\qed
+
+\medskip
+
+\centerline{*}
+
+\medskip
+
+Remarquer la similarité entre
+\[
+\inferrule*[left=App]{
+\inferrule*[left=Abs]{\Gamma, v:\sigma \vdash E : \tau}{
+\Gamma \vdash \lambda(v:\sigma).E : \sigma\to\tau}
+\\
+\Gamma \vdash T : \sigma
+}{\Gamma \vdash (\lambda(v:\sigma).E)T : \tau}
+\]
+et
+\[
+\inferrule*[left=Subs]{\Gamma, v:\sigma \vdash E : \tau
+\\
+\Gamma \vdash T : \sigma
+}{\Gamma \vdash E[v\backslash T] : \tau}
+\]
+
+\end{frame}
+%
 \end{document}