Sequent calculus: better discuss structural rules.

1 files changed, 38 insertions, 0 deletions

diff --git a/transp-inf110-02-typage.tex b/transp-inf110-02-typage.tex
index 07e2999..9c88889 100644
--- a/transp-inf110-02-typage.tex
+++ b/transp-inf110-02-typage.tex
@@ -1420,6 +1420,9 @@ $\bot$
 \\
 \end{tabular}
 
+{\footnotesize Dans tout ça, $\Gamma$ désigne un jeu (\alert{non
+    ordonné}, mais avec multiplicités) d'hypothèses.\par}
+
 {\footnotesize Les hypothèses en \textcolor{mydarkgreen}{vert} sont
   « déchargées », c'est-à-dire qu'elles disparaissent.\par}
 
@@ -2798,6 +2801,41 @@ Et que dans le transp. \ref{example-proposition-proof-with-implication} :
 
 \end{frame}
 %
+\begin{frame}
+\label{sequent-calculus-structural-rules}
+\frametitle{Calcul des séquents : règles « structurales »}
+
+\itempoint On peut choisir de séparer la règle $\inferrule*[left=Ax]{
+}{\Gamma,Q \vdash Q}$ en deux, une règle d'axiome strict et une règle
+d'« affaiblissement » :
+
+\begin{center}
+\begin{tabular}{c|c}
+$\inferrule*[left=Ax]{ }{Q \vdash Q}$
+&$\inferrule*[left=Weak]{\Gamma \vdash Q}{\Gamma,P\vdash Q}$
+\end{tabular}
+\end{center}
+
+\medskip
+
+\itempoint Comme en déduction naturelle, les hypothèses n'ont pas
+d'ordre.
+
+\medskip
+
+\itempoint Si elles ont des multiplicités, la règle de contraction est
+nécessaire (sans elle, on ne peut pas prouver $(A\Rightarrow B) \land A
+\vdash B$) :
+\[
+\inferrule*[left=Contr]{\Gamma,P,P \vdash Q}{\Gamma,P\vdash Q}
+\]
+On peut s'en dispenser en décidant que les hypothèses n'ont pas de
+multiplicité (forment un ensemble, pas un multi-ensemble), ou en
+modifiant les règles $\Rightarrow$L et $\land$L pour ne pas perdre
+d'hypothèse en remontant.
+
+\end{frame}
+%
 % TODO:
 % - présentation en calcul des séquents
 % - élimination des coupures