diff options
| -rw-r--r-- | transp-inf110-02-typage.tex | 97 |
1 files changed, 91 insertions, 6 deletions
diff --git a/transp-inf110-02-typage.tex b/transp-inf110-02-typage.tex index 64f597f..cd3857a 100644 --- a/transp-inf110-02-typage.tex +++ b/transp-inf110-02-typage.tex @@ -2939,8 +2939,8 @@ dans $\Gamma\vdash P$ et à gauche dans $\Gamma,P\vdash Q$ \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 +\itempoint Cas « déplaçants » : 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} @@ -2988,8 +2988,8 @@ $\mpdotsabove{\Gamma\vdash Q}$ \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 +\itempoint Cas « principaux » : 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 : @@ -3031,9 +3031,94 @@ $\inferrule*[left={\color{purple}Cut}]{ \end{frame} % +\begin{frame} +\frametitle{Élimination des coupures : récurrence} + +\itempoint Le \textbf{degré} $\deg P$ d'une formule propositionnelle +est : $0$ pour une variable propositionnelle ou $\top$, $\bot$, et +$\max(\deg P_1, \deg P_2) + 1$ si $P = P_1 \circ P_2$ pour un +connecteur $\circ \in \{\Rightarrow, \land, \lor\}$. C'est donc la +profondeur de l'arbre de cette formule. + +\smallskip + +{\footnotesize P.ex., $\deg(((A\Rightarrow B)\Rightarrow A)\Rightarrow + A) = 3$.\par} + +\medskip + +\itempoint Le degré d'une coupure est le degré de la formule coupée. +Le \textbf{degré de coupure} d'une démonstration en calcul des +séquents est le plus grand degré d'une coupure (ou $-1$ s'il n'y en a +pas). Une \textbf{coupure critique} est une coupure de degré +maximal. + +\medskip + +\itempoint La preuve de l'élimination des coupures se fait par une +\alert{double récurrence} : +\begin{itemize} +\item récurrence principale sur le degré de coupure de la + démonstration, +\item récurrence secondaire, à degré donné, sur la somme des hauteurs + des deux branches de la coupure à éliminer. +\end{itemize} + +\medskip + +\itempoint La démonstration est constructive (algorithmique) ; +l'algorithme esquissé est p.r. (même « élémentaire »). Il n'est pas +déterministe {\footnotesize (ni même confluent)}. + +\end{frame} +% +\begin{frame} +\frametitle{Élimination des coupures : conséquences} + +{\footnotesize\textcolor{blue}{Quel intérêt de pouvoir éliminer les + coupures ?} Les preuves sans coupure ne peuvent pas faire + apparaître de formule inattendue.\par} + +\medskip + +\itempoint\textbf{Propriété de la disjonction :} si $\vdash Q_1\lor +Q_2$ (\alert{sans hypothèse !}) alors $\vdash Q_1$ ou bien $\vdash +Q_2$. {\footnotesize (\underline{Preuve :} une démonstration sans + coupure de $\vdash Q_1\lor Q_2$ doit finir par la règle $\lor$R$_1$ + ou $\lor$R$_2$. \qedsymbol)} + +\medskip + +\itempoint\textbf{Corollaire :} $\vdash A\lor\neg A$ n'est pas +prouvable en logique intuitionniste. + +\medskip + +\itempoint\textbf{Propriété de la sous-formule :} si $P_1,\ldots,P_r +\vdash Q$ alors une preuve sans coupure ne fait intervenir que des +formules qui sont des \alert{sous-formules} de $P_1,\ldots,P_r$ ou +$Q$. {\footnotesize (\underline{Preuve :} c'est clair sur chacune des + règles. \qedsymbol)} + +\medskip + +\itempoint\textbf{Corollaire :} on peut \alert{décider + algorithmiquement} si $P_1,\ldots,P_r \vdash Q$. + +\smallskip + +{\footnotesize\underline{Algorithme :} construire l'ensemble $\Phi$ de + toutes les sous-formules d'une de $P_1,\ldots,P_r$ ou $Q$, et + l'ensemble de tous les séquents possibles $\Gamma\vdash R$ avec + $\Gamma\subseteq\Phi$ et $R\in\Phi$. Marquer comme « valables » + ceux qui découlent de séquents déjà marqués comme valables par + application d'une des règles du calcul des séquents (autre que la + coupure), et répéter jusqu'à ce que le séquent recherché ait été + marqué ou que plus aucun séquent ne soit marqué.\qed\par} + +\end{frame} +% % TODO: -% - présentation en calcul des séquents -% - élimination des coupures % - Kripke % - fragment négatif % - call/cc |