diff options
Diffstat (limited to 'transp-inf110-02-typage.tex')
| -rw-r--r-- | transp-inf110-02-typage.tex | 103 |
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} |