🔢 mathematics

Bidirectional Interpolation for the Lambda-Calculus -- Revisiting and Formalising Craig-Čubrić Interpolation

Cet article présente une nouvelle preuve du théorème d'interpolation pertinent pour les preuves de Čubrić dans le lambda-calcul simplement typé, fondée sur les principes de typage bidirectionnel et formalisée dans le système Rocq.

Auteurs originaux : Meven Lennon Bertrand, Alexis Saurin

Publié 2026-03-04

📖 5 min de lecture🧠 Analyse approfondie

CC BY 4.0

Auteurs originaux : Meven Lennon Bertrand, Alexis Saurin

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 Titre : "L'Interpolation Bidirectionnelle pour le Lambda-Calcul"

(Ou, en français courant : "Comment trouver le pont parfait entre deux idées, même dans un monde de logique complexe")

Imaginez que vous avez deux personnes qui parlent des sujets très différents.

Personne A parle de la cuisine (ingrédients, recettes).
Personne B parle de la construction de maisons (briques, ciment).

Si vous voulez que A explique quelque chose à B, ou vice-versa, il faut un pont. Ce pont ne doit utiliser que des mots que les deux comprennent (par exemple, "la structure" ou "l'organisation"). En logique, ce pont s'appelle un interpolant.

Ce papier de recherche s'intéresse à la façon de construire ce pont non seulement pour les idées (les phrases), mais aussi pour les preuves (la façon dont on arrive à la conclusion). C'est ce qu'on appelle l'interpolation "proof-relevant" (pertinente pour la preuve).

🧩 Le Problème : Un vieux plan de construction un peu moche

Il y a déjà des années, un chercheur nommé Čubrić a trouvé une façon de construire ce pont pour un langage de programmation très simple (appelé STLC+). C'était une découverte géniale, mais son "plan de construction" (sa preuve mathématique) était... disons, très compliqué et un peu laid.

L'analogie : Imaginez qu'il a construit un pont en escaladant chaque brique une par une, en remplaçant des morceaux par d'autres, et en disant "c'est comme le cas précédent" alors que ce n'était pas du tout pareil. C'était laborieux, difficile à vérifier et risqué de faire des erreurs.

Les auteurs de ce papier (Meven Lennon-Bertrand et Alexis Saurin) se sont dit : "On peut faire mieux. On peut rendre ce pont plus élégant, plus solide et plus facile à comprendre."

🛠️ La Solution : Le système "Bidirectionnel" (Aller-Retour)

Pour simplifier la tâche, les auteurs ont utilisé une méthode appelée typage bidirectionnel.

L'analogie du jeu de rôle :
Imaginez que vous essayez de deviner le type d'un objet dans un jeu vidéo.

Mode Inférence (Déduction) : Vous regardez l'objet et vous demandez : "Qu'est-ce que c'est ?" (La réponse sort de l'objet).
Mode Vérification (Contrôle) : Vous avez une étiquette dans la main (ex: "C'est une épée") et vous demandez à l'objet : "Est-ce que tu es bien une épée ?" (L'objet doit correspondre à l'étiquette).

Dans les systèmes logiques classiques, on essaie souvent de tout deviner d'un coup, ce qui crée des confusions. Ici, les auteurs disent : "Non, on va alterner intelligemment. Parfois on devine, parfois on vérifie."

Pourquoi c'est génial ?
Cette méthode correspond parfaitement à une règle fondamentale de la logique appelée la propriété des sous-formules.

La règle : Pour prouver quelque chose, on ne doit jamais "inventer" de nouveaux concepts magiques. On ne doit utiliser que des briques qui sont déjà présentes dans la question ou la réponse.
L'analogie : C'est comme faire un gâteau. Si vous voulez prouver que vous avez fait un gâteau au chocolat, vous ne pouvez pas soudainement utiliser du saumon. Vous devez utiliser des ingrédients (briques) qui sont soit dans la recette de départ, soit dans le gâteau final.

En utilisant le typage bidirectionnel, les auteurs ont montré que les "formes normales" (les versions simplifiées et propres des programmes) suivent naturellement cette règle. C'est comme si le système de typage était un filtre de sécurité qui empêche d'inventer des concepts illégitimes.

🏗️ Le Résultat : Un pont plus solide et vérifié par ordinateur

Grâce à cette nouvelle méthode, les auteurs ont pu :

Réécrire la preuve de Čubrić de manière beaucoup plus simple et directe. Plus besoin de sauter d'une brique à l'autre de façon confuse ; on suit un chemin logique clair.
Tout vérifier par ordinateur. Ils ont utilisé un assistant de preuve appelé Rocq (un robot mathématicien très pointu) pour vérifier chaque étape de leur nouveau pont.
- Analogie : Au lieu de dire "je crois que ce pont tient", ils ont demandé à un robot de marcher sur chaque planche, de la première à la dernière, pour s'assurer qu'aucune ne bouge.

Ils ont même prouvé que tout programme dans ce langage peut être "nettoyé" (normalisé) pour devenir cette forme simple et propre, ce qui est une étape cruciale pour que l'interpolation fonctionne.

💡 Pourquoi est-ce important pour tout le monde ?

Même si cela semble très technique, cela a des implications concrètes :

Pour les informaticiens : Cela aide à créer des outils de vérification de logiciels plus fiables. Si on peut prouver qu'un logiciel respecte certaines règles sans utiliser de concepts cachés, on a plus confiance en lui.
Pour les mathématiciens : Cela montre que des concepts anciens (comme l'interpolation de Craig) peuvent être rafraîchis et rendus plus élégants grâce aux techniques modernes.
Pour l'avenir : Les auteurs espèrent que cette méthode pourra un jour s'appliquer à des systèmes de logique encore plus complexes (comme ceux utilisés dans l'intelligence artificielle ou les contrats intelligents), pour s'assurer qu'ils ne "trichent" pas en inventant des concepts hors contexte.

En résumé

Ce papier, c'est l'histoire de deux chercheurs qui ont pris un vieux plan de construction de pont (la preuve de Čubrić), qui était bancal et difficile à lire, et qui l'ont remplacé par un pont moderne, élégant et vérifié par un robot, en utilisant une astuce intelligente (le typage bidirectionnel) qui garantit qu'on n'utilise que les bons matériaux pour le construire.

C'est une victoire de la clarté et de la rigueur sur la complexité inutile.

1. Problématique et Contexte

L'article s'intéresse au théorème d'interpolation de Craig, un résultat fondamental en logique mathématique et en informatique théorique. Ce théorème stipule que si une formule $A$ implique une formule $B$ , il existe une formule intermédiaire $I$ (l'interpolant) qui ne contient que les symboles communs à $A$ et $B$ , telle que $A \vdash I$ et $I \vdash B$ .

L'objectif principal des auteurs est de revisiter et de formaliser une version proof-relevant (dépendante de la preuve) de ce théorème, initialement établie par Čubrić pour le $\lambda$ -calcul simplement typé avec sommes et types vides (STLC+).

Le défi : La preuve originale de Čubrić, bien que correcte, est complexe, repose sur une induction sur la taille des termes (remplacement progressif de sous-termes par des variables) et contient des cas subtils mal gérés. De plus, elle n'a jamais été formalisée de manière complète.
La limitation des formes normales : Dans le STLC+ (qui correspond aux catégories bi-cartésiennes fermées), les formes $\beta$ -normales usuelles ne possèdent pas toujours la propriété de sous-formule nécessaire à l'interpolation, en raison des conversions de commutation (commuting conversions) liées aux types positifs (sommes et type vide).

2. Méthodologie

Les auteurs proposent une nouvelle approche fondée sur deux piliers principaux :

A. Caractérisation Bidirectionnelle des Formes Normales

Au lieu d'une induction sur la taille des termes, les auteurs utilisent une induction mutuelle basée sur une caractérisation inductive des formes normales et des termes neutres, exprimée via un système de typage bidirectionnel.

Typage bidirectionnel : Ils distinguent les jugements d'inférence ( $\Gamma \vdash t \triangleright A$ ) et de vérification ( $\Gamma \vdash t \triangleleft A$ ). Cette distinction reflète le flux d'information et correspond naturellement à la propriété de sous-formule : l'information de type ne doit jamais être "inventée".
Gestion des conversions de commutation : Pour obtenir une classe de formes normales possédant une bonne propriété de sous-formule dans le STLC+, les auteurs intègrent les conversions de commutation (qui déplacent les éliminateurs à travers d'autres éliminateurs de types positifs). Ils définissent des formes normales inductives qui incluent les éliminateurs bloqués (neutrals) et les cas de sommes/vides, évitant ainsi les redexes.

B. Preuve de Normalisation par Relations Logiques

Pour garantir que tout terme bien typé peut être réduit à une forme normale (nécessaire pour appliquer le théorème d'interpolation), les auteurs développent une preuve de normalisation par relations logiques (inspirée d'Abel et Sattler).

Ils introduisent une notion de couverture (covering) pour gérer les éliminateurs de types positifs (sommes et $\bot$ ), qui ne sont pas neutres.
Ils définissent des valeurs (values) et des termes réductibles (reducible) pour prouver que tout terme bien typé se réduit vers une forme normale.

3. Contributions Clés

Nouvelle Preuve d'Interpolation Proof-Relevant :
- Les auteurs établissent un nouveau théorème d'interpolation pour le STLC+. Pour tout terme normal $t$ tel que $x:A \vdash t : B$ , il existe un type $C$ (construit à partir des atomes communs à $A$ et $B$ ) et des termes $u : A \to C$ et $v : C \to B$ tels que la composition $(\lambda y. v) u$ se réduit à $t$ .
- Contrairement à la preuve de Čubrić, cette approche est plus directe, plus structurée et évite les cas pathologiques grâce à l'induction mutuelle sur les formes normales bidirectionnelles.
- L'interpolant construit est légèrement différent de celui de Čubrić (utilisant des produits pour regrouper les arguments plutôt que des types fonctionnels itérés), ce qui simplifie la structure.
Formalisation dans Rocq (Coq) :
- C'est la première formalisation complète de la preuve d'interpolation de Čubrić.
- L'article inclut la formalisation de la métathéorie du STLC+, y compris la preuve de normalisation avec conversions de commutation, ce qui est une première pour un calcul avec ces conversions spécifiques.
- Le code fait environ 4000 lignes (LCoC), ce qui est très compact comparé à d'autres formalisations d'interpolation.
Lien entre Typage Bidirectionnel et Propriété de Sous-Formule :
- L'article clarifie et met en lumière le lien entre le typage bidirectionnel et la propriété de sous-formule. Les auteurs montrent que le typage bidirectionnel capture naturellement les formes normales ayant cette propriété, même en présence de sommes (contrairement à une croyance répandue selon laquelle cela échouerait).

4. Résultats Techniques

Théorème d'Interpolation (Constant-free) : Pour un terme normal $t$ dans un contexte partitionné $\Gamma = \Gamma_s \cup \Gamma_t$ , il existe un type interpolant $M$ et des termes $l$ et $r$ tels que $t \equiv r[l..]$ . Le type $M$ n'utilise que le vocabulaire commun aux contextes source et cible.
Gestion des Constantes et Équations : Le théorème est généralisé pour inclure des constantes et des équations arbitraires, en étendant la partition du vocabulaire aux constantes.
Normalisation : Preuve formelle que tout terme bien typé dans STLC+ (avec conversions de commutation) se réduit à une forme normale unique (au sens de la réduction, pas nécessairement de l'équivalence $\eta$ -longue complète).

5. Signification et Impact

Simplification Théorique : La nouvelle preuve remplace une induction complexe sur la taille des termes par une induction structurelle plus naturelle sur les formes normales, rendant le résultat plus robuste et plus facile à comprendre.
Avancée en Formalisation : La réussite de la formalisation dans Rocq démontre la faisabilité de prouver des théorèmes d'interpolation proof-relevant complexes avec des assistants de preuve modernes, en surmontant les difficultés liées aux substitutions et aux conversions de commutation.
Ouverture vers le Futur :
- Interpolation Uniforme : Les auteurs proposent d'étendre ce résultat à une interpolation uniforme (un seul interpolant pour une classe de formules).
- Types Dépendants : Ils identifient les défis pour étendre ce théorème aux types dépendants, notamment la difficulté des conversions de commutation dans ce contexte (ex: le "convoy pattern").
- Termes Non-Normaux : Une piste de recherche consiste à adapter le système de typage bidirectionnel pour interpoler des termes contenant des redexes, en utilisant des annotations explicites pour gérer les coupures.

En résumé, cet article offre une refonte élégante et formalisée d'un résultat classique de la théorie des preuves, en exploitant les propriétés structurelles du typage bidirectionnel pour simplifier la preuve et en fournissant une base solide pour des recherches futures sur l'interpolation proof-relevant dans des systèmes de types plus riches.