Problème de l'arrêt

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