Towards Weak Stratification for Logics of Definitions

Sintesi Tecnica: Verso la Stratificazione Debole per le Logiche delle Definizioni

Enunciato del Problema
La logica delle definizioni è una famiglia di logiche utilizzate per codificare e ragionare su giudizi specificati tramite regole di inferenza, dove i predicati atomici sono associati a formule logiche che possono dipendere dal predicato stesso. Per risolvere la circolarità apparente inerente a tali definizioni, gli approcci standard impongono una condizione di stratificazione, assicurando che un predicato non compaia negativamente (a sinistra di un'implicazione) nel corpo della propria definizione. Questa condizione tratta efficacemente le definizioni come operatori di punto fisso monotoni.

Tuttavia, molte specifiche utili, in particolare quelle riguardanti le relazioni logiche per dimostrare proprietà di linguaggi di programmazione, richiedono definizioni in cui il predicato compaia negativamente. Nella logica $\mathcal{G}$, che sta alla base dell'assistente alla dimostrazione Abella, tali definizioni sono vietate. Tiu [19] ha precedentemente introdotto una logica chiamata $\mathcal{LD}$ che ammorbidisce la condizione di stratificazione verso una stratificazione debole (permettendo occorrenze negative a patto che il livello della testa sia strettamente maggiore del livello dell'occorrenza negativa), ma $\mathcal{LD}$ era limitata a un frammento centrale. Essa mancava del supporto per il quantificatore nabla ($\nabla$), essenziale per ragionare su nomi e freschezza tramite costanti nominali, e per le definizioni induttive generali oltre l'induzione sui numeri naturali. La sfida affrontata in questo lavoro è quella di estendere la logica delle definizioni per includere la stratificazione debole mantenendo la coerenza in presenza di $\nabla$ e di definizioni induttive generali.

Metodologia
Il documento definisce una nuova logica, $\mathcal{LD}\mu\nabla$, che estende la $\mathcal{LD}$ di Tiu con la quantificazione nabla e le definizioni induttive generali. La metodologia procede in tre fasi principali:

1. Sintassi e Semantica di $\mathcal{LD}\mu\nabla$:
   La logica è formulata come un'estensione del calcolo sequente del primo ordine con un insieme di definizioni $\mathcal{D}$ e un insieme di definizioni induttive $\mathcal{I}$.

   • Stratificazione Debole: Un insieme di definizioni $\mathcal{D}$ è debolmente stratificato se per ogni clausola $H \triangleq_X B$ e sostituzione di base $\rho$, $\text{lvl}(H\rho) \ge \text{lvl}(B\rho)$. Fondamentalmente, ciò permette occorrenze negative del predicato definito se il livello della testa è strettamente maggiore del livello dell'occorrenza negativa.
   • Stratificazione Stretta per l'Induzione: Il documento impone una condizione più stretta sulle definizioni induttive $\mathcal{I}$: esse devono essere strettamente stratificate (il livello di un predicato atomico di base deve essere indipendente dai suoi argomenti). Questa restrizione è necessaria per prevenire l'incoerenza quando si combina l'induzione con la stratificazione debole.
   • Quantificatore Nabla: La logica incorpora il quantificatore $\nabla$ per gestire le costanti nominali e la freschezza, distinguendo tra istanze generiche e specifiche di nomi.

2. Logica di Base e Interpretazione:
   Per provare la coerenza, gli autori costruiscono una versione di base della logica, $\mathcal{LD}\mu\nabla_\infty$, dove tutte le formule sono di base (senza variabili proprie).

   • Lemma di Base (Grounding Lemma): Un passaggio tecnico chiave è dimostrare che qualsiasi derivazione in $\mathcal{LD}\mu\nabla$ può essere interpretata come una derivazione in $\mathcal{LD}\mu\nabla_\infty$ tramite una sostituzione di base. Ciò riduce il problema della coerenza della logica completa alla coerenza della logica di base.
   • Regole Infinitarie: In $\mathcal{LD}\mu\nabla_\infty$, le regole standard $\forall R$ e $\exists L$ sono sostituite da regole infinitarie che quantificano su tutti i termini di base, e la regola $\mu L$ per l'induzione è similmente espansa per coprire tutte le istanze di base.

3. Eliminazione del Cut:
   Il cuore della prova di coerenza è l'eliminazione della regola del cut (specificamente, la regola del multicut) in $\mathcal{LD}\mu\nabla_\infty$.

   • Relazione di Riduzione: Viene definita una relazione di riduzione sulle derivazioni, specificando come i cut possano essere spinti verso l'alto o eliminati.
   • Riducibilità: Seguendo la tecnica di Tait-Martin-Löf adattata da McDowell e Miller, gli autori definiscono una nozione di riducibilità (e normalizzabilità) per le derivazioni. Dimostrano che ogni derivazione in $\mathcal{LD}\mu\nabla_\infty$ è riducibile.
   • Gestione dei Casi Induttivi: Un aspetto critico della prova è la gestione dell'interazione tra stratificazione debole e induzione. Gli autori mostrano che, mentre la stratificazione debole è sufficiente per le definizioni generali, le definizioni induttive devono rimanere strettamente stratificate. Forniscono un controesempio (Sezione 3.3) dimostrando che permettere definizioni induttive debolmente stratificate porta all'incoerenza logica.

Contributi Chiave

• Definizione di $\mathcal{LD}\mu\nabla$: Il documento definisce formalmente una logica che combina la stratificazione debole, la quantificazione nabla e le definizioni induttive generali.
• Prova di Coerenza: Il contributo primario è la prova che $\mathcal{LD}\mu\nabla$ è coerente. Ciò è ottenuto dimostrando l'eliminazione del cut per la logica di base $\mathcal{LD}\mu\nabla_\infty$ ed établendo un'interpretazione di base.
• Vincoli di Stratificazione: Il lavoro chiarisce il confine tra definizioni ammissibili e non ammissibili. Dimostra che, mentre la stratificazione debole è sufficiente per le definizioni generali (abilitando le relazioni logiche), le definizioni induttive richiedono una stratificazione stretta per preservare la coerenza.
• Controesempio: Il documento fornisce un controesempio specifico che mostra come allentare la condizione di stratificazione per le definizioni induttive conduca all'incoerenza logica, giustificando la restrizione imposta su $\mathcal{I}$.

Risultati

• Coerenza: Si dimostra che la logica $\mathcal{LD}\mu\nabla$ è coerente. Di conseguenza, la logica $\mathcal{LD}\mu\nabla_\infty$ ammette derivazioni prive di cut per tutti i sequenti provabili.
• Proprietà di Inversione: Il documento stabilisce proprietà meta-teoriche per $\mathcal{LD}\mu\nabla_\infty$, inclusa l'invertibilità di varie regole di introduzione (es. $\wedge R$, $\vee L$, $\nabla R$) e la parziale invertibilità specifica per $\vee R$, $\exists R$ e le regole di definizione ($\Delta R$) quando il contesto è vuoto. Queste proprietà sono cruciali per le procedure di ricerca della prova.
• Limitazioni: Il teorema di eliminazione del cut è stabilito solo per la logica di base $\mathcal{LD}\mu\nabla_\infty$. Il documento nota che estendere questo risultato alla logica completa $\mathcal{LD}\mu\nabla$ (con variabili proprie) rimane una sfida aperta.

Significato
Il significato di questo lavoro risiede nel suo potenziale di estendere le capacità dell'assistente alla dimostrazione Abella. Abella si basa sulla logica $\mathcal{G}$, che attualmente restringe le definizioni a essere strettamente stratificate. Giustificando l'inclusione di definizioni debolmente stratificate, questa ricerca apre la strada affinché Abella possa supportare nativamente le relazioni logiche, una tecnica fondamentale per dimostrare proprietà semantiche di linguaggi di programmazione (come la sicurezza dei tipi e la correttezza dei compilatori).

Il lavoro posiziona questo contributo come un passo fondamentale verso un'estensione più ampia di $\mathcal{G}$. Mentre l'attuale risultato gestisce la stratificazione debole con $\nabla$ e l'induzione, gli autori osservano che una piena giustificazione per Abella richiederebbe ulteriori estensioni per includere la co-induzione e l'astrazione nominale. Il lavoro evidenzia inoltre la necessità di mantenere la stratificazione stretta per le definizioni induttive, un vincolo che previene le incoerenze che altrimenti deriverebbero dal mescolare la stratificazione debole con l'induzione.