Sintesi Tecnica: La Logica Dinamica Proposizionale ha l'Interpolazione di Craig

1. Il Problema

Il documento affronta la questione aperta di lunga data se la Logica Dinamica Proposizionale (PDL) possieda la Proprietà di Interpolazione di Craig (CIP). La CIP afferma che per ogni implicazione valida $\phi \to \psi$, esiste un interpolante $\theta$ tale che $\phi \to \theta$ e $\theta \to \psi$ siano valide, e $\theta$ contenga solo lettere proposizionali e programmi atomici comuni a entrambi $\phi$ e $\psi$.

Nonostante la PDL sia una logica modale ben studiata con risultati stabiliti di decidibilità e completezza, il suo stato di interpolazione è rimasto incerto per decenni. La letteratura contiene tre precedenti tentativi di provare l'interpolazione:

1. Leivant (1981): Ha rivendicato una prova, successivamente confutata da Kracht (1999) per ragioni errate, sebbene rimanga un vuoto genuino nella prova di Leivant.
2. Borzechowski (1988): Una tesi di laurea (Diplomarbeit) che rivendicava una prova, la quale ha ricevuto poca attenzione ed è stata scartata da alcuni come non verificabile.
3. Kowalski (2002): Ha rivendicato una prova, che è stata confutata e ufficialmente ritirata nel 2004.

La difficoltà sorge perché la PDL è una logica a punto fisso modale (a causa dell'operatore di iterazione $*$). Mentre l'interpolazione è stata stabilita per il full $\mu$-calculus e il suo frammento privo di alternanza tramite sistemi di prove cicliche, i vincoli specifici della PDL rendono difficile garantire che le soluzioni delle equazioni a punto fisso che caratterizzano gli interpolanti possano essere espresse all'interno della stessa PDL, piuttosto che richiedere l'intero potere espressivo del $\mu$-calculus.

2. Metodologia

Gli autori forniscono una prova costruttiva basata su un sistema di tableau ciclico e un adattamento del metodo di Maehara di tipo proof-theoretic.

2.1. Un Sistema di Tableau Ciclico per la PDL

Gli autori definiscono un nuovo sistema di tableau per la PDL che opera su sequenti divisi (coppie di insiemi di formule). Caratteristiche chiave includono:

• Ragionamento Locale vs. Modale: Il sistema distingue tra regole locali (ragionamento proposizionale e srotolamento di programmi all'interno di un singolo stato) e regole modali (movimento tra stati in un modello di Kripke).
• Meccanismo di Srotolamento (Unfolding): Invece delle standard regole di riduzione per ogni costruttore di programmi, il sistema utilizza un meccanismo di "caricamento". Le formule della forma $[\alpha]\psi$ (dove $\alpha$ non è atomico) vengono srotolate in un insieme finito di sequenti basati su "profili di test". Questo insieme, denotato $\text{unfold}_\square(\alpha, \psi)$, rappresenta la disgiunzione di tutti i possibili percorsi di esecuzione di $\alpha$ dove specifici test hanno successo o falliscono.
• Gestione dell'Iterazione: Per prevenire lo srotolamento locale infinito di formule come $[\alpha^*]\psi$, il sistema elimina le occorrenze rigenerate della formula durante il processo di srotolamento. Ciò si basa sull'osservazione che $[\alpha^*]\psi$ è un punto fisso massimo.
• Prove Cicliche: Il sistema permette "ripetizioni" (nodi con etichette identiche a un antenato).
  • Ripetizioni a percorso caricato (Loaded-path repeats): Una ripetizione in cui il percorso dall'antenato (compagno) al nodo corrente consiste interamente di nodi caricati. Questi sono trattati come foglie "di successo" (indicando un ciclo che soddisfa la formula).
  • Ripetizioni libere (Free repeats): Una ripetizione in cui il percorso contiene nodi non caricati. Questi sono trattati come foglie "di insuccesso", indicando un potenziale contro-modello.
• Terminazione: Il sistema garantisce la finitezza imponendo che tutte le ripetizioni libere e le ripetizioni a percorso caricato siano foglie, e utilizzando la chiusura di Fischer-Ladner per limitare l'insieme delle formule.

2.2. Interpolazione tramite Quasi-Tableaux ed Equazioni a Punto Fisso

Per costruire l'interpolante, gli autori adattano il metodo di Maehara al contesto ciclico:

• Cluster: Il tableau viene visto come un grafo con archi di ritorno da ripetizioni a compagni. Le componenti fortemente connesse (SCC) di questo grafo sono chiamate "cluster".
• Quasi-Tableaux: Per un cluster proprio (una SCC non singola), gli autori definiscono un "quasi-tableau". Questa struttura è utilizzata per impostare un sistema di equazioni che caratterizza l'interpolante.
• Pre-interpolanti: Il metodo definisce "pre-interpolanti" per i nodi nel quasi-tableau tramite induzione da foglia a radice.
  • Ai nodi di uscita (foglie che non fanno parte del cluster), il pre-interpolante è l'interpolante del nodo di uscita (assunto esistente per induzione).
  • Alle foglie di ripetizione, il pre-interpolante è una variabile proposizionale interna $q_x$.
  • Ai nodi compagni, il pre-interpolante è definito come la soluzione di un'equazione a punto fisso. Nello specifico, se un compagno $x$ ha un figlio $y$ con pre-interpolante $\iota_y \equiv \bigwedge_i [\alpha_i]q_x \wedge \bigwedge_j [\beta_j]q_{z_j} \wedge \psi$, il pre-interpolante per $x$ è definito come $\iota_x := [(\bigcup_i \alpha_i)^*](\bigwedge_j [\beta_j]q_{z_j} \wedge \psi)$.
• Risoluzione in PDL: L'intuizione cruciale è che questa specifica costruzione assicura che le soluzioni alle equazioni a punto fisso rimangano all'interno del linguaggio della PDL. L'uso dell'operatore di iterazione $*$ nella definizione di $\iota_x$ risolve efficacemente l'equazione $\iota_x \equiv \iota_y\langle q_x \mapsto \iota_x \rangle$ all'interno della PDL.
• Interpolante Finale: L'interpolante per la radice del cluster si ottiene sostituendo le variabili interne nel pre-interpolante della radice con le corrispondenti formule di regione (disgiunzioni dei lati sinistri dei sequenti divisi).

3. Contributi Chiave e Risultati

• Prova della CIP per la PDL: Il documento stabilisce che la PDL possiede la Proprietà di Interpolazione di Craig.
• Definibilità di Beth: Come corollario, il documento prova che la PDL possiede la Proprietà di Definibilità di Beth (poiché la CIP implica la definibilità di Beth in presenza di un teorema di deduzione).
• Algoritmo Costruttivo: La prova è costruttiva. Gli autori forniscono un algoritmo chiaro per calcolare gli interpolanti da un tableau chiuso.
• Verifica Formale: Gli autori hanno parzialmente formalizzato la prova nel theorem prover interattivo Lean 4. Al momento della stesura del documento, i teoremi di Correttezza (Soundness) e Completezza, insieme a diversi lemmi di supporto, sono stati verificati.
• Implementazione: È fornita un'implementazione in Haskell del sistema di tableau e della costruzione dell'interpolante, disponibile tramite un'interfaccia web.

4. Significato e Rivendicazioni

Il documento sostiene di risolvere un enigma nella letteratura riguardante lo stato di interpolazione della PDL, fornendo la prima prova verificata che supera le lacune dei tentativi precedenti.

• Risoluzione di Questioni Storiche: Gli autori affrontano esplicitamente la storia dei tentativi falliti, notando che il loro approccio si basa sulle idee centrali di Borzechowski (1988) ma formalizza rigorosamente la gestione delle prove cicliche e la costruzione degli interpolanti all'interno del linguaggio della PDL.
• Novità Metodologica: Il documento evidenzia che, mentre il metodo di Maehara è standard per prove non cicliche, l'applicazione alle prove cicliche (logiche a punto fisso) richiede la risoluzione di equazioni a punto fisso. Gli autori dimostrano che per la PDL, queste soluzioni possono essere espresse utilizzando l'operatore di iterazione della logica stessa, un risultato non banale che distingue la PDL da altri frammenti dove tali soluzioni potrebbero richiedere il $\mu$-calculus completo.
• Questioni Aperte: Gli autori notano con modestia che il loro metodo dipende dalla presenza di programmi di test ($\tau?$). Di conseguenza, rimane una questione aperta se il frammento privo di test della PDL possieda l'interpolazione, poiché la loro costruzione genera generalmente interpolanti contenenti test anche quando l'input è privo di essi. Lasciano inoltre aperta l'estensione del loro metodo ad altre varianti della PDL (ad esempio, con conversi o intersezione) e le implicazioni per l'Algebra di Kleene con Test (KAT).

In sintesi, il documento fornisce una prova definitiva e costruttiva dell'Interpolazione di Craig per la PDL utilizzando un nuovo sistema di tableau ciclico e una tecnica specializzata di risoluzione dei punti fissi per gli interpolanti, supportata sia da un'implementazione in Haskell che da una parziale verifica formale in Lean.