Graphical representation of typing rules.

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}