Give an example of a fully written out derivation tree.

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}