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