diff options
| -rw-r--r-- | transp-inf110-02-typage.tex | 43 |
1 files changed, 35 insertions, 8 deletions
diff --git a/transp-inf110-02-typage.tex b/transp-inf110-02-typage.tex index 4fdb8da..0d0443d 100644 --- a/transp-inf110-02-typage.tex +++ b/transp-inf110-02-typage.tex @@ -890,6 +890,33 @@ de type $\tau$ dans le contexte $\Gamma$ ». \end{frame} % \begin{frame} +\frametitle{Représentation des règles de typage} + +Les trois règles de typage du $\lambda$CST : + +\[ +\inferrule*[left=\llap{Var}]{ }{\Gamma,x:\sigma \vdash x:\sigma} +\] + +\[ +\inferrule*[left=\llap{App},sep=4em]{\Gamma \vdash P:\sigma\to\tau\\ \Gamma + \vdash Q:\sigma}{\Gamma \vdash PQ:\tau} +\] + +\[ +\inferrule*[left=\llap{Abs}]{\Gamma, v:\sigma \vdash E:\tau}{\Gamma + \vdash \lambda(v:\sigma).E : \sigma\to\tau} +\] + +\bigskip + +\itempoint Chaque « fraction » indique que le jugement écrit +\alert{en-dessous} découle par la règle inscrite \alert{à côté} à +partir des hypothèses portées \alert{au-dessus}. + +\end{frame} +% +\begin{frame} \frametitle{Exemple de dérivation} Montrons le jugement selon lequel @@ -897,7 +924,7 @@ $\lambda(f:\beta\to\alpha\to\gamma). \lambda(x:\alpha). \lambda(y:\beta). fyx$ est un terme de type $(\beta\to\alpha\to\gamma) \to (\alpha\to\beta\to\gamma)$ dans le contexte vide : -\vskip-3ex +\vskip-2ex {\footnotesize \[ @@ -906,12 +933,12 @@ est un terme de type $(\beta\to\alpha\to\gamma) \to \inferrule*[left=\llap{Abs}]{ \inferrule*[left=\llap{App}]{ \inferrule*[left=\llap{App}]{ -\inferrule*[left=\llap{Var}]{\relax}{\mbox{$\begin{array}{cc}\scriptscriptstyle f:\beta\to\alpha\to\gamma,\\ \scriptscriptstyle x:\alpha,y:\beta\\ \end{array}$} \vdash f : \beta\to\alpha\to\gamma} +\inferrule*[left=\llap{Var}]{ }{\mbox{$\begin{array}{cc}\scriptscriptstyle f:\beta\to\alpha\to\gamma,\\ \scriptscriptstyle x:\alpha,y:\beta\\ \end{array}$} \vdash f : \beta\to\alpha\to\gamma} \\ -\inferrule*[right=\rlap{Var}]{\relax}{\mbox{$\begin{array}{cc}\scriptscriptstyle f:\beta\to\alpha\to\gamma,\\ \scriptscriptstyle x:\alpha,y:\beta\\ \end{array}$} \vdash y : \beta} +\inferrule*[right=\rlap{Var}]{ }{\mbox{$\begin{array}{cc}\scriptscriptstyle f:\beta\to\alpha\to\gamma,\\ \scriptscriptstyle x:\alpha,y:\beta\\ \end{array}$} \vdash y : \beta} }{\mbox{$\begin{array}{cc}\scriptscriptstyle f:\beta\to\alpha\to\gamma,\\ \scriptscriptstyle x:\alpha,y:\beta\\ \end{array}$} \vdash fy : \alpha\to\gamma} \\ -\inferrule*[right=\rlap{Var}]{\relax}{\mbox{$\begin{array}{cc}\scriptscriptstyle f:\beta\to\alpha\to\gamma,\\ \scriptscriptstyle x:\alpha,y:\beta\\ \end{array}$} \vdash x : \alpha} +\inferrule*[right=\rlap{Var}]{ }{\mbox{$\begin{array}{cc}\scriptscriptstyle f:\beta\to\alpha\to\gamma,\\ \scriptscriptstyle x:\alpha,y:\beta\\ \end{array}$} \vdash x : \alpha} }{f:\beta\to\alpha\to\gamma, x:\alpha, y:\beta \vdash fyx : \gamma} }{f:\beta\to\alpha\to\gamma, x:\alpha \vdash \lambda(y:\beta). fyx : \beta\to\gamma} }{f:\beta\to\alpha\to\gamma \vdash \lambda(x:\alpha). \lambda(y:\beta). fyx : \alpha\to\beta\to\gamma} @@ -920,7 +947,7 @@ est un terme de type $(\beta\to\alpha\to\gamma) \to \par} Chaque barre horizontale justifie le jugement écrit \alert{en-dessous} -par la règle inscrote \alert{à côté} à partir des hypothèses portées +par la règle inscrite \alert{à côté} à partir des hypothèses portées \alert{au-dessus}. \medskip @@ -1066,12 +1093,12 @@ dont on n'a donné que les types et les règles appliquées ? \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*[left=\llap{Var}]{ }{\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} +\inferrule*[right=\rlap{Var}]{ }{\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} +\inferrule*[right=\rlap{Var}]{ }{\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} |