Arrêter le problème - un problème qui me dérange

À ma connaissance, l'arrêt du problème demande s'il existe un programme qui décide si un programme en cours de test, compte tenu de certaines données d'entrée (quel que soit le programme ou quelles données d'entrée nous donnons) se terminera ou non. La réponse à ce problème est «non». En d'autres termes, il n'y a pas de programme «unique» qui puisse le vérifier pour toutes les paires possibles (certains algorithmes, certaines données d'entrée).

Mais cela ne signifie pas que nous ne pouvons pas décider si un programme particulier X se terminera ou non.

Je ne peux pas encore commenter d'autres réponses, mais l' une d'elles a attiré mon attention:

Concrètement, c'est important car cela vous permet de dire à vos patrons ignorants "ce que vous demandez est mathématiquement impossible".

Peut-être pouvez-vous me dire ce que cette personne voulait dire? Dans mon scénario, mon patron ignorant peut me demander de vérifier (en fait, prouver ou réfuter) si mon programme (c'est un programme particulier) va se terminer ou non. Et bien sûr, il existe des paires (algorithme, données d'entrée) dont on peut prouver qu'elles se terminent (ou ne se terminent jamais).

La question est - puis-je le prouver séparément pour chaque paire (programme, données d'entrée)? Même si la réponse est oui, alors il y a un problème - il peut y avoir une infinité de «données d'entrée». Il est donc tout à fait naturel de demander - puis-je prouver, pour chaque algorithme, que cet algorithme se terminera (ou l'inverse), quelles que soient les données d'entrée que je fournis?

computability halting-problem user4205580
la source

La question de savoir si nous pouvons trouver toutes ces preuves est une question de logique, mais il y en a certainement beaucoup que nous n'avons pas encore trouvées .

Raphael

le problème d'arrêt est défini comme un algorithme spécifique qui peut déterminer si un programme s'arrêtera ou non. Vérifier un programme spécifique (ou même plusieurs programmes spécifiques) avec différents algorithmes s'ils peuvent s'arrêter ou non est faisable (le cas général n'est pas)

Nikos M.

Réponses:

Non, vous ne pouvez pas le prouver pour chaque algorithme (machine de Turing). Cela devient une question sur la nature des preuves plutôt qu'une question sur le calcul.

Considérez la machine de Turing suivante $M(x)$ : vérifier s'il existe une preuve de la déclaration $\forall x \hspace{1mm} M(x)$ haltes, de longueur $\le |x|$ (pour des explications sur l'auto-référence, voir le théorème de récursion de Klenee). Si une telle preuve est trouvée, entrez dans une boucle infinie (sinon arrêtez).

De toute évidence, vous ne pouvez pas prouver $M(x)$ s'arrête pour tous $x$ , car si vous pouvez trouver une preuve de longueur $p$ , il ne s'arrêtera pas pour toutes les entrées de taille $\ge p$ . De plus, vous ne pouvez pas prouver $M(x)$ ne s'arrête pas pour certains $x$ , car cela signifierait qu'il existe une preuve de l'arrêt de la $M$ sur toutes les entrées (contradiction). La situation ici est que si notre système d'axiomes est cohérent, alors $M(x)$ s'arrête pour tous $x$ , mais vous ne pouvez pas le prouver (ce qui signifie que vous pouvez le prouver dans votre théorie $T$ que si $T$ est cohérent alors $\forall x \hspace{1mm} M(x)$ s'arrête, mais vous ne pouvez pas prouver qu'il s'arrête sans cette hypothèse, sauf si votre système est incohérent).

Ariel
la source

C'est la réponse à «puis-je prouver, pour chaque algorithme, que cet algorithme se terminera (ou l'inverse), quelles que soient les données d'entrée que je fournis? - Juste pour en être certain.

user4205580

Oui. Besoin de plus de personnages

Ariel

Vous pourriez également être intéressé par les résultats d'incomplétude de Godel : fondamentalement, dans tout système logique suffisamment puissant pour parler d'arithmétique, il y a des affirmations qui sont vraies et qui ne peuvent pas être prouvées.

jmite

M

$M$ - machine de turing,

x

$x$ - son entrée. Ensuite, nous l'exécutons avec, disons,

x = 2

$x=2$ . Le programme se traduit par: "vérifier s'il existe une preuve pour la déclaration: pour tous

2

$2$ M (2) haltes, de longueur

\leq 2

$\le 2$ ... "Ça n'a pas de sens de dire pour tous

2

$2$ . Ou peut-être que ce n'est pas comme ça que je devrais le voir.

user4205580

La variable quantifiée est nouvelle, pensez-y comme

\forall y M (y)

$\forall y M(y)$ s'arrête.

x

$x$ (l'entrée) n'apparaît que comme limite de la longueur de l'épreuve.

Ariel

Pour un programme spécifique, je peux certes prouver que le programme s'arrêtera sur toutes les entrées: mon programme a "arrêt" comme première instruction.

Un autre exemple: je peux avoir un programme spécifique qui est un simulateur de machine de Turing (c'est-à-dire une machine de Turing universelle). Il interprète son entrée comme une description d'une machine de Turing, et le simulateur simule la machine fonctionnant sur une bande vierge. Ainsi, le simulateur s'arrêtera si la machine en cours d'entrée s'arrête et fonctionnera indéfiniment si la machine en cours d'entrée fonctionne indéfiniment. (Si l'entrée n'est pas au format correct pour décrire une machine de Turing, le simulateur s'arrête.)

Nous savons qu'il est impossible de décider si une machine Turing arbitraire s'arrête lorsqu'elle est démarrée sur une bande vierge. Donc, pour ma machine de simulation spécifique, il n'y a pas d'algorithme pour décider de ce qu'il fait sur une entrée arbitraire.

Je ne sais pas si ces deux exemples aident.

Certes, dans de nombreux domaines problématiques, il est raisonnable de pouvoir prouver que des programmes spécifiques se terminent. Si mon programme multiplie deux matrices, je m'attendrais à pouvoir prouver qu'il n'y a aucun moyen qu'il puisse durer éternellement.

user42735
la source

Je peux au moins clarifier la question hypothétique que le patron imaginaire est censé poser et qui mène à cette réponse:

Pouvez-vous concevoir un programme qui prend cet autre programme / modèle / requête de base de données / etc. qui détermine toujours s'il termine / déclenche une exception / manque de mémoire?

Le point de la preuve de l'impossibilité est qu'une telle tâche ne peut pas être accomplie. Bien sûr, il est de notoriété publique aujourd'hui qu'une telle tâche peut être assez bien approchée , c'est-à-dire qu'il est possible de donner un algorithme qui détermine si un programme va lever une exception, mais parfois répond "pourrait lever une exception" même si le programme ne fait pas ne le fais pas dans la pratique .

Certains d'entre eux sont également plus difficiles à faire dans la pratique, par exemple, la terminaison est beaucoup plus difficile à prouver que l'absence d'exception de pointeur nul pour les "programmes du monde réel" (mais équivalente en théorie).

cody
la source