Problème de l'arrêt

En théorie de la calculabilité, le problème de l'arrêt consiste, étant donné un programme informatique quelconque (au sens machine de Turing), à déterminer s'il finira par s'arrêter ou non.

Ce problème idéalisé n'est pas décidable, c'est-à-dire qu'il n'existe pas de programme informatique qui prendrait comme entrée tout code d'un programme informatique quelconque et qui grâce à la seule analyse de ce code — bien que celui-ci soit de taille finie — ressortirait VRAI si le programme s'arrête et FAUX sinon. Plus concrètement, on ne peut pas élaborer un compilateur capable de déterminer dans tous les cas si le programme bouclera indéfiniment ou non, bien qu'il soit cependant possible pour certaines séquences de codes identifiables de s'assurer que la construction génère potentiellement un bug. Ce résultat est généralisé par le théorème de Rice à de nombreuses autres propriétés concernant l'analyse des programmes.

Il ne s'applique toutefois qu'à ce cas théorique et il existe au contraire pour les programmes réels, s’exécutant sur une mémoire finie, des méthodes de détection de boucle infinie^[1], dont le slow-fast consistant à exécuter deux programmes en parallèle à raison de deux instructions dans l'un pour une dans l'autre et de comparer à chaque étape les états mémoire : quand on en trouve deux identiques, on est dans une boucle infinie et le programme ne saurait donc se terminer. Or le nombre d'états possibles d'une mémoire finie étant lui-même fini, bien que très grand, les configurations tomberont nécessairement en un temps fini sur un arrêt ou une boucle.

Preuve

Preuve classique

La preuve de ce résultat repose sur un argument diagonal, tout comme la preuve d'indénombrabilité des réels de Cantor (1891) et celle du théorème d'incomplétude de Gödel (1931).

Sans entrer dans le formalisme des machines de Turing, il suffit de savoir que toute machine de Turing (autrement appelée programme) peut prendre en entrée des chaînes de caractères "ch" (disons que les caractères autorisés sont "0" "1", et un autre par exemple "," ce n'est pas restrictif), effectue une suite d'opérations, et soit ne s'arrête jamais, soit s'arrête et renvoie une autre chaîne de caractères.

Par ailleurs, dans le cas général, tout programme PROG est également une chaîne de caractères, qui représente le codage de PROG, qui sera notée prog.

Supposons qu'il existe un programme HALT(P,X) tel que :

HALT(prog,ch) = \begin{cases} 1 & \text{si } \text{le programme }prog\mathrm{~s'arr\hat{e}te~sur~l'entr\acute{e}e~}ch, \\ 0 & \text{sinon.} \end{cases}

On pourrait alors construire le programme DIAGONALE suivant^[2] :

DIAGONALE(ch)

Si HALT(ch,ch)=1 alors faire une boucle infinie sinon terminer

Mais, on obtient une contradiction pour l'entrée diagonale. En effet, supposons que HALT(diagonale,diagonale)=1, ce qui signifie que le programme DIAGONALE s'arrête sur l'entrée diagonale. Dans ce cas, d'après le pseudo-code de DIAGONALE, DIAGONALE(diagonale) va boucler indéfiniment, ce qui est le contraire de l'hypothèse.

Inversement, si on suppose que HALT(diagonale,diagonale)=0, et donc que le programme DIAGONALE ne s'arrête pas sur l'entrée diagonale, alors DIAGONALE(diagonale) va s'arrêter immédiatement, ce qui est également contradictoire.

Finalement, on a prouvé que si l'on suppose l'existence de HALT, on a l'existence de DIAGONALE qui contredit son fonctionnement. Cela prouve donc par l'absurde que HALT n'existe pas.

Ceci est la preuve classique du problème de l'arrêt par argument diagonal, fondée sur l'idée utilisée par Turing dans son article fondateur de 1936 (page 247).

Preuve de Gregory Chaitin

Une autre preuve fondée sur une idée légèrement différente a été établie par Gregory Chaitin^[3]. Cette preuve est également une démonstration par l'absurde, partant de l'hypothèse que HALT(prog), déterminant si le programme PROG s'arrête, existe.

Imaginons le programme PARADOXE qui énumère tous les programmes dont la taille est plus petite que 10 fois^[4] la taille de PARADOXE, et qui exécute la fonction HALT sur tous ces programmes. PARADOXE exécute les programmes qui s'arrêtent et mémorise leur résultat. PARADOXE dresse ainsi une liste de tous les résultats possibles que peuvent retourner toutes les machines de Turing qui s'arrêtent et dont la taille est inférieure à 10 fois la taille de PARADOXE. À partir de cette liste, PARADOXE détermine le plus petit entier positif n'appartenant pas à cette liste, et termine en retournant cet entier.

Mais, PARADOXE se terminant inévitablement, le résultat retourné par PARADOXE devrait se trouver dans la liste de tous les résultats possibles des machines de Turing qui se terminent et dont la taille est inférieure à 10 fois la taille de PARADOXE, ce qui n'est pas le cas par construction de PARADOXE qui retourne un nombre n'appartenant pas à cette liste.

On démontre ainsi l'impossibilité de l'existence de HALT.

Un raisonnement similaire démontre qu'aucun programme de taille sensiblement inférieure à N bits ne peut résoudre le problème de l'arrêt pour tous les programmes dont la taille est inférieure à N bits^[3]. Ce qui signifie que même si HALT pouvait exister, sa taille croitrait vers l'infini à mesure que la taille des programmes qu'il devrait tester croitrait aussi vers l'infini.

Conséquences

Le problème de l'arrêt a de nombreuses conséquences en informatique théorique :

Il existe un ensemble d'entiers naturels récursivement énumérable qui n'est pas un ensemble récursif. En termes plus simples, il existe un ensemble d'entiers dont on peut produire la liste exhaustive par un algorithme, mais pour lequel il n'existe pas de programme permettant de dire sans faillir si un entier appartient à cet ensemble ou non.

Cela traduit le fait qu'un sens du problème de l'arrêt est facile (si une machine de Turing s'arrête, on finit évidemment par le savoir), alors que l'autre est impossible. Par ailleurs un théorème profond de Yuri Matiyasevich (fondé sur des travaux de Julia Robinson) assure que tout ensemble récursivement énumérable est diophantien, et la réciproque est facile. (Un ensemble E de nombre entiers est diophantien s'il existe un polynôme à plusieurs variables qui possède une solution entière si et seulement si la valeur de sa première inconnue est dans E). En prenant un ensemble diophantien non récursif (le problème de l'arrêt nous en assure l'existence), on montre ainsi qu'il n'existe aucun algorithme qui peut indiquer si un polynôme à plusieurs variables donné admet une solution constitué d'entiers. C'est en fait la réponse au dixième problème de Hilbert sur la résolubilité des équations diophantiennes.

Une autre application est une forme faible du théorème d'incomplétude de Gödel sur l'existence d'énoncés vrais mais non démontrables. Cette application est qu'il existe une machine de Turing T et une entrée e telles que T ne s'arrête pas sur e mais qu'aucune preuve n'existe du fait que T ne s'arrête pas sur e. En effet, l'argument peut se faire en raisonnant par l'absurde. Supposons que pour toute paire (T,e) telle que T ne s'arrête pas sur e, il existe une preuve de ce fait. Considérons maintenant l'algorithme A suivant. Étant donnée une paire (T,e), l'algorithme A effectue deux procédures en parallèle. La première exécute T sur l'entrée e (pour vérifier si cela s'arrêterait). La seconde énumère toutes les preuves mathématiques logiquement valides à la recherche d'une preuve que T ne s'arrêterait pas sur e, et s'arrête si elle en trouve une. On décrète que A s'arrête dès que l'une des deux procédures s'est arrêté. D'après notre hypothèse (du raisonnement par l'absurde), l'une des deux procédures doit s'arrêter. Ainsi A s'arrête pour toutes les entrées (T,e). Selon que l'arrêt de A est causé par l'arrêt de la première ou de la seconde procédure, on déduit si T s'arrête sur e ou pas (ici on suppose implicitement le système consistant, c'est-à-dire que les preuves valides ne montrent que des choses vraies). L'algorithme A est donc une solution du problème de l'arrêt-- contradiction. Il convient de remarquer que cet argument ne permet pas de savoir qui sont T et e, mais juste qu'ils existent. On peut appliquer cet argument à tous les problèmes algorithmiquement indécidables.

De très nombreux problèmes en informatique, notamment concernant l'analyse statique de programmes, sont équivalents au problème de l'arrêt. On le montre là encore en réduisant la résolution du problème de l'arrêt à celle du problème étudié.

Citons par exemple le problème du ramasse-miettes : on cherche à libérer des zones mémoires juste après leur dernière utilisation. Ce problème est équivalent à celui de l'arrêt. La réduction est simple : soit P un programme dont on veut tester l'arrêt ; considérons le programme :

créer une zone mémoire ''X'' (jamais utilisée dans ''P'')
exécuter ''P''
écrire dans ''X''.

Clairement, la zone mémoire X sert après sa création si et seulement si P termine. Donc, si on savait déterminer automatiquement au vu de la lecture du programme si on peut libérer X juste après son allocation, on saurait si P termine. Cela est impossible, donc il n'existe aucun algorithme de ramasse-miettes optimalement précis.

Variante

Le problème de l'arrêt est en théorie décidable dans le cas d'une mémoire de taille finie, car l'ensemble des états de la mémoire, bien que très grand, est fini lui-même. Or, dans le cas d'une mémoire finie, les états successifs de la mémoire finissent toujours par se répéter quand le programme ne s'arrête pas, avec un cycle de répétition au plus égal au nombre d'états possibles de la mémoire^[5]. En effet, une machine de Turing étant déterministe, si un même état de mémoire se présente de nouveau, alors l'état suivant est nécessairement toujours celui déterminé par l'état précédent et ainsi de suite, et un cycle s'ensuit inévitablement.

Il est donc théoriquement possible de déterminer si la machine à mémoire finie boucle ou non en un temps fini. Un algorithme possible est celui du slow-fast^[6]. Ce calcul doit cependant être effectué par un superviseur examinant en permanence les deux processus, et leur donnant le contrôle instruction par instruction pour l'un, deux instructions par deux instructions pour l'autre.

Le nombre exponentiellement élevé de combinaisons des états d'une mémoire limite dans la pratique cette méthode à de petits programmes comportant moins d'un millier de données scalaires (les instructions n'ont pas à être examinées si elles sont dans des segments protégés contre l'écriture, et donc ne varient jamais). C'est typiquement le cas des calculs par corrections successives d'un pangramme autodescriptif, qui ne décrivent qu'un sous-ensemble extrêmement petit des états mémoires possible.

Ce résultat qui concerne les machines finies ne contredit en rien la démonstration générale, qui porte sur des machines infinies n'existant pas dans la pratique.

Notes et références

Notes

Références

↑ http://groups.csail.mit.edu/pac/jolt/
↑ Pseudo-code classique. Voir par exemple Harry R. Lewis Elements of the theory of computation Prentice-Hall 1998 p. 251 "The halting problem"
1 2 Gregory Chaitin The limits of reason Scientific American 2006
↑ Le facteur dépend du langage informatique utilisé. Le facteur 10 est à titre d'exemple et est celui utilisé dans la source
↑ Marvin Minsky, Computation, Finite and Infinite Machines, Prentice-Hall, Inc., N.J., 1967. Chapitre 8, Section 8.2 "The Unsolvability of the Halting Problem"
↑ Cours de Jacques Arsac, Paris VI

Annexes

Bibliographie

(en) Alan Turing, « On Computable Numbers, with an Application to the Entscheidungsproblem », Proc. London Math. Soc., 2^e série, vol. 42,‎ 1937, p. 230-265 (DOI 10.1112/plms/s2-42.1.230) et « [idem] : A Correction », Proc. London Math. Soc., 2^e série, vol. 43,‎ 1938, p. 544-546 (DOI 10.1112/plms/s2-43.6.544, lire en ligne)
L'article fondateur où Turing définit les machines de Turing, formule le problème de l'arrêt, et démontre qu'il ne possède pas de solution (ainsi que l'Entscheidungsproblem).

Portail de l'informatique théorique

This article is issued from Wikipédia - version of the Wednesday, October 21, 2015. The text is available under the Creative Commons Attribution/Share Alike but additional terms may apply for the media files.