💻 computer science

A Constructive Proof of Rice's Theorem and the Halting Problem via Hilbert's Tenth Problem

Cet article présente une preuve constructive de l'indécidabilité du théorème de Rice et du problème de l'arrêt, basée sur l'indécidabilité du dixième problème de Hilbert et formalisée dans l'assistant de preuve Rocq, évitant ainsi l'usage du tiers exclu et de la diagonalisation.

Auteurs originaux : Jonathan Brossard

Publié 2026-04-21

📖 5 min de lecture🧠 Analyse approfondie

CC BY 4.0

Auteurs originaux : Jonathan Brossard

Article original sous licence CC BY 4.0 (http://creativecommons.org/licenses/by/4.0/). ✨ Ceci est une explication générée par l'IA de l'article ci-dessous. Elle n'a pas été rédigée ni approuvée par les auteurs. Pour une précision technique, consultez l'article original. Lire la clause de non-responsabilité complète

🕵️‍♂️ Le Grand Détective et le Mystère des Programmes

Imaginez que vous êtes un détective privé. Votre travail consiste à examiner des programmes informatiques (des recettes de cuisine numériques) pour répondre à une question précise : "Ce programme va-t-il s'arrêter un jour, ou va-t-il tourner dans une boucle éternelle ?"

En informatique, il existe une règle célèbre appelée le Théorème de Rice. Elle dit quelque chose de très frustrant pour les détectives : "Il est impossible de créer un détective universel capable de répondre à n'importe quelle question sur le comportement des programmes, sauf si la question est triviale (comme 'est-ce que ce programme existe ?')."

Autrement dit, vous ne pouvez pas écrire un logiciel qui prédit le comportement futur de n'importe quel autre logiciel.

🚫 Le Problème des Anciens Détectifs (La Preuve Classique)

Pendant des décennies, les mathématiciens ont prouvé ce théorème en utilisant une méthode un peu "magique" et un peu effrayante :

Le Miroir Magique (Diagonalisation) : Ils inventaient un programme qui se regardait dans le miroir et disait : "Si tu dis que je m'arrête, je continue ! Si tu dis que je continue, je m'arrête !" Cela créait un paradoxe logique.
Le Pari (Loi du Tiers Exclu) : Ils forçaient le détective à faire un choix binaire : "Soit le programme s'arrête, soit il ne s'arrête pas." En logique classique, on accepte ce pari. Mais en logique "constructive" (celle qui veut construire des choses réelles), on ne peut pas faire ce pari sans preuve.

Ces anciennes preuves étaient comme des tours de magie : elles montraient que le détective ne pouvait pas exister, mais elles ne nous donnaient pas de nouvelles règles pour comprendre pourquoi c'est impossible sans utiliser de "magie" logique.

🌱 La Nouvelle Approche : Le Jardin des Équations (Ce Papier)

L'auteur de ce papier, Jonathan Brossard, propose une nouvelle façon de prouver l'impossibilité de ce détective. Il ne veut pas utiliser de magie ni de miroirs. Il veut utiliser des pieds de biche et des équations.

Voici son idée, expliquée avec une métaphore :

1. Le Problème de l'Équation Impossible (Hilbert)

Imaginez un jeu de puzzle mathématique très difficile. On vous donne une équation avec des nombres entiers (comme $x^2 + y^2 = z^2$ ).

Parfois, il existe une solution (des nombres qui rendent l'équation vraie).
Parfois, il n'y a aucune solution possible, peu importe combien de temps vous cherchez.

Un grand théorème (le théorème MRDP) nous dit qu'il est impossible de créer un algorithme qui peut dire, pour n'importe quelle équation, si une solution existe ou non. C'est le "mur" de l'informatique.

2. La Construction à Deux Témoins (Le Secret du Papier)

L'auteur dit : "Et si nous utilisions ce mur (l'impossibilité de résoudre les équations) pour prouver l'impossibilité de prédire les programmes ?"

Il imagine deux programmes jumeaux, appelons-les S0 et S1.

Le Scénario A (L'équation a une solution) :
- Le programme S1 se comporte comme un programme qui s'arrête (il réussit sa tâche).
- Le programme S0 se comporte comme un programme qui tourne en boucle (il échoue).
- Résultat : Un détective qui fonctionne bien devrait dire "S1 = OUI" et "S0 = NON". Il y a une différence claire.
Le Scénario B (L'équation n'a PAS de solution) :
- Ici, c'est la partie géniale. Puisqu'il n'y a pas de solution, les programmes S0 et S1 ne trouvent jamais leur "issue". Ils sont forcés de continuer à chercher indéfiniment.
- Résultat : S0 et S1 deviennent identiques. Ils tournent tous les deux en boucle éternelle.
- Le Détective : Même s'il ne sait pas si "la boucle éternelle" est une propriété vraie ou fausse, il doit donner la même réponse pour S0 et S1, car ils se comportent exactement pareil.

3. Le Piège

Si un détective (un programme qui décide) existait vraiment, il pourrait regarder la différence entre sa réponse pour S1 et sa réponse pour S0.

Si la différence est grande, l'équation a une solution.
Si la différence est nulle, l'équation n'a pas de solution.

Boum ! Ce détective aurait résolu le problème des équations impossibles. Or, on sait déjà que c'est impossible. Donc, le détective de départ n'a jamais pu exister.

✨ Pourquoi est-ce important ? (La Magie Constructive)

La différence majeure avec les anciennes preuves, c'est que cette nouvelle preuve est constructive.

L'ancienne preuve disait : "Si un détective existait, on pourrait créer un monstre paradoxal. Donc, il n'existe pas." (C'est comme dire : "Si tu existes, tu vas exploser, donc tu n'existes pas").
La nouvelle preuve dit : "Si un détective existait, on pourrait l'utiliser pour résoudre des énigmes mathématiques que nous savons être insolubles. Donc, il n'existe pas."

C'est une preuve plus "propre" et plus utile. Elle ne repose pas sur des suppositions magiques ("Soit A, soit non-A"). Elle montre comment l'impossibilité d'un domaine (les équations) se propage directement à un autre (les programmes).

🏁 Conclusion Simple

Ce papier nous dit :

"Vous ne pouvez pas prédire le comportement futur d'un programme, non pas parce que l'univers est magique, mais parce que si vous le pouviez, vous pourriez résoudre des énigmes mathématiques qui sont, par nature, insolubles. C'est comme essayer de construire une machine à voyager dans le temps : si vous y arriviez, vous pourriez résoudre le paradoxe du grand-père, ce qui prouve que votre machine ne peut pas exister."

L'auteur a même écrit tout cela dans un langage que les ordinateurs peuvent vérifier (Rocq/Coq), prouvant que son raisonnement est solide, sans aucun raccourci logique interdit. C'est une victoire de la logique pure sur la magie.

1. Le Problème

L'article s'attaque à la démonstration constructive de deux piliers de la théorie de la calculabilité :

Le Théorème de Rice : Aucune propriété sémantique non triviale d'un programme n'est décidable.
Le Problème de l'Arrêt : Il n'existe pas d'algorithme capable de déterminer si un programme arbitraire s'arrête.

Les preuves classiques de ces résultats reposent sur des arguments de diagonalisation (auto-référence) et invoquent systématiquement la Loi du Tiers Exclu (LTE) (ou Law of Excluded Middle - LEM). Plus précisément, les preuves classiques nécessitent :

De supposer qu'un programme hypothétique construit soit s'arrête, soit diverge (LTE sur la convergence).
De faire une analyse de cas sur la valeur de vérité d'une propriété $P$ appliquée au programme qui diverge toujours ( $\bot$ ), c'est-à-dire $P(\bot) \lor \neg P(\bot)$ .

Ces dépendances rendent les preuves non valides en logique intuitionniste et empêchent leur extraction directe en programmes vérifiés dans des assistants de preuve comme Coq ou Rocq, car elles ne fournissent pas de contenu computationnel constructif.

2. Méthodologie

L'auteur propose une preuve entièrement constructive (valide en logique intuitionniste) qui élimine la diagonalisation et l'auto-référence. La stratégie repose sur une réduction directe au 10ème Problème de Hilbert (MRDP) plutôt qu'au problème de l'arrêt.

Les éléments clés de la méthodologie sont :

Réduction au MRDP : Au lieu de réduire le théorème de Rice au problème de l'arrêt, l'article réduit directement la décidabilité d'une propriété sémantique à la décidabilité de la solvabilité d'équations diophantiennes (polynômes à coefficients entiers). Le théorème MRDP (Davis-Putnam-Robinson-Matiyasevich) établit que tout ensemble récursivement énumérable est diophantien. L'indécidabilité de la solvabilité diophantienne est utilisée comme axiome de départ (prouvé constructivement dans la bibliothèque coq-library-undecidability).
Construction à deux témoins (Two-Witness Construction) :
- Soit $P$ une propriété sémantique non triviale, avec deux programmes témoins explicites : $e_0$ (tel que $\neg P(e_0)$ ) et $e_1$ (tel que $P(e_1)$ ).
- Pour tout polynôme diophantien $D$ , l'auteur construit deux programmes $S^0_D$ et $S^1_D$ .
- Comportement :
  - Si $D$ a une solution, $S^0_D$ se comporte comme $e_0$ et $S^1_D$ se comporte comme $e_1$ .
  - Si $D$ n'a pas de solution, les deux programmes $S^0_D$ et $S^1_D$ divergent de manière identique (ils sont observationnellement équivalents à $\bot$ ).
Absence de cas sur $P(\bot)$ : La force de cette construction réside dans le fait que lorsque $D$ est insoluble, $S^0_D$ et $S^1_D$ sont indistinguables. Par extensionnalité, $P(S^0_D) \iff P(S^1_D)$ . Le décideur hypothétique pour $P$ doit donc retourner la même valeur pour les deux, rendant la connaissance de la valeur de $P(\bot)$ totalement inutile.
Séparation par différence ( $\delta_D$ ) : Si un décideur $Decide_P$ $D ec i d e_{P}$ existait, on pourrait définir une fonction $F(D) = Decide_P(S^1_D) - Decide_P(S^0_D)$ $F (D) = D ec i d e_{P} (S_{D}^{1}) - D ec i d e_{P} (S_{D}^{0})$ .
- Si $D$ est soluble : $F(D) = 1 - 0 = 1$ .
- Si $D$ est insoluble : $F(D) = 0 - 0 = 0$ (car les programmes sont équivalents).
- Cela créerait un séparateur calculable pour la solvabilité diophantienne, contredisant le théorème MRDP.

3. Contributions Clés

Preuve Constructive du Théorème de Rice : C'est la première preuve qui évite à la fois la diagonalisation et l'analyse de cas sur $P(\bot)$ , rendant le théorème valide en logique intuitionniste pure.
Élimination de la Diagonalisation : La preuve ne repose pas sur le théorème de récursion ou sur l'auto-référence. Les programmes témoins sont construits explicitement à partir d'un polynôme et d'un bit, sans point fixe.
Modélisation par Indexation (Step-Indexed) : L'article utilise un modèle de calcul basé sur l'indexation par étapes (fuel) pour définir l'équivalence observationnelle. Cela permet de gérer la convergence et la divergence de manière constructive sans avoir besoin de conditions de totalité sur les programmes témoins.
Formalisation Complète en Rocq (Coq) : L'article est accompagné d'une formalisation complète (1919 lignes) dans l'assistant de preuve Rocq.
- Axiomes : La preuve ne dépend d'aucun axiome classique. Le seul axiome externe est l'indécidabilité du 10ème problème de Hilbert (prouvée constructivement par Larchey-Wendling et Forster).
- Vérification : L'outil Print Assumptions confirme que les théorèmes de Rice et de l'arrêt sont « fermés sous le contexte global » (closed under the global context), signifiant qu'ils ne reposent sur aucune hypothèse classique implicite.

4. Résultats

Théorème de Rice Constructif : Il est démontré que pour toute propriété sémantique non triviale $P$ , il n'existe pas de programme décidant $P$ . La preuve est structurée comme deux implications distinctes (Solvable $\implies \delta_D=1$ et Insolvable $\implies \delta_D=0$ ) sans jamais affirmer la disjunction « Solvable ou Insoluble ».
Indécidabilité du Problème de l'Arrêt : En tant que corollaire immédiat (une seule ligne de code Rocq), l'indécidabilité du problème de l'arrêt est déduite en appliquant le théorème de Rice à la propriété « Terminates » (s'arrête). Cela inverse la direction habituelle des preuves (où le théorème de Rice est souvent déduit du problème de l'arrêt).
Hiérarchie de Degré : L'article introduit une notion de « degré de Rice » basée sur le degré du polynôme diophantien utilisé pour la réduction. Il est démontré que le degré 4 suffit pour capturer toute l'indécidabilité (saturé par le théorème MRDP), tandis que les degrés 2 et 3 restent des questions ouvertes.

5. Signification

Pour la Logique Constructive et la Vérification Formelle : Cette preuve permet d'intégrer l'indécidabilité de Rice et de l'arrêt dans des systèmes de types dépendants (comme Coq/Rocq) sans recourir à des axiomes classiques (comme la LTE). Cela ouvre la voie à l'extraction de programmes vérifiés et à l'internalisation de ces arguments dans des environnements de preuve purement constructifs.
Changement de Paradigme : En remplaçant la diagonalisation (auto-référence) par une réduction arithmétique (MRDP), l'article offre une perspective structurelle différente sur l'indécidabilité. Il montre que l'indécidabilité provient fondamentalement de la complexité de l'arithmétique diophantienne plutôt que de l'auto-référence.
Audit des Axiomes : L'article fournit un audit rigoureux de la dépendance aux axiomes, démontrant que l'indécidabilité peut être établie avec un minimum de principes non constructifs (seulement l'indécidabilité du MRDP, elle-même prouvée constructivement).
Impact Pratique : La construction des programmes témoins est explicite et algorithmique. L'auteur fournit même un exemple en C (undecidable.c) illustrant comment ces constructions pourraient se manifester dans un code réel, reliant la théorie abstraite à des conjectures de théorie des nombres (sommes de cubes).

En résumé, cet article réussit à « purifier » les preuves classiques de Rice et de l'arrêt, les rendant compatibles avec la logique intuitionniste et les systèmes de preuve formels modernes, tout en offrant une compréhension plus profonde de la source de l'indécidabilité via l'arithmétique diophantienne.