Voir la source de Problème de l'arrêt

[[Fichier:Programme impossible qui teste si un programme s'arrête sur son entrée.gif|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'[[terminaison d'un algorithme|arrête]] avec cette entrée ou non.

[[Alan Turing]] a montré en 1936 que le problème de l'arrêt est [[Décidabilité|indécidable]]<ref>{{Article|langue=en|prénom1=A. M.|nom1=Turing|titre=On Computable Numbers, with an Application to the Entscheidungsproblem|périodique=Proceedings of the London Mathematical Society|volume=s2-42|numéro=1|date=1937-01-01|issn=1460-244X|doi=10.1112/plms/s2-42.1.230|lire en ligne=http://onlinelibrary.wiley.com/doi/10.1112/plms/s2-42.1.230/abstract|consulté le=2017-11-27|pages=230–265}}</ref>, 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 [[machine de Turing|machines de Turing]].

En pratique, il n'y a donc pas de méthode générale d'[[Analyse statique de programmes|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 [[Alan Turing|Turing]] dans son article fondateur de 1936 (page 247). Elle repose sur un [[Argument de la diagonale de Cantor|argument diagonal]]<ref name="Vollat">{{ouvrage|auteur=P. Vollat|titre=Calculabilité effective et algorithmique théorique Broché|date= 1989|éditeur=Eyrolles|pages=186 |isbn=2212081685}}</ref>, tout comme la preuve d'[[Argument de la diagonale de Cantor|indénombrabilité des réels de Cantor (1891)]] et celle du [[Théorèmes d'incomplétude de Gödel|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 <math>m</math> 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 [[Raisonnement par l'absurde|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<ref>Pseudo-code classique. Voir par exemple [[Harry R. Lewis]], ''{{Langue|en|Elements of the Theory of Computation}}'', Prentice-Hall, 1998, {{p.|251}}, « {{Langue|en|The halting problem}} ».</ref> :

<syntaxhighlight lang="pascal">
procedure diagonale(x):
    si halt accepte (x, x)
        boucle infinie
    sinon
        accepter
</syntaxhighlight>

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]]<ref name="chaitin-limit">[[Gregory Chaitin]] ''The limits of reason'' Scientific American 2006</ref>. Cette preuve est également une [[Raisonnement par l'absurde|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 {{nobr|10 fois}}<ref>Le facteur dépend du langage informatique utilisé. Le facteur 10 est à titre d'exemple et est celui utilisé dans la source</ref> 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 à {{nobr|10 fois}} la taille de ''PARADOXE''. À partir de cette liste, ''PARADOXE'' détermine le plus petit [[entier naturel]] 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 à {{nobr|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<ref name="chaitin-limit"/>. 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 {{incise|contradiction|stop}}. 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 (informatique)|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 (complexité)|réduction]] est simple : soit ''P'' un programme dont on veut tester l'arrêt ; considérons le programme :
<pre>
créer une zone mémoire ''X'' (jamais utilisée dans ''P'')
exécuter ''P''
écrire dans ''X''.
</pre>
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<ref>{{Article|prénom1=Gabor T.|nom1=Herman|titre=A simple solution of the uniform halting problem|périodique=Journal of Symbolic Logic|volume=34|date=1969-11-01|issn=1943-5886|doi=10.2307/2270856|lire en ligne=http://journals.cambridge.org/article_S0022481200093208|consulté le=2016-05-26|pages=639–640}}</ref>.

=== 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''<ref>{{lien web |titre=Jolt |url=http://groups.csail.mit.edu/pac/jolt/ |site=mit.edu |consulté le=27-04-2023}}.</ref>, 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<ref>[[Marvin Minsky]], ''Computation, Finite and Infinite Machines'', Prentice-Hall, Inc., N.J., 1967. Chapitre 8, Section 8.2 "The Unsolvability of the Halting Problem"</ref>. En effet, une machine de Turing étant [[Déterminisme|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''<ref>Cours de [[Jacques Arsac]], Paris VI</ref>. 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|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 ==
=== Notes et références ===
{{Références}}

=== Bibliographie ===
* {{On Computable Numbers}} {{Commentaire biblio| L'article fondateur où Turing définit les [[machine de Turing|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]]).}}
* {{Calculateurs, calculs, calculabilité (Ridoux, Lesventes)|numéro chapitre=3|titre chapitre=Le problème de l'arrêt}}
{{Palette|Informatique théorique}}{{Portail|informatique théorique}}

[[Catégorie:Calculabilité]]
[[Catégorie:Alan Turing]]