diff options
| -rw-r--r-- | transp-inf110-02-typage.tex | 55 |
1 files changed, 55 insertions, 0 deletions
diff --git a/transp-inf110-02-typage.tex b/transp-inf110-02-typage.tex index 9c88889..b31d1cb 100644 --- a/transp-inf110-02-typage.tex +++ b/transp-inf110-02-typage.tex @@ -2836,6 +2836,61 @@ d'hypothèse en remontant. \end{frame} % +\begin{frame} +\frametitle{Calcul des séquents : équivalence avec la déduction naturelle} + +L'équivalence générale entre déduction naturelle et calcul des +séquents n'est pas difficile si on utilise librement la règle de +coupure. + +\medskip + +Montrons l'exemple de la conversion entre $\Rightarrow$Élim et +$\Rightarrow$Left : + +\medskip + +\itempoint Dans le sens déduction naturelle $\to$ calcul des +séquents : +\vskip-3ex\leavevmode +\begin{center} +\scalebox{0.8}{% +\begin{tabular}{c|c} +Déduction naturelle&Calcul des séquents\\\hline +$\inferrule*[left=$\Rightarrow$Élim]{\Gamma\vdash P\Rightarrow Q\\\Gamma\vdash P}{\Gamma\vdash Q}$ +& +$\inferrule*[left=Cut]{\Gamma\vdash P\Rightarrow Q +\\ +\inferrule*[left=$\Rightarrow$L]{\Gamma\vdash P\\ +\inferrule*[left=Ax]{ }{\Gamma,Q\vdash Q} +}{\Gamma,P\Rightarrow Q\vdash Q} +}{\Gamma\vdash Q}$ +\end{tabular} +} +\end{center} + +\itempoint Dans le sens calcul des séquents $\to$ déduction +naturelle : +\vskip-6ex\leavevmode +\begin{center} +\scalebox{0.8}{% +\begin{tabular}{c|c} +Calcul des séquents&Déduction naturelle\\\hline +$\inferrule*[left=$\Rightarrow$L]{\Gamma\vdash M\\\Gamma,P\vdash R}{\Gamma,M\Rightarrow P\vdash R}$ +& +$\inferrule*[left=$\Rightarrow$Élim]{ +\inferrule*[left=\llap{$\Rightarrow$Intro}]{\Gamma,P\vdash R}{\Gamma\vdash P\Rightarrow R} +\\ +\inferrule*[left=$\Rightarrow$Élim]{ +\inferrule*[left=\llap{Ax}]{ }{\Gamma,M\Rightarrow P\vdash M\Rightarrow P} +\\\Gamma\vdash M}{\Gamma,M\Rightarrow P\vdash P} +}{\Gamma,M\Rightarrow P\vdash R}$ +\end{tabular} +} +\end{center} + +\end{frame} +% % TODO: % - présentation en calcul des séquents % - élimination des coupures |