A Strategy Language for Controlled Proof Search

Sintesi Tecnica: Un Linguaggio di Strategia per la Ricerca Controllata di Dimostrazioni

Enunciato del Problema
Nella deduzione automatica, la completezza statica di un calcolo logico (l'esistenza di una dimostrazione per ogni teorema) non garantisce la completezza dinamica di un dimostore (la capacità di trovare effettivamente tale dimostrazione). Nelle logiche semi-decidibili, le regole di inferenza possono generare un numero infinito di successori. Se una strategia di ricerca della dimostrazione impiega un'esplorazione non equa — come un approccio ingenuo di tipo depth-first che privilegia indefinitamente un ramo — può posticipare le inferenze rilevanti all'infinito, fallendo nel scoprire dimostrazioni valide anche quando esistono. Questo problema è particolarmente acuto in framework come Pgeon, che separano le regole di inferenza dalle strategie di ricerca della dimostrazione, poiché il design della politica di esplorazione diventa un determinante critico del successo.

Metodologia
Il documento introduce un linguaggio di strategia formale per Pgeon, un framework di meta-prover che compila specifiche dichiarative di calcoli logici in dimostori eseguibili. Il nucleo dello spostamento metodologico consiste nel modellare la ricerca della dimostrazione non come una relazione tra stati, ma come l'enumerazione di stati di dimostrazione tramite stream.

1. Semantica Formale: Uno stato di dimostrazione ($\Sigma$) è trattato come un albero di dimostrazione parzialmente costruito. Una strategia è definita come una funzione $s: \Sigma \to \text{Str}(\Sigma)$, che mappa uno stato a uno stream (finito o infinito) di stati successivi. Ciò rende esplicita la non-determinismo:

   • Un empty stream rappresenta il fallimento.
   • Uno stream con un singolo elemento rappresenta il successo deterministico.
   • Uno stream con molteplici elementi rappresenta il branching non deterministico.
   • Stream infiniti rappresentano regole che possono generare un numero illimitato di successori.

2. Combinatori: Il linguaggio fornisce un insieme di operatori per comporre queste strategie, distinguendo tra esplorazione polarizzata (depth-first) ed equa (interleaved):

   • Composizione Sequenziale ($;$): Applica una strategia ai risultati di un'altra.
   • Scelta Polarizzata a Sinistra ($\parallel$): Tenta la prima strategia; se questa fallisce (empty stream), ricorre alla seconda.
   • Composizione Sequenziale Equa ($\&;$): Intercala i risultati delle applicazioni sequenziali utilizzando la diagonalizzazione ($\triangle$), garantendo che se un risultato è raggiungibile in passi finiti, esso verrà eventualmente esplorato.
   • Scelta Equa ($\&|$): Intercala equamente i risultati di due strategie alternative.
   • Ripetizione ($*$): Definita come un punto fisso minimo tramite composizione sequenziale equa ($\mu X. \text{id} \&; (s \&; X)$), assicurando che tutte le profondità di iterazione finita siano esplorate anziché procedere strettamente in modalità depth-first.

3. Operazioni Primitive: Il linguaggio include regole primitive ($r$) e un operatore di applicazione esaustiva ($r!$) che applica una regola a tutti i match ammissibili in uno stato.

Contributi Chiave

• Semantica di Stream Composizionale: Il documento fornisce un'algebra composizionale per i combinatori di strategia dove lo spazio di ricerca è reificato come un oggetto di prima classe (uno stream). Ciò consente di ragionare sulla fairness e sull'enumerazione indipendentemente dai dettagli implementativi come la disciplina dello stack o le continuazioni.
• Meccanismi di Fairness: Introducendo operatori di interleaving basati sulla diagonalizzazione ($\&;$ e $\&|$), il framework affronta il problema della "starvation" (inedia) in cui rami infiniti impediscono la scoperta di dimostrazioni finite.
• Linguaggio di Strategia Formale per Pgeon: Il lavoro formalizza la componente di strategia del framework Pgeon, astrarre il controllo del flusso della ricerca della dimostrazione in un linguaggio dichiarativo.

Risultati e Casi di Studio
Il documento dimostra l'espressività ed l'efficacia dell'approccio attraverso due casi di studio:

1. Logica del Primo Ordine (LK): Gli autori affrontano l'interazione tra chiusura (unificazione) e saturazione delle regole. Una strategia ingenua di ripetuta applicazione delle regole spesso fallisce nel trovare dimostrazioni perché si impegna su istanze specifiche troppo presto. La strategia proposta, $(\odot^* \&; (\alpha \parallel \delta \parallel \beta \parallel \gamma!)^*)^*$, utilizza la composizione equa per intercalare i tentativi di chiusura con la saturazione delle regole. Ciò assicura che diverse scelte di unificazione siano esplorate attraverso tutti i livelli di ricerca, impedendo al sistema di incastrarsi in loop di istanziazione infinita mentre perde una derivazione di chiusura.

2. Logica Modale (S4): In S4, la regola non deterministica $\theta$ (rimozione arbitraria di formule) è necessaria per abilitare l'applicazione della regola modale S4 ma rischia di scartare formule necessarie per la chiusura. Un uso incontrollato di $\theta$ porta a vicoli ciechi. Gli autori propongono una strategia combinata $\theta^* \&; \text{S4}$, che esplora equamente tutti i modi di rimuovere le formule per abilitare le applicazioni di S4. Questa è integrata in una strategia più ampia $((\alpha \parallel \beta \parallel T)^*; (\theta^* \&; \text{S4}))^*$, garantendo che se un'applicazione riuscita di S4 richiede un sottoinsieme specifico di formule rimosse, tale configurazione venga comunque raggiunta senza starvation.

Significatività
Il documento sostiene che questo approccio offre una base principata e modulare per specificare e analizzare procedure di ricerca della dimostrazione. Separando le regole di inferenza dalle strategie di ricerca e fornendo un linguaggio formale con semantica composizionale, il framework permette l'esplorazione sistematica degli spazi di ricerca nelle logiche semi-decidibili. Dimostra che la completezza dinamica può essere raggiunta anche quando strategie naive depth-first falliscono, gestendo esplicitamente la fairness attraverso l'interleaving degli stream. Il lavoro abilita il ragionamento sulle procedure di ricerca della dimostrazione a un livello astratto, indipendente dall'implementazione specifica del dimostore.