The Global Orientation Barrier in Step-Duplicating Recursors: Impossibility, Modular Escape, and a Certified Witness

Cet article établit, grâce à une vérification formelle dans Lean 4 et à des preuves externes, l'impossibilité de prouver la terminaison de recursors dupliquant les étapes par des mesures compositionnelles globales, tout en démontrant que les méthodes basées sur la projection échappent à cette barrière et en délivrant une chaîne de certification complète pour un fragment sécurisé.

L'essentiel

🏗️ Le Mur Invisible : Quand la duplication bloque les mathématiques

Imaginez que vous êtes un architecte chargé de prouver qu'une machine complexe (un système informatique) s'arrêtera toujours un jour et ne tournera pas éternellement. C'est ce qu'on appelle prouver la terminaison.

Dans ce papier, l'auteur, Moses Rahnama, a découvert un "mur" très spécifique. Ce mur empêche certaines méthodes mathématiques classiques de prouver que la machine s'arrête, même si elle s'arrête vraiment !

Voici comment cela fonctionne, étape par étape.

1. La Machine et le Problème de la "Duplication"

Imaginez une machine qui a une règle bizarre :

"Pour faire le prochain pas, prends ton outil actuel, copie-le deux fois, et utilise-le pour avancer."

En termes techniques, c'est une récursion qui duplique.

• Le piège : Si vous essayez de compter la "taille" ou le "poids" de la machine pour voir si elle diminue à chaque étape, vous êtes coincé.
• L'analogie : Imaginez que vous avez un gâteau. La règle dit : "Mange une part, mais avant de manger, duplique le reste du gâteau".
  • Si vous comptez simplement la quantité de gâteau, elle augmente ! (1 gâteau devient 2 gâteaux).
  • Les méthodes mathématiques classiques (appelées "mesures compositionnelles") disent : "Si le gâteau grossit, la machine ne s'arrêtera jamais".
  • Le problème : Ces méthodes sont trop bêtes. Elles voient le gâteau grossir et pensent que c'est une boucle infinie, alors que la machine s'arrête en réalité.

2. Le Mur de l'Impossibilité (Ce que le papier prouve)

L'auteur a construit une petite machine minimale (appelée KO7) avec seulement 7 pièces et 8 règles. Il a utilisé un assistant de preuve informatique (Lean 4) pour prouver une chose incroyable :

Aucune méthode de comptage simple ne peut prouver que cette machine s'arrête.

C'est comme si vous essayiez de prouver qu'une voiture s'arrête en pesant ses pneus. Peu importe comment vous pesez, le fait que la voiture duplique ses pneus à chaque tour de roue fausse votre balance. C'est le "Mur de l'Orientation Globale".

• Pourquoi ? Parce que la duplication crée une "masse" inutile qui grossit artificiellement le poids total, trompant les mathématiciens qui regardent l'ensemble du système d'un seul coup d'œil.

3. L'Échappatoire Magique : Le Détective Modulaire

Alors, comment prouver que la machine s'arrête si les méthodes classiques échouent ?

L'auteur montre qu'il existe une méthode différente, appelée Dépendance Modulaire (ou "Dependency Pairs").

• L'analogie du détective : Au lieu de peser tout le gâteau d'un coup, le détective regarde uniquement la partie qui compte vraiment : le compteur de tours.
• Il ignore le gâteau dupliqué (l'outil inutile). Il dit : "Peu importe combien de copies de l'outil on fait, le compteur (le nombre de tours restants) diminue toujours de 1."
• Le résultat : Le détective voit que le compteur descend vers zéro. Donc, la machine s'arrête.
• La leçon : Pour échapper au mur, il faut arrêter de regarder l'ensemble (global) et se concentrer sur la pièce maîtresse (modulaire), en ignorant le bruit de la duplication.

4. La Preuve par l'Ordinateur

L'auteur n'a pas seulement théorisé cela. Il a fait deux choses concrètes :

1. Certification par code : Il a écrit 7 000 lignes de code dans un langage mathématique rigoureux (Lean 4) pour prouver que les méthodes simples échouent vraiment et que la méthode modulaire fonctionne. C'est comme un contrat juridique infalsifiable.
2. Test réel : Il a donné la machine à un logiciel de test célèbre (TTT2).
   • Les méthodes "globales" (qui regardent tout) ont dit : "Je ne sais pas, peut-être que ça tourne à l'infini" (Résultat : MAYBE).
   • Les méthodes "modulaires" (qui ignorent la duplication) ont dit : "C'est fini !" (Résultat : YES).

5. La Partie "Sûre" et le Normalisateur

Le papier va plus loin. Il crée une version "sécurisée" de la machine (appelée SafeStep) où l'on ajoute des garde-fous pour éviter les conflits.

• Pour cette version sûre, l'auteur a construit un normalisateur certifié.
• Analogie : C'est comme un robot de cuisine qui prend n'importe quel gâteau complexe, le coupe, le mange, et vous rend un petit morceau final parfait. Le papier prouve mathématiquement que ce robot ne se bloquera jamais et donnera toujours le même résultat, peu importe le gâteau de départ.

🎯 En Résumé

Ce papier est une histoire de limites et de solutions :

1. Le Problème : Quand un système informatique copie ses propres données (duplication), les méthodes de calcul classiques qui regardent "l'ensemble" se trompent et pensent que le système tourne à l'infini.
2. La Preuve : L'auteur a prouvé mathématiquement (avec un ordinateur) que c'est impossible à résoudre avec ces méthodes classiques.
3. La Solution : Il faut changer de lunettes. Au lieu de regarder le poids total, il faut regarder uniquement la partie qui rétrécit (le compteur), en ignorant le reste. C'est ce que font les méthodes modulaires.

C'est une découverte importante car elle nous dit exactement où et pourquoi nos outils mathématiques habituels échouent, et comment les contourner intelligemment pour vérifier la sécurité des systèmes informatiques complexes.

Résumé technique

Voici un résumé technique détaillé du papier "The Global Orientation Barrier in Step-Duplicating Recursors: Impossibility, Modular Escape, and a Certified Witness" de Moses Rahnama (Mina Analytics, février 2026).

1. Problématique et Contexte

Le papier s'attaque à un problème fondamental dans la théorie de la réécriture de termes : la termination des systèmes de réécriture du premier ordre (TRS) contenant des récursifs à duplication d'étape (step-duplicating recursors).

• Le cœur du problème : Considérons une règle de récursion de la forme rec(b, s, σ(n)) → f(s, rec(b, s, n)). Ici, l'argument d'étape s apparaît une fois à gauche et deux fois à droite (dupliqué).
• La barrière : Les méthodes de preuve de termination "directes" ou "globales" (qui attribuent une mesure unique à tout le terme en agrégeant les sous-termes, comme les poids additifs ou les interprétations polynomiales) échouent systématiquement à prouver la termination pour de telles règles. La duplication de s fait augmenter la mesure globale, empêchant une décroissance stricte nécessaire à la preuve.
• L'hypothèse de travail : Le papier cherche à formaliser et prouver l'impossibilité de ces méthodes globales sur un système minimal, tout en montrant comment les méthodes modulaires (comme les paires de dépendance) contournent cette limite.

2. Méthodologie et Outils

L'approche est une combinaison rigoureuse de formalisation mécanique (Lean 4) et de validation expérimentale (TTT2/CeTA).

• Le Calcul KO7 (Témoin Minimal) :
  • Un système de réécriture minimal de premier ordre avec 7 constructeurs et 8 règles.
  • Il contient un récursif à duplication (rec∆) et des opérateurs pour la confluence (merge, eqW, integrate).
  • Conditions de conception : Pas de liaisons (binders), pas de mémoire externe (pas de partage de sous-termes, sémantique arborescente), et pas d'axiomes d'équation au niveau objet. Ces conditions isolent la duplication comme seule source de difficulté.
• Formalisation en Lean 4 :
  • Environ 7 000 lignes de code.
  • Preuve d'impossibilité pour deux classes de mesures composantes (additives et abstraites).
  • Preuve de terminaison forte (SN) et de confluence pour un fragment "sûr" (SafeStep) via une mesure lexicographique triple.
  • Certification d'un normaliseur total et correct.
• Validation Externe (TTT2) :
  • Utilisation de l'outil TTT2 pour prouver la termination du système complet (non restreint) via les paires de dépendance (DP) et le critère de sous-terme.
  • Comparaison des stratégies : les méthodes globales (Polynomial, KBO, Matrices) échouent (retour "MAYBE"), tandis que les méthodes modulaires (DP, LPO) réussissent.

3. Contributions Clés

A. Théorème d'Impossibilité (La Barrière Globale)

Le papier formalise et prouve deux théorèmes d'impossibilité (Théorème 9.1) pour le système KO7 :

1. Classe Additive (Tier 1) : Aucune mesure additive (où le poids d'un terme est la somme des poids des sous-termes + un poids pour le constructeur) ne peut orienter strictement la règle de duplication, à condition que le constructeur d'application (app) ait un poids positif.
2. Classe Abstraite (Tier 2) : Aucune mesure compositionnelle satisfaisant les axiomes de domination des sous-termes pour app (c'est-à-dire capp(x,y) > x et capp(x,y) > y) ne peut orienter la règle, même si le constructeur de successeur (delta) est transparent.

• Mécanisme de l'échec : La duplication de s dans app(s, rec(...)) force la mesure du côté droit à être supérieure ou égale à celle du côté gauche, brisant la décroissance stricte. C'est ce que l'auteur appelle le "App Trap" (Piège de l'application) : la duplication est syntaxiquement réelle mais sémantiquement inerte (car app n'a pas de règles de réduction), ce qui rend la duplication invisible pour les méthodes modulaires mais fatale pour les méthodes globales.

B. Évasion Modulaire (Paires de Dépendance)

Le papier démontre (Théorème 9.2) que la méthode des Paires de Dépendance (DP) avec le critère de sous-terme contourne cette barrière.

• En projetant sur le troisième argument du récursif (le compteur de récurrence n) et en ignorant l'argument dupliqué s (car il est enfermé sous un constructeur app qui est traité comme un constructeur par le cadre DP), la mesure décroît strictement.
• Cela prouve que la barrière n'est pas une limitation de la termination du système, mais une limitation des méthodes de preuve globales.

C. Certificat de Terminaison et Confluence pour le Fragment Sûr

Pour le fragment SafeStep (une sous-relation de KO7 avec des gardes pour assurer la confluence) :

• Terminaison Forte : Prouvée par une mesure lexicographique triple computable : (δ-flag, κM, τ).
  • δ-flag : Bit de phase qui décroît lors de la récursion.
  • κM : Ordre multienl (Dershowitz-Manna) gérant la duplication.
  • τ : Mesure de taille pour résoudre les égalités.
• Confluence : Prouvée via le Lemme de Newman (Terminaison + Confluence Locale ⇒ Confluence Globale). La confluence locale est vérifiée machine pour toutes les paires critiques.
• Normaliseur Certifié : Un algorithme de normalisation total et correct est extrait de la preuve, avec une borne supérieure de complexité ordinaire inférieure à $\varepsilon_0$ (et précisément calibrée autour de $\omega^\omega$).

4. Résultats Expérimentaux et Validation

• TTT2 : Sur le système KO7 complet (non gardé), TTT2 prouve la termination en < 1 seconde avec les stratégies DP et LPO.
• Échec des méthodes globales : Les stratégies basées sur les interprétations polynomiales, KBO et les interprétations matricielles retournent "MAYBE" (échec de recherche), confirmant empiriquement l'impossibilité théorique prouvée en Lean.
• Certification CeTA : Les preuves de termination générées par TTT2 sont indépendamment certifiées par CeTA (Isabelle/HOL).

5. Signification et Implications

1. Frontière Précise : Le papier établit une frontière mathématiquement prouvée entre les méthodes de preuve globales et modulaires pour les systèmes avec duplication. Il montre que la duplication d'arguments non contrôlée rend les mesures globales inadéquates, même si le système est terminant.
2. Rôle de la Duplication : Une ablation mécanique (§9.6) montre que si l'on retire la duplication (récursif linéaire), les mesures globales simples (comme la taille) fonctionnent immédiatement. Cela confirme que la duplication est la cause unique de la barrière.
3. Validité des Méthodes Modulaires : Cela renforce la nécessité des cadres modulaires (comme DP) pour les systèmes complexes, car ils peuvent "projeter" hors des parties du terme qui causent des problèmes de mesure (comme la masse dupliquée inerte).
4. Preuve Formelle Complète : L'ensemble de la chaîne de preuve (impossibilité, termination, confluence, normalisation, calibration ordinaire) est mécanisée, offrant un exemple rare de système de réécriture où les limites théoriques et les preuves de termination sont toutes deux vérifiées formellement.

En résumé, ce papier démontre que pour les récursifs à duplication sans liaisons ni mémoire externe, la terminaison est prouvable par décomposition modulaire mais impossible par agrégation globale, et fournit une preuve formelle complète de cette dichotomie sur un système témoin minimal.