Encoding Peano Arithmetic in a Minimal Fragment of Separation Logic

1. Problématique

L'article s'attaque à la question fondamentale de la décidabilité de la validité dans les extensions de la logique de séparation (Separation Logic - SL) par l'arithmétique.

• Contexte : La logique de séparation est un outil puissant pour la vérification de programmes manipulant la mémoire (tas/heap). Pour vérifier des systèmes impliquant des calculs numériques, il est nécessaire d'étendre la SL avec de l'arithmétique.
• Hypothèse initiale : On pourrait s'attendre à ce qu'une extension minimale de la SL avec une arithmétique décidable (comme l'arithmétique de Presburger) reste décidable.
• Problème central : Les auteurs démontrent le contraire : même une extension extrêmement restreinte de la logique de séparation, ne contenant que le prédicat de pointage intuitionniste ($\to$), la constante $0$ et la fonction successeur $s$, devient indécidable pour la validité. Plus précisément, ce fragment est suffisamment expressif pour encoder toutes les formules $\Pi^0_1$ de l'arithmétique de Peano (PA).

2. Méthodologie

Les auteurs proposent une traduction formelle de l'arithmétique de Peano vers un fragment minimal de logique de séparation, noté SLN.

A. Définition du Fragment SLN

Le fragment SLN est défini comme suit :

• Termes : Variables, $0$, et $s(t)$ (successeur).
• Formules : Égalité, prédicat de pointage $t_1 \to t_2$ (intuitionniste, signifiant qu'il existe une cellule à l'adresse $t_1$ contenant $t_2$), connecteurs booléens et quantificateurs du premier ordre.
• Absence de : Conjonction séparatrice ($*$) et implication séparatrice ($-\ast$), qui sont souvent sources de complexité dans d'autres fragments de SL.

B. Technique de Codage : Les Tables d'Opération

Le cœur de la preuve réside dans la capacité à encoder les opérations arithmétiques complexes (addition, multiplication, inégalité) en utilisant uniquement la structure de la mémoire (le tas).

• Représentation du tas : Le tas est vu comme une fonction partielle finie $h : \mathbb{N} \to_{fin} \mathbb{N}$.
• Encodage des opérations : Les auteurs construisent des "tables d'opération" dans le tas. Chaque entrée de la table est stockée dans une séquence de cellules contiguës.
  • Tags : Les valeurs $0, 1, 2$ servent de tags pour distinguer l'addition, la multiplication et l'inégalité.
  • Offset : Les arguments et résultats sont encodés avec un décalage de $+3$ pour éviter les collisions avec les tags.
  • Structure :
    • Addition : $0, x+3, y+3, (x+y)+3$.
    • Multiplication : $1, x+3, y+3, (x \times y)+3$.
    • Inégalité : $2, x+3, y+3$ (si $x \le y$).
• Condition de validité du tas ($H$) : Une formule $H$ est définie pour garantir que le tas contient une table d'opérations cohérente (respectant les règles de récurrence de l'addition et de la multiplication, et la transitivité de l'inégalité).

C. Traduction des Formules

Les auteurs définissent une traduction $(\cdot)^\circ$ des formules bornées de PA vers SLN :

• Les opérations $+$, $\times$ et $\le$ sont remplacées par des prédicats logiques ($Add$, $Mult$, $Ineq$) qui interrogent la table d'opération dans le tas.
• Gestion de la finitude du tas : Puisqu'un tas donné peut être trop petit pour contenir toutes les entrées nécessaires pour une formule donnée, la traduction utilise une implication logique. Par exemple, $x + y = z$ devient $H \to Add(x, y, z)$. Si le tas ne contient pas la table nécessaire, l'implication est trivialement vraie.
• Quantificateurs bornés : La traduction des quantificateurs $\exists x \le t$ et $\forall x \le t$ est subtile pour gérer les cas où la table est incomplète, en utilisant des disjonctions avec la négation de la présence de l'entrée dans la table.

D. Preuve de Préservation

L'objectif est de prouver qu'une formule $\Pi^0_1$ de PA est valide (dans le modèle standard de l'arithmétique) si et seulement si sa traduction est valide dans SLN (pour tous les tas et assignations).

• Lemme clé : Pour toute formule donnée, il existe un "tas de table simple" ($h_n$) suffisamment grand pour contenir toutes les opérations nécessaires.
• Monotonie : Si une propriété arithmétique est vraie dans un tas suffisamment grand (où la table est complète), elle l'est dans tous les tas (car la validité de SLN exige que la formule soit vraie pour tous les tas, y compris ceux qui ne contiennent pas la table, rendant l'implication vraie, et ceux qui la contiennent, où l'arithmétique est correcte).

3. Contributions Clés

1. Théorème de Représentation : Démonstration que le fragment SLN (avec seulement $\to$, $0$, $s$) est capable d'encoder toutes les formules $\Pi^0_1$ de l'arithmétique de Peano.
2. Indécidabilité de la Validité : Conséquence directe du théorème précédent, la validité dans SLN est indécidable. Cela contredit l'intuition selon laquelle l'ajout d'arithmétique simple à une logique de séparation faible devrait rester décidable.
3. Complétude $\Pi^0_1$ : Les auteurs établissent que le problème de validité de SLN est $\Pi^0_1$-complet.
   • Hardness : Dérivé de l'encodage de PA.
   • Upper Bound : Dérivé de la preuve que le problème de vérification de modèle (model-checking) pour SLN est décidable (en bornant l'espace de recherche des variables liées aux prédicats de pointage et en réduisant le reste à l'arithmétique du successeur, décidable).
4. Limites de l'Encodage : Ils montrent que cette traduction ne préserve pas la validité pour les formules $\Sigma^0_1$. Un contre-exemple est fourni montrant qu'une formule $\Sigma^0_1$ non valide en PA peut devenir valide en SLN sous cette traduction (en exploitant les tas "trop petits" qui rendent les conditions d'existence trivialement vraies).
5. Preuve Alternative : Une deuxième preuve d'indécidabilité est fournie via une réduction depuis la théorie des modèles finis (Théorème de Trakhtenbrot), codant des structures finies dans des tas.

4. Résultats Principaux

• Indécidabilité : Le problème de validité pour le fragment SLN est indécidable.
• Complexité : Le problème de validité est $\Pi^0_1$-complet.
• Expressivité Surprenante : L'ajout de seulement $0$ et $s$ à un prédicat de pointage intuitionniste (déjà connu pour être décidable sans arithmétique) suffit à atteindre la puissance expressive de l'arithmétique de Peano pour les classes $\Pi^0_1$.
• Distinction $\Pi^0_1$ vs $\Sigma^0_1$ : La traduction fonctionne pour les formules universelles ($\Pi^0_1$) mais échoue pour les existentielles ($\Sigma^0_1$) en raison de la nature de la sémantique de validité (tous les tas) qui permet de "tricher" avec des tas incomplets pour les formules existentielles.

5. Signification et Impact

• Frontières de la Logique de Séparation : Ce travail redéfinit les limites de ce qui est décidable dans la logique de séparation. Il montre que même sans conjonction séparatrice ni prédicats inductifs complexes, l'interaction entre la structure de la mémoire et l'arithmétique simple suffit à engendrer l'indécidabilité.
• Vérification de Programmes : Pour la vérification formelle, cela implique que l'on ne peut pas espérer un algorithme général de décision pour des systèmes combinant logique de séparation et arithmétique, même dans des configurations très simples.
• Théorie des Modèles : La connexion établie entre les propriétés de consistance des systèmes logiques (qui sont souvent $\Pi^0_1$) et la validité en SLN ouvre de nouvelles perspectives pour l'analyse de la puissance expressive des logiques de spécification.
• Fondements Mathématiques : La preuve de la complétude $\Pi^0_1$ fournit une caractérisation précise de la complexité de ce fragment, comblant un vide dans la littérature sur les fragments minimaux de la logique de séparation.

En résumé, cet article démontre que la simplicité syntaxique d'un fragment de logique de séparation peut masquer une complexité computationnelle maximale (indécidabilité), dès lors qu'il est enrichi d'opérations arithmétiques de base et interprété sur des structures de mémoire.