Question sur le problème de l'arrêt

La meilleure de l'année a écrit:

Autrement dit la réalité est le juge suprême de toute science

Merci pour l'éclat de rire que tu vas provoquer chez 90% des lecteurs du forum. Hélas, bien sûr que non. La réalité, justement on ne la connait pas. Le juge (si on parle comme toi) des sciences est la preuve formelle (c'est à dire des textes qui ne cachent rien sous le tapis et mettent en gras ce qu'ils supposent sans le prouver)

Concernant le problème de l'arrêt, tu te compliques la vie.

Le programme

p:= [let a(x):= (if boucle (x(x)) then exit else lancer_une_boucle() ) in a(a)]

peut tout à fait être interrompu en débranchant la prise de courant.

Il n'en reste pas moins vrai que s'il s'arrête c'est parce qu'il a exécuté le "exit" face au test "boucle(p)", donc considéré que p ne s'arrête pas

De plus, si au bout d'un certain temps que tu estimes subjectivement assez long pour que le test a été consommé et que si ça ne s'est pas arrêté, c'est parce qu'il a exécuté le "else", tu te dois alors d'estimer qu'il a résolu le test "boucle(p)" en faux autrement dit qu'il considère que P s'arrête.

Mais il n'y avait rien ni de méchant ni d'acide. Qu'appellse tu "sérieux"? (Ici on est en sciences pas en philo: des philosophes "sérieux" qui contestent Godel il y en a plus que deux :-D )

Soit $E,S$ deux ensembles. Soit $p$ une application de $E^2$ dans $E$. Soit $C$ une partie de $E\times S$ (édité). Soient $\bf v,f$ deux éléments de $S$.

Il s'agit d'un modèle de calcul (vraiment dépouillé) avec des entrées ($E$) et des sorties $(S)$; $C$ désigne en fait l'ensemble des couples $(a,b)$ tels que si on soumet $a$ à la machine, le résultat $b$ est renvoyé.

On utilisera ici l'abréviation $x \to y$ à la place de $(x,y) \in C$.
On dira que deux $a,b$ dans $E$ donnent le même résultat si pour tout $r\in S$, $a\to r$ si et seulement si $b\to r$
( ($\spadesuit$) autrement dit -lorsque l'hypothèse A2 ci-dessous est satisfaite- s'il n'existe aucun $z$ tel que $a\to z$ ou $b \to z$ (édité), ou bien s'il existe un $t\in S$ tel que $a\to t$ et $b\to t$).

Pour faciliter la lecture on désignera par $u[v]$ l'élément $p(u,v)$ de $E$ dans la suite.

On suppose que

A1) $\mathbf v \neq \mathbf f$
A2) pour tout $x$ dans $E$ et tous $r,r'$ dans $S$, si $x \to r$ et $x \to r'$ alors $r=r'$ (édité) (unicité des résultats de calculs s'ils existent)
A3) pour tout $x$ dans $E$, il existe $x^*$ dans $E$ tel que pour tout $y$ dans $E$, $x^* [y]$ donne le même résultat que $x \left [ y [y]\right ] $(a.k.a. $p \left (x, p(y,y) \right )$).
A4) pour tous $c,m,n\in E$, il existe $i_{c,m,n}\in E$ tel que pour tout $x\in E$, si $c[x]\to \mathbf v$ (resp $c[x] \to \mathbf f$) alors $i_{c,m,n} [x]$ donne le même résultat que $m$ (resp. $n$) (le système supporte les boucles if).

Alors:

I°) Pour tout $x$ dans $E$, $x^* [x^*]$ et $x \left [x^* [x^*] \right ]$ donnent le même résultat (évident d'après A3).

II°) Soit $f:E \to \{\mathbf v, \mathbf f\}$ une fonction non constante telle que pour tous $x,y \in E$, si $x$ donne le même résultat que $y$, alors $f(x)=f(y)$. Alors il n'existe aucun $t\in E$ tel que pour tout $x\in E$, $t [x] \to f(x)$ ("théorème de Rice")

En effet ($f$ étant non constante) soient $k,\ell\in E$ tels que $f(k)=\mathbf v$ et $f(\ell)=\mathbf f$. Supposons qu'un tel $t$ existe et posons $e:=i_{t,\ell ,k}^* [ i_{t,\ell ,k}^*]$. Alors (cf I°) $i_{t,\ell,k} [e]$ et $e$ donnent le même résultat ($\clubsuit$).
Si $f(e)=\mathbf v$, alors $t [e] \to v$ donc d'après A3°, $\ell$ donne le même résultat que $i_{t,\ell,k} [e]$ qui donne le même résultat que $e$ d'après ($\clubsuit$). Donc $f(\ell)= f(e)$, or $f(e)=\mathbf v$ et $f(k)=\mathbf f$ ce qui est impossible.
Si $f(e)=\mathbf f$, on a une contradiction similaire: $t [e] \to f$ donc $k$ donne le même résultat que $i_{t,\ell,k} [e]$ d'après A3°), et $i_{t,\ell,k} [e]$ donne le même résultat que $e$ d'après ($\clubsuit$) et donc $f(k)=f(e)$ mais $f(k)=\mathbf v$ et $f(e)=\mathbf f$ ce qui ne peut pas arriver.
Bref il n'y a pas de tel $t$.

III°) On dit qu'un élément $x\in E$ s'arrête s'il existe $y\in S$ tel que $x\to y$.
S'il existe au moins un élément de $E$ qui ne s'arrête pas, alors il n'existe aucun $h\in E$ tel que pour tout $x\in E$,
$h[x] \to \mathbf t$ si $x$ s'arrête et $h[x] \to \mathbf f$ si $x$ ne s'arrête pas ("théorème de l'arrêt").
Supposons qu'un tel $h$ existe. Alors l'application $g$ qui à $x\in E$ fait correspondre $\mathbf v$ si $x$ s'arrête et $\mathbf f$ si $x$ ne s'arrête pas satisfait toutes les conditions du théorème II° (il est clair- cf remarque $(\spadesuit)$ en introduction que si $x$ et $y$ donnent le même résultat, alors $g(x)=g(y)$). Pour voir que $g$ est non constante, il suffit de voir que comme $h[x]$ s'arrête pour tout $x$ et donc $g(h[h])=\mathbf v$, d'autre part si $m\in E$ ne s'arrête pas (il en existe par hypothèse) alors $g(m)=\mathbf f$. Enfin on a par construction $h[x] \to g(x)$ pour tout $x\in E$ et donc on aboutit à une contradiction en appliquant le théorème II°).

@Foys : je suis bouché à l'émeri, ou alors il y a pas mal de trucs qui ne vont pas dans ce que tu as écrit ?

%%%%%%%%%%%%%%%%%%
> Soit $E,S$ deux ensembles. Soit $p$ une application de $E^2$ dans $E$.
> Soit $C$ une partie de $E$. Soient $\bf v,f$ deux éléments de $S$.
>
> Il s'agit d'un modèle de calcul (vraiment dépouillé) avec des entrées ($E$) et des
> sorties $(S)$; $C$ désigne en fait l'ensemble des couples $(a,b)$ tels que
> si on soumet $a$ à la machine, le résultat $b$ est renvoyé.

$C$ serait en fait une partie de $E\times S$ ???

%%%%%%%%%%%%%%%%
> On dira que deux $a,b$ dans $E$ donnent le même résultat si pour tout $r\in S$,
> $a\to r$ si et seulement si $b\to r$ ( ($\spadesuit$) autrement dit
> -lorsque l'hypothèse A2 ci-dessous est satisfaite- s'il n'existe aucun $z$ tel que $x\to z$ ou $y \to z$,
> ou bien s'il existe un $t\in S$ tel que $a\to t$ et $b\to t$).

$x$ et $y$ sont en fait $a$ et $b$ ?

%%%%%%%%%%%%%%%%%%%%%

> A2) pour tout $x$ dans $E$ et tous $r,r'$ dans $S$, $x\to r$ si et seulement $x\to r'$
> (unicité des résultats de calculs s'ils existent)

???????????

Si je comprends bien ce que tu voulais faire, ne pourrais-tu pas plutôt dire que tu ajoutes un élément, disons $\infty$, à $S$ et que tu as simplement une application de $E$ dans $S\cup\{\infty\}$ ? Ça éviterait tout ce mic-mac avec ton ensemble $C$ mal introduit, ta définition de "donner le même résultat" à coquille et ton axiome A2) foiré.

@emmch: ne crois pas qu'il y a besoin d'attendre un temps infini pour commenter la situation du programme en train de s'exécuter. "Commenter" est affaire textuel. La science est textuelle dans ses conclusions.

C'est corrigé!

Précisions: $abc$ abrège $(ab)c$

et pour $f$ on peut prendre ce qu'on veut, mais ici, on peut prendre :

$$ x\mapsto Z x uv$$

où $u$ est l'instruction "Stop" et $v$ n'importe quel programme dont il est évident qu'il boucle

$Z$ représente le candidat (qui n'existe "donc"** pas) vérifiant $Zx=K$ pour $x$ qui boucle et $Zx=KJ$ pour $x$ ne bouclant pas

Grace au point fixe $e$ tel que $e=Zeuv$ construit au post précédent.

C'est fait.

http://www.les-mathematiques.net/phorum/read.php?16,1008195,1730482,page=20#msg-1730482

Et le nom de la petite spécialité concerné est "logique combinatoire".

Elle est (pour des gens comme toi) largement préférable (même si elle raconte la même chose) au lambda calcul ou à la théorie des ensembles dans un premier temps, car elle n'est pas consommatrice de variables liées, notion grammaticale qui pose de nombreux problèmes aux étudiants généralistes.