diff options
| -rw-r--r-- | transp-inf110-02-typage.tex | 39 |
1 files changed, 39 insertions, 0 deletions
diff --git a/transp-inf110-02-typage.tex b/transp-inf110-02-typage.tex index 1c3a778..03bc64b 100644 --- a/transp-inf110-02-typage.tex +++ b/transp-inf110-02-typage.tex @@ -21,6 +21,7 @@ \usepackage{amsthm} % \usepackage{mathrsfs} +\usepackage{mathpartir} % \usepackage{graphicx} \usepackage{tikz} @@ -808,6 +809,44 @@ $\tau$ dans le contexte $\Gamma$ ». l'ensemble engendré par les règles ci-dessus, i.e., le plus petit ensemble qui les respecte.)\par} +\medskip + +\itempoint Une \textbf{dérivation} d'un jugement est un arbre +(d'instances de) règles qui aboutit au jugement considéré. + +\end{frame} +% +\begin{frame} +\frametitle{Exemple de dérivation} + +Montrons le jugement selon lequel +$\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 : + +{\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 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} +}{\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} +}{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} +}{\vdash \lambda(f:\beta\to\alpha\to\gamma). \lambda(x:\alpha). \lambda(y:\beta). fyx : (\beta\to\alpha\to\gamma) \to (\alpha\to\beta\to\gamma)} +\] +\par} + +Ceci est typographiquement abominable et hautement redondant, ce qui +explique qu'on écrive rarement de tels arbres complètement. + \end{frame} % \end{document} |