Parmi toutes les machines de Turing à 5 états qui finissent par s’arrêter, laquelle tourne le plus longtemps ? Ce problème du « castor affairé » (busy beaver) résistait depuis 1990. En 2024, une collaboration en ligne d’amateurs et de chercheurs, bbchallenge, l’a résolu.
Le record est tenu par une machine trouvée dès 1989 : il fallait prouver qu’aucune des autres machines à 5 états ne fait mieux sans tourner indéfiniment. La preuve, qui passe en revue des millions de machines, a été entièrement vérifiée par un assistant de preuve (Coq).
Qu’est-ce qu’une machine de Turing ?
Imaginée par Alan Turing en 1936, c’est l’ordinateur le plus simple qu’on puisse concevoir. Un ruban infini est découpé en cases qui contiennent 0 ou 1. Une tête de lecture, qui se trouve dans un certain état (A, B, C…), lit la case devant elle. Selon ce qu’elle lit et son état, elle écrit un symbole, se déplace d’une case vers la gauche ou la droite, et change d’état. Un état spécial, H, arrête la machine.
Voici le champion à 2 états, qui s’arrête après 6 étapes en laissant quatre 1 sur le ruban. « 1DB » se lit : écrire 1, aller à droite, passer dans l’état B.
État | Lit 0 | Lit 1 |
|---|---|---|
A | 1DB | 1GB |
B | 1GA | 1DH |
Une fonction qui explose
BB(n) est le plus grand nombre d’étapes que puisse faire, avant de s’arrêter, une machine à n états partant d’un ruban vide. La fonction a été inventée par Tibor Radó en 1962. Les valeurs pour 3 et 4 états ont été établies en 1965 et en 1983 ; la suivante s’est fait attendre plus de quarante ans.
États | 1 | 2 | 3 | 4 | 5 |
|---|---|---|---|---|---|
BB(n) | 1 | 6 | 21 | 107 | 47 176 870 |
La fonction BB croît plus vite que toute fonction calculable : aucun programme ne peut la calculer pour tout . Pour , on sait déjà que la valeur dépasse tout ce qu’on peut écrire en notation décimale.
Pourquoi aucun programme ne peut calculer BB
Supposons qu’un programme calcule BB(n). On saurait alors si n’importe quelle machine à n états s’arrête : il suffirait de la faire tourner BB(n) étapes. Si elle ne s’est pas arrêtée, elle ne s’arrêtera jamais.
Or Turing a démontré en 1936 qu’aucun programme ne peut décider, pour toute machine, si elle finit par s’arrêter : c’est le célèbre problème de l’arrêt. Un tel programme ne peut donc pas exister.
Pourquoi a-t-il fallu si longtemps ?
Chacune des cases de la table offre 2 symboles à écrire, 2 directions et n + 1 états suivants (arrêt compris). Pour 5 états, cela fait :
Les symétries en éliminent beaucoup, et la plupart des autres s’arrêtent vite ou bouclent de façon évidente. Mais quelques machines au comportement très irrégulier, comme la redoutable « Skelet #17 », ont exigé chacune une preuve sur mesure.
Une preuve vérifiée par ordinateur
Lancé en 2022 par Tristan Stérin, le projet bbchallenge a réuni en ligne des contributeurs du monde entier, souvent amateurs. Tout est documenté sur bbchallenge.org.
Faire vérifier une preuve par un assistant comme Coq (aujourd’hui appelé Rocq), c’est avoir la garantie que chaque étape logique est correcte, sans relire à la main des milliers de cas.