🔢 mathematics

Propositional Dynamic Logic has Craig Interpolation: a tableau-based proof

Cet article fournit une preuve constructive que la logique dynamique propositionnelle (PDL) possède la propriété d'interpolation de Craig en employant un système de tableau cyclique avec un mécanisme de chargement et une méthode de Maehara modifiée pour calculer les interpolants, résolvant ainsi un problème ouvert de longue date après que des tentatives précédentes ont été rétractées ou critiquées.

Auteurs originaux : Manfred Borzechowski, Malvin Gattinger, Helle Hvid Hansen, Revantha Ramanayake, Francisco Trucco Dalmas, Yde Venema

Publié 2026-08-12

📖 4 min de lecture🧠 Analyse approfondie

CC BY 4.0

Auteurs originaux : Manfred Borzechowski, Malvin Gattinger, Helle Hvid Hansen, Revantha Ramanayake, Francisco Trucco Dalmas, Yde Venema

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

Imaginez que vous soyez un détective tentant de résoudre un mystère, mais que vous ne soyez autorisé à utiliser qu'un ensemble spécifique d'indices. Vous avez un long rapport compliqué provenant d'un témoin (appelons-le « l'Accusateur ») et un contre-rapport d'un autre (« le Défenseur »). Votre travail est de trouver une seule phrase courte qui explique le conflit entre eux. Cette phrase doit être le « terrain d'entente » : elle doit être vraie si l'Accusateur a raison, et elle doit être fausse si le Défenseur a raison. Crucialement, cette phrase ne peut utiliser que des mots qui apparaissent dans les deux rapports. Si l'Accusateur parle de « chats » et de « souris » et que le Défenseur parle de « chiens » et d'« os », votre phrase intermédiaire ne peut pas mentionner les « chats » ou les « os » ; elle ne peut utiliser des mots comme « animaux » ou « poursuite » que si ces mots apparaissent dans les deux récits. Dans le monde de l'informatique, ce jeu de détective est appelé la propriété d'interpolation de Craig. C'est un superpouvoir qui aide les ordinateurs à comprendre comment différentes parties d'un système se rapportent les unes aux autres sans se laisser confondre par des détails non pertinents.

Le jeu de détective spécifique que ce document traite concerne la Logique Dynamique Propositionnelle (LDP). Voyez la LDP comme un langage décrivant comment les programmes informatiques se comportent. C'est comme un livre de règles pour un jeu vidéo qui dit des choses telles que : « Si vous appuyez sur 'A' puis sur 'B', vous allez sauter », ou « Si vous continuez d'appuyer sur 'X', vous finirez par voler ». La partie délicate est le « éventuellement » ou le « continuer à faire cela indéfiniment », ce qui rend la logique très puissante mais aussi très difficile à résoudre. Pendant des décennies, des mathématiciens et des informaticiens ont tenté de prouver que ce livre de règles spécifique (la LDP) possède ce superpouvoir d'interpolation. Trois équipes différentes ont tenté de résoudre l'énigme, mais leurs solutions ont été jugées incomplètes, laissant la question ouverte et frustrante.

Ce document résout enfin le mystère. Les auteurs, une équipe de chercheurs d'Allemagne et des Pays-Bas, ont construit une toute nouvelle preuve rigoureuse que la Logique Dynamique Propositionnelle possède bel et bien la propriété d'interpolation de Craig. Ils n'ont pas seulement deviné ; ils ont construit un outil spécifique appelé « système de tableau cyclique ». Imaginez ce système comme un arbre géant et ramifié où vous tentez de décomposer un puzzle logique complexe en morceaux de plus en plus petits. Habituellement, ces arbres croissent indéfiniment, mais les auteurs ont ajouté un mécanisme de « chargement » spécial qui agit comme un filet de sécurité. Si l'arbre commence à boucler sur lui-même (ce qui arrive lorsque les programmes répètent des actions), ce mécanisme reconnaît la boucle et arrête la croissance, garantissant que la preuve reste finie et gérable.

En utilisant ce nouvel outil de construction d'arbres, les auteurs ont montré que pour toute proposition logique valide en LDP, on peut toujours trouver cette « phrase intermédiaire » parfaite (l'interpolant) qui relie deux côtés d'un argument en utilisant uniquement leur vocabulaire commun. Ils n'ont pas seulement prouvé qu'elle existe ; ils ont montré exactement comment la calculer. Ils ont même écrit un programme informatique dans un langage appelé Haskell qui peut effectuer ce calcul pour vous, et ils travaillent actuellement sur une seconde couche de preuve utilisant un assistant numérique appelé « Lean » pour vérifier que leurs mathématiques sont 100 % correctes. Bien qu'ils aient résolu l'énigme principale, ils admettent que certaines questions plus petites et connexes — comme savoir si cela fonctionne pour une version simplifiée de la logique sans les commandes de « test » — restent ouvertes pour de futurs détectives à résoudre. Mais pour l'instant, la grande question est tranchée : la LDP possède le superpouvoir de l'interpolation, et nous savons désormais exactement comment l'utiliser.

Résumé Technique : La Logique Dynamique Propositionnelle possède l'Interpolation de Craig

1. Le Problème

L'article traite de la question ouverte de longue date de savoir si la Logique Dynamique Propositionnelle (PDL) possède la Propriété d'Interpolation de Craig (PIC). La PIC stipule que pour toute implication valide $\phi \to \psi$ , il existe un interpolant $\theta$ tel que $\phi \to \theta$ et $\theta \to \psi$ sont valides, et $\theta$ ne contient que des lettres propositionnelles et des programmes atomiques communs à $\phi$ et $\psi$ .

Bien que la PDL soit une logique modale bien étudiée avec des résultats établis de décidabilité et de complétude, son statut en matière d'interpolation est resté incertain pendant des décennies. La littérature contient trois tentatives antérieures de preuve d'interpolation :

Leivant (1981) : A revendiqué une preuve, plus tard réfutée par Kracht (1999) pour des raisons incorrectes, bien qu'une lacune réelle subsiste dans la preuve de Leivant.
Borzechowski (1988) : Une thèse de master (Diplomarbeit) revendiquant une preuve, qui a reçu peu d'attention et a été rejetée par certains comme étant invérifiable.
Kowalski (2002) : A revendiqué une preuve, qui a été réfutée et officiellement retirée en 2004.

La difficulté réside dans le fait que la PDL est une logique de point fixe modal (en raison de l'opérateur d'itération $*$ ). Bien que l'interpolation ait été établie pour le $\mu$ -calcul complet et son fragment sans alternance via des systèmes de preuves cycliques, les contraintes spécifiques de la PDL rendent difficile la garantie que les solutions des équations de point fixe caractérisant les interpolants puissent être exprimées au sein même de la PDL, plutôt que de nécessiter la pleine puissance expressive du $\mu$ -calcul.

2. Méthodologie

Les auteurs fournissent une preuve constructive basée sur un système de tableau cyclique et une adaptation de la méthode de Maehara de type preuve-théorique.

2.1. Un Système de Tableau Cyclique pour la PDL

Les auteurs définissent un nouveau système de tableau pour la PDL qui opère sur des séquents scindés (paires d'ensembles de formules). Les caractéristiques clés incluent :

Raisonnement Local vs Modal : Le système distingue entre les règles locales (raisonnement propositionnel et déploiement de programmes au sein d'un seul état) et les règles modales (mouvement entre les états dans un modèle de Kripke).
Mécanisme de Déploiement : Au lieu des règles de réduction standard pour chaque constructeur de programme, le système utilise un mécanisme de "chargement". Les formules de la forme $[\alpha]\psi$ (où $\alpha$ est non atomique) sont déployées en un ensemble fini de séquents basés sur des "profils de tests". Cet ensemble, noté $\text{unfold}_\square(\alpha, \psi)$ , représente la disjonction de tous les chemins d'exécution possibles de $\alpha$ où des tests spécifiques réussissent ou échouent.
Gestion de l'Itération : Pour empêcher le déploiement local infini de formules comme $[\alpha^*]\psi$ , le système élimine les occurrences régénérées de la formule durant le processus de déploiement. Cela repose sur l'observation que $[\alpha^*]\psi$ est un plus grand point fixe.
Preuves Cycliques : Le système autorise les "répétitions" (nœuds avec des étiquettes identiques à un ancêtre).
- Répétitions de chemin chargé (Loaded-path repeats) : Une répétition où le chemin de l'ancêtre (compagnon) vers le nœud actuel consiste entièrement de nœuds chargés. Elles sont traitées comme des feuilles "réussies" (indiquant une boucle qui satisfait la formule).
- Répétitions libres (Free repeats) : Une répétition où le chemin contient des nœuds non chargés. Elles sont traitées comme des feuilles "échouées", indiquant un potentiel contre-modèle.
Terminaison : Le système assure la finitude en imposant que toutes les répétitions libres et les répétitions de chemin chargé soient des feuilles, et en utilisant la clôture de Fischer-Ladner pour borner l'ensemble des formules.

2.2. Interpolation via Quasi-Tableaux et Équations de Point Fixe

Pour construire l'interpolant, les auteurs adaptent la méthode de Maehara au contexte cyclique :

Clusters : Le tableau est vu comme un graphe avec des arêtes de retour des répétitions vers les compagnons. Les composantes fortement connexes (SCC) de ce graphe sont appelées "clusters".
Quasi-Tableaux : Pour un cluster propre (une SCC non singulière), les auteurs définissent un "quasi-tableau". Cette structure est utilisée pour mettre en place un système d'équations caractérisant l'interpolant.
Pré-interpolants : La méthode définit des "pré-interpolants" pour les nœuds du quasi-tableau via une induction de la feuille vers la racine.
- Aux nœuds de sortie (feuilles ne faisant pas partie du cluster), le pré-interpolant est l'interpolant du nœud de sortie (supposé exister par induction).
- Aux feuilles de répétition, le pré-interpolant est une variable propositionnelle interne $q_x$ .
- Aux nœuds compagnons, le pré-interpolant est défini comme la solution d'une équation de point fixe. Plus précisément, si un compagnon $x$ a un enfant $y$ avec un pré-interpolant $\iota_y \equiv \bigwedge_i [\alpha_i]q_x \wedge \bigwedge_j [\beta_j]q_{z_j} \wedge \psi$ , le pré-interpolant pour $x$ est défini comme $\iota_x := [(\bigcup_i \alpha_i)^*](\bigwedge_j [\beta_j]q_{z_j} \wedge \psi)$ .
Résolution dans la PDL : L'intuition cruciale est que cette construction spécifique garantit que les solutions des équations de point fixe restent dans le langage de la PDL. L'utilisation de l'opérateur d'itération $*$ dans la définition de $\iota_x$ résout efficacement l'équation $\iota_x \equiv \iota_y\langle q_x \mapsto \iota_x \rangle$ au sein de la PDL.
Interpolant Final : L'interpolant pour la racine du cluster est obtenu en substituant les variables internes du pré-interpolant de la racine par les formules de région correspondantes (disjonctions des côtés gauches des séquents scindés).

3. Contributions Clés et Résultats

Preuve de la PIC pour la PDL : L'article établit que la PDL possède la Propriété d'Interpolation de Craig.
Définissabilité de Beth : Comme corollaire, l'article prouve que la PDL possède la Propriété de Définissabilité de Beth (puisque la PIC implique la définissabilité de Beth en présence d'un théorème de déduction).
Algorithme Constructif : La preuve est constructive. Les auteurs fournissent un algorithme clair pour calculer les interpolants à partir d'un tableau fermé.
Vérification Formelle : Les auteurs ont partiellement formalisé la preuve dans le prouveur de théorèmes interactif Lean 4. Au moment de la rédaction de l'article, les théorèmes de Sonde et de Complétude, ainsi que plusieurs lemmes de support, ont été vérifiés.
Implémentation : Une implémentation en Haskell du système de tableau et de la construction de l'interpolant est fournie, disponible via une interface web.

4. Signification et Revendications

L'article prétend résoudre un puzzle dans la littérature concernant le statut d'interpolation de la PDL, fournissant la première preuve vérifiée qui surmonte les lacunes des tentatives précédentes.

Résolution des Problèmes Historiques : Les auteurs abordent explicitement l'histoire des tentatives échouées, notant que leur approche s'appuie sur les idées centrales de Borzechowski (1988) mais formalise rigoureusement la gestion des preuves cycliques et la construction des interpolants au sein du langage de la PDL.
Nouveauté Méthodologique : L'article souligne que si la méthode de Maehara est standard pour les preuves non cycliques, son application aux preuves cycliques (logiques de point fixe) nécessite la résolution d'équations de point fixe. Les auteurs démontrent que pour la PDL, ces solutions peuvent être exprimées en utilisant l'opérateur d'itération propre à la logique, un résultat non trivial qui distingue la PDL d'autres fragments où de telles solutions pourraient nécessiter le $\mu$ -calcul complet.
Questions Ouvertes : Les auteurs notent modestement que leur méthode repose sur la présence de programmes de test ( $\tau?$ ). Par conséquent, il reste une question ouverte de savoir si le fragment sans tests de la PDL possède l'interpolation, car leur construction génère généralement des interpolants contenant des tests même lorsque l'entrée est sans tests. Ils laissent également ouverte l'extension de leur méthode à d'autres variantes de la PDL (par exemple, avec la converse ou l'intersection) et les implications pour l'Algèbre de Kleene avec Tests (KAT).

En résumé, l'article fournit une preuve définitive et constructive de l'Interpolation de Craig pour la PDL en utilisant un nouveau système de tableau cyclique et une technique spécialisée de résolution de point fixe pour les interpolants, soutenue à la fois par une implémentation en Haskell et une vérification formelle partielle dans Lean.