diff options
| -rw-r--r-- | transp-inf110-02-typage.tex | 77 |
1 files changed, 74 insertions, 3 deletions
diff --git a/transp-inf110-02-typage.tex b/transp-inf110-02-typage.tex index cae26b4..32ff068 100644 --- a/transp-inf110-02-typage.tex +++ b/transp-inf110-02-typage.tex @@ -1985,6 +1985,7 @@ intuitionniste restreint au seul connecteur $\Rightarrow$. \end{frame} % \begin{frame} +\label{example-proposition-proof-with-implication} \frametitle{Correspondance de Curry-Howard : exemple avec implication} \itempoint Transformons en démonstration le terme @@ -1994,11 +1995,11 @@ $(\beta\to\alpha\to\gamma) \to (\alpha\to\beta\to\gamma)$ : {\footnotesize \[ -\inferrule*[left=\llap{$\Rightarrow$Élim}]{ -\inferrule*[left=\llap{$\Rightarrow$Élim}]{ -\inferrule*[left=\llap{$\Rightarrow$Élim}]{ \inferrule*[left=\llap{$\Rightarrow$Int}]{ \inferrule*[left=\llap{$\Rightarrow$Int}]{ +\inferrule*[left=\llap{$\Rightarrow$Int}]{ +\inferrule*[left=\llap{$\Rightarrow$Élim}]{ +\inferrule*[left=\llap{$\Rightarrow$Élim}]{ \inferrule*[left=\llap{Ax}]{ }{\mbox{$\begin{array}{cc}\scriptscriptstyle B \Rightarrow A \Rightarrow C ,\\ \scriptscriptstyle A ,B \\ \end{array}$} \vdash B \Rightarrow A \Rightarrow C } \\ \inferrule*[right=\rlap{Ax}]{ }{\mbox{$\begin{array}{cc}\scriptscriptstyle B \Rightarrow A \Rightarrow C ,\\ \scriptscriptstyle A ,B \\ \end{array}$} \vdash B } @@ -2719,6 +2720,76 @@ $\bot$ \end{frame} % +\begin{frame} +\frametitle{Exemples de démonstrations en calcul des séquents} + +On reprend les mêmes exemples que dans le +transp. \ref{example-propositional-proofs} : +\vskip-5ex\leavevmode +\begin{center} +\begin{tabular}{c|c} +% +{\footnotesize +$ +\inferrule*[left={$\Rightarrow$R},right=\hphantom{Int}]{ +\inferrule*[left=\llap{$\land$R}]{ +\inferrule*[left=\llap{$\land$L$_2$}]{ +\inferrule*[left=\llap{Ax}]{ }{B \vdash B} +}{A\land B \vdash B} +\\ +\inferrule*[right=\rlap{$\land$L$_1$}]{ +\inferrule*[right=\rlap{Ax}]{ }{A \vdash A} +}{A\land B \vdash A} +}{A\land B \vdash B\land A} +}{\vdash A\land B \Rightarrow B\land A} +$ +} +& +{\footnotesize +$ +\inferrule*[left={$\Rightarrow$R},right=\hphantom{Int}]{ +\inferrule*[left=\llap{$\lor$L}]{ +\inferrule*[left=\llap{$\lor$R$_2$}]{ +\inferrule*[left=\llap{Ax}]{ }{A \vdash A} +}{A \vdash B\lor A} +\\ +\inferrule*[right=\rlap{$\lor$R$_1$}]{ +\inferrule*[right=\rlap{Ax}]{ }{B \vdash B} +}{B \vdash B\lor A} +}{A\lor B \vdash B\lor A} +}{\vdash A\lor B \Rightarrow B\lor A} +$ +} +\end{tabular} +\end{center} + +\medskip + +Et que dans le transp. \ref{example-proposition-proof-with-implication} : + +\vskip-2ex +{\footnotesize +\[ +\inferrule*[left=\llap{$\Rightarrow$R}]{ +\inferrule*[left=\llap{$\Rightarrow$R}]{ +\inferrule*[left=\llap{$\Rightarrow$R}]{ +\inferrule*[left=\llap{$\Rightarrow$L}]{ +\inferrule*[left=\llap{Ax}]{ }{A, B \vdash B } +\\ +\inferrule*[right=\rlap{$\Rightarrow$L}]{ +\inferrule*[left=\llap{Ax}]{ }{A , B \vdash A } +\\ +\inferrule*[right=\rlap{Ax}]{ }{C , A , B \vdash C } +}{A \Rightarrow C , A , B \vdash C } +}{B \Rightarrow A \Rightarrow C , A , B \vdash C } +}{B \Rightarrow A \Rightarrow C , A \vdash B \Rightarrow C } +}{B \Rightarrow A \Rightarrow C \vdash A \Rightarrow B \Rightarrow C } +}{\vdash (B \Rightarrow A \Rightarrow C ) \Rightarrow (A \Rightarrow B \Rightarrow C )} +\] +\par} + +\end{frame} +% % TODO: % - présentation en calcul des séquents % - élimination des coupures |