diff options
| -rw-r--r-- | transp-inf110-02-typage.tex | 91 |
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} |