Probleme – Le problème de l'arrêt : ce qu'il interdit vraiment

1. L'équivalence de deux programmes. On réduit arrêt-vide — indécidable, d'après l'exercice — au problème de l'équivalence.

Soit $q$ un programme. On fabrique deux programmes :

(* r1 : lance q sur l'entree vide, puis rend 0 quoi qu'il arrive. *)
let r1 _ = executer q ""; 0

(* r2 : rend 0 immediatement, sans rien faire. *)
let r2 _ = 0

Fabriquer ces deux textes est calculable. Et

$$r_1\text{ et }{r}_2\text{ calculent la meˆme fonction}⟺q\text{ s’arreˆte sur l’entreˊe vide}.$$

En effet, si $q$ s'arrête, $r_1$ rend $0$ sur toute entrée, comme $r_2$. Si $q$ ne s'arrête pas, $r_1$ ne rend jamais rien : sa fonction n'est définie nulle part, alors que celle de $r_2$ est définie partout.

Donc un décideur de l'équivalence donnerait un décideur de arrêt-vide. Il n'en existe pas.

Ce que ce résultat interdit concrètement : il n'existera jamais d'outil qui, recevant deux versions d'une fonction, réponde à coup sûr « elles font la même chose ». Aucun test de non-régression n'est complet, et ce n'est pas un défaut d'outillage.

2. La semi-décidabilité. La procédure « simuler $p$ sur $x$ et répondre oui dès que la simulation se termine » répond correctement sur toutes les instances positives. arrêt est donc semi-décidable.

Son complémentaire ne l'est pas. Supposons-le : il existerait une procédure $S_{-}$ qui répond oui exactement quand $p$ ne s'arrête pas sur $x$. Alors on décide arrêt en entrelaçant les deux procédures : on exécute une étape de la simulation, puis une étape de $S_{-}$, puis une autre étape de chaque, et ainsi de suite. Comme l'une des deux répond forcément, l'entrelacement s'arrête toujours, et arrêt serait décidable. Contradiction.

L'entrelacement mérite d'être retenu : il permet de simuler deux calculs sans en privilégier aucun, et sans jamais rester bloqué sur celui qui ne finit pas. C'est le seul procédé de la théorie qui ressemble à de la programmation concurrente, au sens du chapitre chap:concurrence.

3. Pour un compilateur. Trois conséquences, toutes visibles dans les outils réels.

• Aucun avertissement n'est à la fois complet et exact. Un analyseur qui signale toutes les boucles infinies en signalera aussi de fausses ; un analyseur qui n'en signale aucune à tort en manquera. Les compilateurs choisissent la seconde attitude : ils préfèrent se taire que crier à tort, car un avertissement souvent injustifié cesse très vite d'être lu.
• Les optimisations sont conservatrices. Le compilateur ne supprime un calcul que s'il prouve qu'il est inutile. Ne pas savoir le prouver n'est pas une preuve du contraire, et le calcul reste.
• La troisième réponse est la clef. Un outil qui répond « termine », « ne termine pas », ou « je ne sais pas » peut toujours s'arrêter, et il est utile dès que la troisième réponse est rare. C'est ce que font les analyseurs statiques et les vérificateurs de types.

Une mesure pour finir. La suite de Syracuse, mesurée plus haut, demande $524$ étapes pour $n=837799$ et $685$ pour $n=8400511$. Personne ne sait si elle termine pour tout $n$ ; en particulier, aucun outil ne peut répondre pour ce programme-là. L'indécidabilité n'est pas un obstacle lointain : elle commence à une boucle de trois lignes.