Examples of cut elimination steps.

1 files changed, 76 insertions, 15 deletions

diff --git a/transp-inf110-02-typage.tex b/transp-inf110-02-typage.tex
index 6ce7248..ae52265 100644
--- a/transp-inf110-02-typage.tex
+++ b/transp-inf110-02-typage.tex
@@ -32,6 +32,7 @@
 \newcommand{\dbllangle}{\mathopen{\langle\!\langle}}
 \newcommand{\dblrangle}{\mathclose{\rangle\!\rangle}}
 \mathchardef\emdash="07C\relax
+\newcommand{\mpdotsabove}[1]{\inferrule*{\vdots}{#1}}
 \setlength{\derivskip}{4pt}
 %
 %
@@ -2900,6 +2901,10 @@ La règle de coupure exprime une forme de transitivité des démonstrations :
 \inferrule*[left=Cut]{\Gamma \vdash P\\\Gamma,P\vdash Q}{\Gamma\vdash Q}
 \]
 
+\smallskip
+
+(On dira que $P$ est la « formule coupée ».)
+
 \medskip
 
 \itempoint \textbf{Théorème} (Gentzen) : la règle de « coupure » n'est
@@ -2924,46 +2929,102 @@ d'utiliser celle de $\Gamma\vdash P$ partout où $P$ est invoquée
 \medskip
 
 \itempoint En calcul des séquents, la difficulté supplémentaire est
-que $P$ peut faire intervenir un connecteur introduit à droite dans
-$\Gamma\vdash P$ et à gauche dans $\Gamma,P\vdash Q$.
+que $P$ peut faire intervenir un connecteur qui est introduit à droite
+dans $\Gamma\vdash P$ et à gauche dans $\Gamma,P\vdash Q$
+(cf. transp. \ref{cut-elimination-interesting-cases}).
 
 \end{frame}
 %
 \begin{frame}
-\frametitle{Exemples d'étape d'élimination des coupures}
+\label{cut-elimination-boring-cases}
+\frametitle{Exemples d'étape d'élimination des coupures (1)}
+
+\itempoint Cas « inintéressants » : la dernière règle d'une des
+branches de la coupure n'opère pas sur la formule coupée : on fait
+\alert{remonter} la coupure sur cette branche (quitte à choisir).
+
+\begin{center}
+\scalebox{0.65}{%
+$\inferrule*[left={\color{purple}Cut}]{
+\inferrule*[left=\llap{$\land$R}]{\mpdotsabove{\Gamma \vdash P_1}\\\mpdotsabove{\Gamma \vdash P_2}}{\Gamma \vdash P_1\land P_2}
+\\
+\inferrule*[right=\rlap{?}]{\mpdotsabove{\Gamma',P_1\land P_2\vdash Q'}}{\Gamma,P_1\land P_2\vdash Q}
+}{\Gamma\vdash Q}$
+}
+~devient~
+\scalebox{0.65}{%
+$\inferrule*[right=\rlap{?}]{
+\inferrule*[left=\llap{\color{purple}Cut}]{
+\inferrule*[left=\llap{$\land$R}]{\mpdotsabove{\Gamma \vdash P_1}\\\mpdotsabove{\Gamma \vdash P_2}}{\Gamma \vdash P_1\land P_2}
+\\
+\mpdotsabove{\Gamma',P_1\land P_2\vdash Q'}
+}{\Gamma,\Gamma'\vdash Q'}
+}{\Gamma\vdash Q}$
+}
+\end{center}
+
+{\footnotesize (On n'a pas montré ici les règles structurales
+  (contraction+affaiblissement) permettant d'avoir $\Gamma$ et/ou
+  $\Gamma'$ comme hypothèses.)\par}
+
+\bigskip
+
+\itempoint Cas final : une des branches de la coupure est la règle
+« axiome » sur la formule coupée : la coupure disparaît :
+
+\begin{center}
+\scalebox{0.8}{%
+$\inferrule*[left={\color{purple}Cut}]{\inferrule*[left=Ax]{ }{\Gamma \vdash P}\\\mpdotsabove{\Gamma,P\vdash Q}}{\Gamma\vdash Q}$
+}
+~devient~
+\scalebox{0.8}{%
+$\mpdotsabove{\Gamma\vdash Q}$
+}
+\end{center}
+
+\end{frame}
+%
+\begin{frame}
+\label{cut-elimination-interesting-cases}
+\frametitle{Exemples d'étape d'élimination des coupures (2)}
+
+\itempoint Cas « intéressants » : la dernière règle de chaque branche
+de la coupure concerne le connecteur logique de la formule coupée : la
+coupure ne remonte pas et peut même se multiplier, mais le « degré »
+de complexité de la formule coupée diminue :
 
 \begin{center}
 \scalebox{0.8}{%
-$\inferrule*[left=Cut]{
-\inferrule*[left=\llap{$\land$R}]{\Gamma \vdash P_1\\\Gamma \vdash P_2}{\Gamma \vdash P_1\land P_2}
+$\inferrule*[left={\color{purple}Cut}]{
+\inferrule*[left=\llap{$\land$R}]{\mpdotsabove{\Gamma \vdash P_1}\\\mpdotsabove{\Gamma \vdash P_2}}{\Gamma \vdash P_1\land P_2}
 \\
-\inferrule*[right=\rlap{$\land$L$_1$}]{\Gamma,P_1\vdash Q}{\Gamma,P_1\land P_2\vdash Q}
+\inferrule*[right=\rlap{$\land$L$_1$}]{\mpdotsabove{\Gamma,P_1\vdash Q}}{\Gamma,P_1\land P_2\vdash Q}
 }{\Gamma\vdash Q}$
 }
 ~devient~
 \scalebox{0.8}{%
-$\inferrule*[left=Cut]{
-\Gamma \vdash P_1
+$\inferrule*[left={\color{purple}Cut}]{
+\mpdotsabove{\Gamma \vdash P_1}
 \\
-\Gamma,P_1\vdash Q
+\mpdotsabove{\Gamma,P_1\vdash Q}
 }{\Gamma\vdash Q}$
 }
 \end{center}
 
 \begin{center}
 \scalebox{0.7}{%
-$\inferrule*[left=Cut]{
-\inferrule*[left=\llap{$\Rightarrow$R}]{\Gamma, M\vdash P}{\Gamma \vdash M\Rightarrow P}
+$\inferrule*[left={\color{purple}Cut}]{
+\inferrule*[left=\llap{$\Rightarrow$R}]{\mpdotsabove{\Gamma, M\vdash P}}{\Gamma \vdash M\Rightarrow P}
 \\
-\inferrule*[right=\rlap{$\Rightarrow$L}]{\Gamma \vdash M\\\Gamma,P\vdash Q}{\Gamma,M\Rightarrow P\vdash Q}
+\inferrule*[right=\rlap{$\Rightarrow$L}]{\mpdotsabove{\Gamma \vdash M}\\\mpdotsabove{\Gamma,P\vdash Q}}{\Gamma,M\Rightarrow P\vdash Q}
 }{\Gamma\vdash Q}$
 }
 ~devient~
 \scalebox{0.7}{%
-$\inferrule*[left=Cut]{
-\Gamma \vdash M
+$\inferrule*[left={\color{purple}Cut}]{
+\mpdotsabove{\Gamma \vdash M}
 \\
-\inferrule*[right=\rlap{Cut}]{\Gamma,M \vdash P\\\Gamma,P\vdash Q}{\Gamma,M\vdash Q}
+\inferrule*[right=\rlap{{\color{purple}Cut}}]{\mpdotsabove{\Gamma,M \vdash P}\\\mpdotsabove{\Gamma,P\vdash Q}}{\Gamma,M\vdash Q}
 }{\Gamma\vdash Q}$
 }
 \end{center}