Encoding Peano Arithmetic in a Minimal Fragment of Separation Logic

1. Il Problema

La logica di separazione (Separation Logic - SL) è uno strumento fondamentale per la verifica formale di programmi che manipolano strutture dati dinamiche (heap). Tuttavia, quando si verifica software che coinvolge calcoli numerici, è necessario estendere la SL con l'aritmetica.
La domanda centrale della ricerca è: fino a che punto un frammento minimale della logica di separazione, arricchito solo con concetti aritmetici di base, mantiene la decidibilità?
In generale, si spera che combinare un frammento decidibile della SL con l'aritmetica di Presburger (che è decidibile) produca un sistema decidibile. Gli autori sfidano questa ipotesi dimostrando che anche un'estensione estremamente minima può portare all'indecidibilità.

2. Metodologia

Gli autori studiano un frammento specifico della logica di separazione chiamato SLN (Separation Logic with Numbers), che include:

• Il predicato di puntamento intuitivo (intuitionistic points-to): $t_1 \mapsto t_2$.
• La costante $0$.
• La funzione successore $s$.
• Connettivi booleani e quantificatori del primo ordine.
• Nota: Il frammento esclude la congiunzione separata ($*$) e il "magic wand" ($-\ast$), rendendolo sintatticamente molto semplice.

Per dimostrare l'espressività di SLN, gli autori sviluppano una traduzione dalle formule $\Pi^0_1$ dell'Aritmetica di Peano (PA) a formule in SLN. La tecnica chiave consiste nel simulare le operazioni aritmetiche (addizione, moltiplicazione e disuguaglianza) utilizzando una tabella di operazioni codificata nell'heap (memoria).

Meccanismo di Codifica

L'idea centrale è che l'heap non deve solo contenere dati, ma deve anche contenere una "tabella di verità" per le operazioni aritmetiche.

• Struttura della tabella: L'heap contiene celle contigue che rappresentano le triple o quadruple di dati.
  • Per l'addizione ($x+y=z$): una cella con tag 0, seguita da $x+3$, $y+3$, e il risultato $z+3$.
  • Per la moltiplicazione ($x \times y = z$): tag 1, seguito da $x+3$, $y+3$, e $z+3$.
  • Per la disuguaglianza ($x \le y$): tag 2, seguito da $x+3$ e $y+3$.
• Offset: Viene usato un offset di 3 per evitare collisioni con i tag (0, 1, 2).
• Condizione della Tabella ($H$): Viene definita una formula logica $H$ che impone all'heap di rispettare le regole ricorsive dell'aritmetica (es. $s(x) + y = s(x+y)$). Se l'heap contiene un'entry per un'operazione, le celle successive devono contenere il risultato corretto.

La traduzione di una formula PA in SLN ($A^\circ$) sostituisce i simboli aritmetici ($+, \times, \le$) con predicati che consultano questa tabella nell'heap (es. $Add(x, y, z)$).

3. Contributi Chiave

1. Teorema di Rappresentazione per $\Pi^0_1$:
   Gli autori dimostrano che esiste una traduzione che preserva validità e non-validità per le formule $\Pi^0_1$ (universali) dell'Aritmetica di Peano.

   • Risultato: Una formula $\Pi^0_1$ è valida nel modello standard dell'aritmetica se e solo se la sua traduzione in SLN è valida sotto l'interpretazione standard.
   • Meccanismo: La validità in SLN richiede che la formula sia vera per tutti gli heap. Se l'aritmetica è corretta, esiste un heap "grande" (tabella semplice) che contiene tutte le entry necessarie. Se l'heap è troppo piccolo, la formula diventa trivialmente vera (perché le premesse della tabella non sono soddisfatte), ma la validità universale richiede che sia vera anche negli heap grandi dove l'aritmetica è completa.

2. Limiti della Traduzione (Controesempio $\Sigma^0_1$):
   Viene dimostrato che la traduzione non funziona per le formule $\Sigma^0_1$ (esistenziali).

   • Esempio: La formula $\exists x (x + 0 \neq x)$ è falsa in PA. Tuttavia, nella traduzione SLN, è possibile scegliere un heap troppo piccolo che non contiene l'entry per $x+0$. In tal caso, il predicato $Add(x, 0, z)$ diventa vero (perché la premessa è falsa), rendendo l'intera formula valida in SLN. Questo mostra che la preservazione della validità fallisce per le formule esistenziali.

3. Indecidibilità:
   Poiché il problema della validità per le formule $\Pi^0_1$ in PA è indecidibile (equivalente al problema dell'arresto), ne consegue che la validità in SLN è indecidibile.

4. Completezza $\Pi^0_1$:
   Gli autori stabiliscono che il problema della validità in SLN è $\Pi^0_1$-completo.

   • Hardness: Deriva direttamente dalla traduzione da PA.
   • Membership: Viene dimostrato che il problema del model-checking (verificare se una formula è vera in un dato heap e assegnazione) è decidibile. Poiché la validità è "per tutti gli heap e assegnazioni", e il model-checking è decidibile, la validità può essere espressa come un predicato $\Pi^0_1$.

5. Dimostrazione Alternativa:
   Viene fornita una seconda prova di indecidibilità basata sulla riduzione dal problema della validità nella teoria dei modelli finiti (Teorema di Trakhtenbrot), codificando strutture finite direttamente nell'heap.

4. Risultati Principali

• Indecidibilità Sorprendente: Anche un frammento di SL senza congiunzione separata ($*$) e con solo un predicato di puntamento, arricchito solo da $0$e$s$, è sufficiente per codificare l'aritmetica di Peano completa per le formule $\Pi^0_1$.
• Complessità: Il problema della validità per SLN è esattamente $\Pi^0_1$-completo.
• Distinzione tra $\Pi^0_1$ e $\Sigma^0_1$: La traduzione preserva la validità solo per le formule universali. Le formule esistenziali non possono essere tradotte preservando la validità a causa della natura parziale degli heap (un heap può "mancare" di entry che renderebbero falsa una formula esistenziale in PA, ma che in SLN la rendono vera per mancanza di controesempi nell'heap).

5. Significato e Implicazioni

• Confini dell'Espressività: Questo lavoro ridefinisce i confini di ciò che è necessario per rendere la logica di separazione indecidibile. Non sono necessari predicati complessi o strutture dati avanzate; basta la capacità di codificare tabelle di operazioni nell'heap tramite il puntamento.
• Verifica dei Programmi: Suggerisce che qualsiasi sistema di verifica che tenti di integrare la logica di separazione con l'aritmetica deve affrontare l'indecidibilità se permette di ragionare su proprietà universali complesse (come la correttezza totale o la terminazione forte) senza restrizioni severe sulla struttura dell'heap.
• Teoria della Computabilità: Dimostra una connessione profonda tra la struttura della memoria (heap) e la teoria dei numeri, mostrando come la limitatezza fisica della memoria (in un modello ideale) possa essere sfruttata per simulare l'aritmetica infinita attraverso la quantificazione universale su tutti i possibili stati di memoria.

In sintesi, il paper dimostra che la semplicità sintattica di SLN è ingannevole: l'aggiunta di semplici funzioni aritmetiche a un nucleo minimale di logica di separazione è sufficiente a catturare la complessità dell'aritmetica di Peano, rendendo il problema della validità indecidibile e $\Pi^0_1$-completo.