From 51ee5482d0824c7b517bdae7682f1f8765577f35 Mon Sep 17 00:00:00 2001
From: "David A. Madore" <david+git@madore.org>
Date: Wed, 15 Nov 2023 21:04:02 +0100
Subject: Give an example of a fully written out derivation tree.

---
 transp-inf110-02-typage.tex | 39 +++++++++++++++++++++++++++++++++++++++
 1 file changed, 39 insertions(+)

(limited to 'transp-inf110-02-typage.tex')

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}
-- 
cgit v1.2.3