diff options
| -rw-r--r-- | exercices-inf110.tex | 120 |
1 files changed, 119 insertions, 1 deletions
diff --git a/exercices-inf110.tex b/exercices-inf110.tex index e6c7867..f492d9d 100644 --- a/exercices-inf110.tex +++ b/exercices-inf110.tex @@ -1039,7 +1039,7 @@ récursive.) % -\exercice\ (${\star}{\star}$)\par\nobreak +\exercice\label{exercise-computably-inseparable-sets}\ (${\star}{\star}$)\par\nobreak On dira que deux parties $L,M$ de $\mathbb{N}$ disjointes (c'est-à-dire $L\cap M = \varnothing$) sont \textbf{calculablement @@ -2529,6 +2529,124 @@ le serait, or elles ne sont même pas prouvables classiquement). \end{corrige} +\exercice\ (${\star}{\star}{\star}{\star}$)\par\nobreak + +En prenant connaissance du résultat de +l'exercice \ref{exercise-computably-inseparable-sets}, montrer que la +formule suivante (« axiome de Kreisel-Putnam ») n'est pas réalisable : +\[ +(\neg A \Rightarrow B\lor C) \Rightarrow +(\neg A\Rightarrow B) \lor (\neg A\Rightarrow C) +\] +(On pourra supposer par l'absurde qu'il y a un programme $r$ qui +réalise cette formule, et chercher à s'en servir pour séparer les +ensembles $L$ et $M$ définis dans +l'exercice \ref{exercise-computably-inseparable-sets}. +\emph{Indication :} plus précisément, on pourra poser $B_z$ comme +valant $\mathbb{N}$ si $z\in L$ et $\varnothing$ sinon ; $C_z$ comme +valant $\mathbb{N}$ si $z\in M$ et $\varnothing$ sinon ; et $A_z$ +comme valant $\varnothing$ si $z\in L\cup M$ et $\mathbb{N}$ sinon ; +et chercher à définir un élément de $(\dottedneg A_z \dottedlimp +B_z\dottedlor C_z)$ auquel appliquer $r$.) + +\begin{corrige} +Supposons par l'absurde qu'il existe (un \emph{même}) $r$ qui réalise +$(\neg A \Rightarrow B\lor C) \Rightarrow (\neg A\Rightarrow B) \lor +(\neg A\Rightarrow C)$, c'est-à-dire qui appartienne à $(\dottedneg A +\dottedlimp B\dottedlor C) \dottedlimp (\dottedneg A\dottedlimp B) +\dottedlor (\dottedneg A\dottedlimp C)$ quels que soient +$A,B,C\subseteq \mathbb{N}$ (où $P \dottedlor Q = \{\langle 0,m\rangle +: m\in P\} \cup \{\langle 1,n\rangle : n\in Q\}$ et $(P \dottedlimp Q) += \{e \in \mathbb{N} : \varphi_e(P){\downarrow} \subseteq Q\}$, et on +se rappelle bien sûr que $\dottedneg P = (P\dottedlimp \varnothing)$ +vaut $\mathbb{N}$ si $P$ est vide et $\varnothing$ si $P$ n'est pas +vide). + +On pose $L := \{\langle e,x\rangle : \varphi_e(x){\downarrow} = 1\}$ +et $M := \{\langle e,x\rangle : \varphi_e(x){\downarrow} = 2\}$. On a +vu dans l'exercice \ref{exercise-computably-inseparable-sets} qu'il +n'existe aucun programme $s$ qui, prenant en entrée un +$z\in\mathbb{N}$, termine toujours en temps fini, et renvoie « vrai » +lorsque $z \in L$ et « faux » lorsque $z \in M$ (et une réponse +quelconque, lorsque $z \not\in L\cup M$, mais le programme doit quand +même terminer). Or on va utiliser $r$ pour faire précisément une +telle chose, ce qui constituera une contradiction. + +Définissons les ensembles $A_z,B_z,C_z$ pour $z = \langle e,x\rangle$ +comme suit : +\[ +\begin{aligned} +A_z &= \varnothing \text{~si~$\varphi_e(x){\downarrow} = 1$ ou + $\varphi_e(x){\downarrow} = 2$,}\\ +&= \mathbb{N} \text{~sinon}\\ +\text{(donc~}\dottedneg A_z &= \mathbb{N} \text{~si~$\varphi_e(x){\downarrow} = 1$ ou + $\varphi_e(x){\downarrow} = 2$,}\\ +&= \varnothing \text{~sinon)}\\ +B_z &= \mathbb{N} \text{~si~$\varphi_e(x){\downarrow} = 1$,}\\ +&= \varnothing \text{~sinon}\\ +C_z &= \mathbb{N} \text{~si~$\varphi_e(x){\downarrow} = 2$,}\\ +&= \varnothing \text{~sinon}\\ +\end{aligned} +\] + +Donné $z\in \mathbb{N}$, considérons le programme $p_z$ défini comme +suit. Il prend un unique argument, qu'il ignore. Il décode le couple +$z = \langle e,x\rangle$, puis il exécute $\varphi_e(x)$ (au moyen +d'un interpréteur universel). Si $\varphi_e(x){\downarrow} = 1$, il +renvoie $\langle 0,0\rangle$, et si $\varphi_e(x){\downarrow} = 2$, il +renvoie $\langle 1,0\rangle$ ; dans tout autre cas, il fait une boucle +infinie (y compris bien sûr si $\varphi_e(x){\uparrow}$, c'est-à-dire +si l'exécution ne termine jamais : dans ce cas forcément $p_z$ ne +termine pas non plus). + +On remarque que $p_z$ est construit algorithmiquement en fonction +de $z$ (par le théorème s-m-n si on veut). + +Par construction, si on passe à $p_z$ un argument de $\dottedneg A_z$, +ce qui implique que $\varphi_e(x){\downarrow} = 1$ ou +$\varphi_e(x){\downarrow} = 2$ (l'argument est une \emph{promesse} de +ce fait), alors il renvoie un élément de $B_z \dottedlor C_z$ (à +savoir un couple $\langle 0,n\rangle$ avec $n\in B_z$ ou $\langle +1,n\rangle$ avec $n\in C_z$). On a donc $p_z \in (\dottedneg A_z +\dottedlimp B_z\dottedlor C_z)$. + +Par hypothèse sur $r$, on doit donc avoir $\varphi_r(p_z)$ défini et +appartenant à $(\dottedneg A_z\dottedlimp B_z) \dottedlor (\dottedneg +A_z\dottedlimp C_z)$. Notamment, $\varphi_r(p_z)$ est (le codage +d')un couple dont la première coordonnée vaut $0$ ou $1$ et indique si +la seconde est dans $\dottedneg A_z\dottedlimp B_z$ ou dans +$\dottedneg A_z\dottedlimp C_z$. On considère le programme $s$ qui +prend un $z$ en entrée, calcule $\varphi_r(p_z)$ (noter que ce calcul +est bien algorithmique puisque $p_z$ est construit algorithmiquement +en fonction de $z$, et il termine toujours d'après ce qu'on vient de +dire), et renvoie « vrai » si la première coordonnée du résultat +vaut $0$ et « faux » si la seconde coordonnée du résultat vaut $1$. + +Si $z = \langle e,x\rangle$ avec $\varphi_e(x){\downarrow} = 1$, alors +$C_z = \varnothing$ et $\dottedneg A_z = \mathbb{N}$, donc +$(\dottedneg A_z\dottedlimp C_z) = \varnothing$, donc $\varphi_r(p_z)$ +doit forcément être de la forme $\langle 0,\cdots\rangle$, et $s$ +renvoie « vrai » sur l'entrée $z$. Symétriquement, si $z = \langle +e,x\rangle$ avec $\varphi_e(x){\downarrow} = 2$, alors $(\dottedneg +A_z\dottedlimp B_z) = \varnothing$ donc $\varphi_r(p_z)$ doit +forcément être de la forme $\langle 1,\cdots\rangle$, et $s$ renvoie +« faux » sur l'entrée $z$. + +Donc $s$ termine toujours, et sépare $L$ et $M$ puisqu'il renvoie +« vrai » sur le premier et « faux » sur le second. Ceci contredit le +fait que $L$ et $M$ sont récursivement inséparables. On a abouti à +une contradiction : c'est qu'en fait $r$ n'existait pas. + +(La formule de Kreisel-Putnam n'est donc pas réalisable. En +particulier, par \emph{correction} de la sémantique de la +réalisabilité, elle n'est pas démontrable dans le calcul +propositionnel intuitionniste, c'est-à-dire, par Curry-Howard, qu'il +n'y a pas de terme du $\lambda$-calcul simplement typé ayant pour type +$(\neg A \Rightarrow B\lor C) \Rightarrow (\neg A\Rightarrow B) \lor +(\neg A\Rightarrow C)$.) +\end{corrige} + + % % % |