Computation by infinite descent made explicit

Problema e Motivazione
La teoria della dimostrazione non ben fondata, nata nel contesto del $\mu$-calcolo modale, permette ad alberi di dimostrazione infiniti di rappresentare il ragionamento induttivo e coinduttivo. Una sfida centrale in questo campo è definire un criterio di correttezza che distingua le dimostrazioni valide da alberi di derivazione invalidi. I criteri tradizionali, come la condizione di "traccia" (trace) o di "filo progressivo" (progressing thread), richiedono che ogni ramo infinito di un albero di dimostrazione contenga una specifica sequenza di formule in cui un punto fisso minimo viene srotolato infinitamente sulla sinistra o un punto fisso massimo sulla destra.

Tuttove, recenti lavori di Baelde et al. [BDKS22] hanno identificato i limiti delle condizioni basate sulle tracce, in particolare riguardo alla compositionalità. Essi hanno introdotto i "fili rimbalzanti" (bouncing threads) per gestire i casi in cui i tagli (cuts) interrompono le tracce, ma hanno osservato che tale condizione è indecidibile e interagisce negativamente con le regole strutturali dei sistemi di dimostrazione. Inoltre, sebbene la corrispondenza Curry-Howard veda le dimostrazioni come programmi, stabilire che le dimostrazioni non ben fondate rappresentino funzioni computabili (normalizzazione) è non banale sotto queste complesse condizioni di validità.

Questo articolo affronta il problema della compositionalità e del contenuto computazionale delle dimostrazioni non ben fondate esplorando un quadro alternativo: sistemi di dimostrazione con variabili ordinali esplicite. Questo approccio, pionieristicamente sviluppato da Dam, Gurov e Sprenger [DG02, SD03a], annota le formule di punto fisso con variabili che rappresentano approssimanti ordinali. L'articolo investiga se questo framework possa fornire un criterio di correttezza più trasparente che supporti un'interpretazione Curry-Howard robusta, potenzialmente catturando dimostrazioni che le standard condizioni di traccia mancano, pur rimanendo decidabile.

Metodologia
L'autore, Sebastian Enqvist, sviluppa un sistema di dimostrazione non ben fondato per la logica proposizionale intuizionistica estesa con definizioni induttive ($\mu$) e coinduttive ($\nu$). La metodologia centrale prevede:

1. Estensione della Sintassi: Il linguaggio è esteso con variabili ordinali esplicite e vincoli. Formule come $\mu X. A$ sono annotate come $\mu_\alpha X. A$, dove $\alpha$ è un termine ordinale (variabili $a, b, \dots$ o una costante $\infty$). I sequenti includono un albero di vincoli $O$ che rappresenta le disuguaglianze tra questi termini ordinali.
2. Criterio di Validità: Una derivazione è definita valida se, per ogni ramo infinito, esiste una catena discendente infinita di variabili ordinali ($a_0 > a_1 > a_2 > \dots$) che si verifica infine su quel ramo. Ciò rende esplicita nella sintassi l'argomento della "discesa infinita", centrale per la correttezza del ragionamento induttivo.
3. Semantica della Computabilità: L'articolo definisce una nozione di computabilità per le derivazioni chiuse. Una dimostrazione è computabile se riduce a una forma normale che soddisfa specifiche clausole induttive corrispondenti ai connettivi logici e ai punti fissi. Ad esempio, una dimostrazione di un punto fisso minimo $\mu_\infty X. A$ è computabile se riduce a una dimostrazione di un approssimante $\mu_\xi X. A$ per qualche ordinale $\xi$.
4. Riduzioni del Taglio (Cut Reductions): Viene introdotto un insieme di regole di riscrittura (riduzioni del taglio e regole di permutazione) per definire il comportamento computazionale delle dimostrazioni. Il sistema è progettato per essere confluente sotto queste specifiche regole, permettendo una nozione ben definita di normalizzazione.
5. Modellazione Categoriale: Viene costruito un sistema di categorie in cui gli oggetti sono formule chiuse e le frecce sono classi di equivalenza di dimostrazioni. L'autore dimostra che questa categoria supporta la struttura di algebra iniziale e coalgebra finale per le rispettive formule di punto fisso.

Contributi Chiave e Risultati

• Computabilità delle Dimostrazioni Valide: Il risultato primario (Teorema 4.9) stabilisce che ogni dimostrazione valida (che soddisfa la condizione della catena discendente infinita) è computabile. Ciò è provato mostrando che, se una dimostrazione fosse incomputabile, si potrebbe costruire un ramo infinito privo di una catena discendente di ordinali, contraddicendo la condizione di validità.
• Normalizzazione per Formule Finitarie: Come conseguenza del risultato di computabilità, l'articolo dimostra che le dimostrazioni di "formule finitarie" (formule costruite con $\top, \land, \lor, \mu$ senza $\nu$) normalizzano sempre in un'unica forma normale (Teorema 4.11).
• Rappresentazione di Funzioni: Il sistema fornisce un risultato di normalizzazione per le dimostrazioni di sequenti della forma $N, \dots, N \vdash N$ (dove $N$ rappresenta i numeri naturali). Tali dimostrazioni rappresentano funzioni totali uniche sui numeri naturali (Teorema 4.12).
• Gestione dei Casi di "Rimbalzo" (Bouncing): L'articolo dimostra che il framework delle variabili ordinali può catturare dimostrazioni che falliscono la standard condizione del filo progressivo ma che sono valide sotto la condizione del "filo rimbalzante". Viene fornito un esempio in cui un taglio interrompe una traccia standard, ma le variabili ordinali esplicite nella formula del taglio preservano l'argomento della discesa, rendendo la dimostrazione valida in questo sistema.
• Semantica Categoriale: L'articolo costruisce un modello categoriale dove i punti fissi minimi corrispondono ad algebre iniziali e i punti fissi massimi a coalgebre finali (Sezioni 5.2 e 5.3). Ciò conferma che la semantica della computabilità si allinea con le standard interpretazioni categoriali dei tipi induttivi e coinduttivi.
• Decidibilità: A differenza della condizione del filo rimbalzante, il criterio di validità basato sulle variabili ordinali è noto per essere decidibile [SD03a].

Significato e Rivendicazioni
L'articolo si pone come uno studio pilota che contribuisce al progetto avviato da Baelde et al. [BDKS22] di trovare criteri di validità naturali per le dimostrazioni non ben fondate che vadano oltre le standard condizioni di traccia. L'autore sostiene che il framework di Dam-Gurov-Sprenger delle variabili ordinali esplicite sia un candidato idoneo per questo scopo.

La significatività risiede in due osservazioni principali:

1. Espressività: La condizione di validità cattura dimostrazioni (specificamente quelle con comportamento "rimbalzante") che non sono riconosciute come valide dalla standard condizione del filo progressivo.
2. Significato Computazionale: Fornendo una semantica della computabilità, l'articolo dimostra che tutte le dimostrazioni valide in questo sistema rappresentano programmi computabili e ben definiti. Ciò colma il divario tra la condizione sintattica di validità e il requisito semantico di terminazione/computabilità.

L'autore nota con modestia che l'articolo non fornisce una completa dimostrazione di eliminazione del taglio per la logica (il che richiederebbe ulteriori regole di permutazione) né una prova definitiva che il sistema delle variabili ordinali sia equivalente in potenza alla condizione del filo rimbalzante. Invece, lascia aperta la questione se ogni dimostrazione valida sotto la condizione del filo rimbalzante possa essere rappresentata utilizzando le variabili ordinali come un problema aperto per la ricerca futura. Il lavoro serve a motivare l'esplorazione ulteriore delle variabili ordinali da una prospettiva Curry-Howard.