Problème de l'arrêt

L'animation illustre une machine impossible : il n'y a pas de machine qui lit n'importe quel code source d'un programme et dit si son exécution termine ou non.

En théorie de la calculabilité, le problème de l'arrêt est le problème de décision qui détermine, à partir d'une description d'un programme informatique, et d'une entrée, si le programme s'arrête avec cette entrée ou non.

Alan Turing a montré en 1936 que le problème de l'arrêt est indécidable, c'est-à-dire qu'il n'existe pas de programme informatique qui prend comme entrée une description d'un programme informatique et un paramètre et qui, grâce à la seule analyse de ce code, répond VRAI si le programme s'arrête sur son paramètre et FAUX sinon. Une partie importante de la démonstration a été la formalisation du concept de programmes informatiques : les machines de Turing.

En pratique, il n'y a donc pas de méthode générale d'analyse statique capable de déterminer si un programme boucle 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 une boucle infinie. 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.

Indécidabilité du problème de l'arrêt

Preuve classique

Donnons ici la preuve de ce résultat fondée sur l'idée utilisée par Turing dans son article fondateur de 1936 (page 247). Elle 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) prend en entrée des mots finis $m$ sur un alphabet fini. Par ailleurs, on décrit un programme (machine de Turing) par un mot fini prog, qui représente son codage.

Montrons par l'absurde que le problème de l'arrêt est indécidable. Supposons qu'il existe un programme halt qui décide le problème de l'arrêt. C'est-à-dire :

• Si prog(m) s'arrête, alors halt accepte (prog, m) en un temps fini ;
• Si prog(m) ne s'arrête pas, alors halt refuse (prog, m) en un temps fini.

On construit le programme diagonale suivant :

procedure diagonale(x):
    si halt accepte (x, x)
        boucle infinie
    sinon
        accepter

Mais, on obtient une contradiction pour l'entrée diagonale. En effet, diagonale(diagonale) boucle à l'infini si et seulement si halt accepte (diagonale, diagonale), c'est-à-dire si et seulement si diagonale(diagonale) termine. Cela prouve donc par l'absurde que halt n'existe pas.

Preuve de Gregory Chaitin

Une autre preuve fondée sur une idée légèrement différente a été établie par Gregory Chaitin. 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 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. Ce qui signifie que même si HALT pouvait exister, sa taille croîtrait 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 nombres 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ée 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é 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, seulement 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.

Variantes

Arrêt uniforme

On peut s'intéresser à savoir si une machine s'arrête depuis toute configuration (pas forcément des configurations initiales). Le problème est appelé le problème de l'arrêt uniforme et il est également indécidable.

Mémoire de taille finie

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. 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. 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.

Annexes

Bibliographie

• (en) Alan Turing, On Computable Numbers, with an Application to the Entscheidungsproblem : Proceedings of the London Mathematical Society, London Mathematical Society, 1937 (DOI 10.1112/PLMS/S2-42.1.230, lire en ligne) 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).
• Olivier Ridoux et Gilles Lesventes, Calculateurs, calculs, calculabilité, Dunod, coll. « Sciences sup », 2008, 204 p. (ISBN 978-2-10-051588-2), chap. 3 (« Le problème de l'arrêt »)