diff options
| -rw-r--r-- | transp-inf110-02-typage.tex | 79 |
1 files changed, 79 insertions, 0 deletions
diff --git a/transp-inf110-02-typage.tex b/transp-inf110-02-typage.tex index b31d1cb..6ce7248 100644 --- a/transp-inf110-02-typage.tex +++ b/transp-inf110-02-typage.tex @@ -1150,6 +1150,7 @@ chaque règle « variable ». \end{frame} % \begin{frame} +\label{substitution-lemma} \frametitle{Lemme de substitution} \itempoint\textbf{Lemme :} Si $\Gamma, v:\sigma \vdash E : \tau$ et @@ -2891,6 +2892,84 @@ $\inferrule*[left=$\Rightarrow$Élim]{ \end{frame} % +\begin{frame} +\frametitle{Calcul des séquents : élimination des coupures} + +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} +\] + +\medskip + +\itempoint \textbf{Théorème} (Gentzen) : la règle de « coupure » n'est +pas nécessaire en calcul des séquents : tout séquent prouvable avec +elle est encore prouvable sans elle. + +\smallskip + +La preuve est même constructive et se fait par des transformations +« locales ». + +\medskip + +\itempoint En déduction naturelle, l'élimination des coupures est +facile : pour éliminer une coupure il suffit de reprendre la +démonstration de $\Gamma,P\vdash Q$ avec l'hypothèse $P$ en moins, et +d'utiliser celle de $\Gamma\vdash P$ partout où $P$ est invoquée +(cf. transp. \ref{substitution-lemma}). {\footnotesize (La difficulté + est plutôt l'élimination de « détours » Intro+Élim $\approx$ + normal\textsuperscript{ion}.)} + +\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$. + +\end{frame} +% +\begin{frame} +\frametitle{Exemples d'étape d'élimination des coupures} + +\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*[right=\rlap{$\land$L$_1$}]{\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 +\\ +\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*[right=\rlap{$\Rightarrow$L}]{\Gamma \vdash M\\\Gamma,P\vdash Q}{\Gamma,M\Rightarrow P\vdash Q} +}{\Gamma\vdash Q}$ +} +~devient~ +\scalebox{0.7}{% +$\inferrule*[left=Cut]{ +\Gamma \vdash M +\\ +\inferrule*[right=\rlap{Cut}]{\Gamma,M \vdash P\\\Gamma,P\vdash Q}{\Gamma,M\vdash Q} +}{\Gamma\vdash Q}$ +} +\end{center} + +\end{frame} +% % TODO: % - présentation en calcul des séquents % - élimination des coupures |