Quand on ne sait pas construire l'ordre

(* Precondition : n >= 1. *)
let rec vol n =
  if n = 1 then 0
  else if n mod 2 = 0 then 1 + vol (n / 2)
  else 1 + vol (3 * n + 1)

Personne ne le sait. C'est la conjecture de Syracuse, formulée en 1937 et toujours ouverte : on ignore si cette fonction termine pour tout $n\ge 1$.

Pourquoi les outils du chapitre échouent. Sur la branche paire, $n/2<n$ : tout va bien. Sur la branche impaire, $3n+1>n$ : l'argument triple. Il faudrait donc un ordre bien fondé pour lequel $3n+1\prec n$ quand $n$ est impair, et $n/2\prec n$ quand il est pair — et l'on ne sait pas en construire, ni prouver qu'il n'en existe pas.

Les mesures montrent pourquoi c'est difficile.

Partant de $27$, la suite monte jusqu'à $9232$ — $342$ fois sa valeur de départ — avant de retomber sur $1$ en $111$ étapes. Le record de longueur pour $n\le 1000$ est $n=871$, avec $178$ étapes. Aucune régularité n'apparaît : $7$ demande $16$ étapes et $8$ en demande $3$.

Ce que l'exercice enseigne, et c'est le contraire de ce qu'on attend d'un exercice. La méthode du chapitre — exhiber un ordre bien fondé pour lequel les appels décroissent — est une méthode suffisante pour prouver la terminaison. Elle n'est pas un algorithme : il n'existe aucune procédure générale décidant si un programme termine, et le chapitre chap:decidabilite le démontrera. Syracuse en est un témoin de deux lignes.

Ce qu'un programmeur en retire, concrètement. Une fonction dont on ne sait pas prouver la terminaison n'est pas une fonction dont on a prouvé qu'elle boucle : c'est une fonction sans garantie. En production, on lui adjoint un compteur d'étapes maximal — ce qui rend la terminaison triviale et déplace la question sur la correction du résultat. La conjecture, elle, a été vérifiée par ordinateur jusqu'à des valeurs de $n$ dépassant $2^{68}$, ce qui ne constitue pas une preuve et n'en constituera jamais une.