A Classical Linear $λ$-Calculus based on Contraposition

Sintesi Tecnica: Un $\lambda$-calcolo Lineare Classico basato sulla Contrapposizione

Problema
Il saggio affronta la sfida di armonizzare le simmetrie classiche della Logica Lineare (LL) con il formalismo computazionale del $\lambda$-calcolo. La Logica Lineare esibisce forti simmetrie (ad esempio, la dualità tra regole di sinistra e di destra, la negazione involutiva dove $\neg\neg A = A$), mentre le tipiche presentazioni di deduzione naturale spesso non riescono a preservare tali simmetrie pur mantenendo buone proprietà computazionali come la confluenza e la normalizzazione forte. I sistemi esistenti rientrano tipicamente in due categorie:

1. Frammenti intuizionistici: Sistemi come ILL o DILL limitano la logica a sequenti a conclusione singola, perdendo le simmetrie classiche e la capacità di modellare certi teoremi.
2. Sistemi basati su sequenti: Sistemi derivati dal calcolo dei sequenti (ad esempio, proof-nets o calcoli di processi) preservano le simmetrie ma trattano spesso i teoremi come processi paralleli piuttosto che come programmi funzionali, rendendoli meno adatti ai paradigmi di programmazione funzionale.

Nello specifico, gli autori osservano che nella logica classica, affermare una proposizione $A$ come tesi è equivalente a negarla come ipotesi. Nel contesto della Logica Lineare, ciò implica che $A \multimap B$ e $B^\perp \multimap A^\perp$ debbano condividere gli stessi teoremi. Tuttavia, i $\lambda$-calcoli standard per la logica classica (come il $\lambda\mu$ di Parigot) sono confluenti ma non simmetrici (la negazione non è involutiva), mentre i sistemi simmetrici (come quelli di Barbanera e Berardi) spesso mancano di confluenza. Il saggio cerca un sistema di deduzione naturale a conclusione singola per la MELL (Multiplicative Exponential Linear Logic) che mantenga le simmetrie classiche e goda delle standard proprietà dei linguaggi di programmazione tipizzati.

Metodologia
Gli autori propongono un nuovo assegnamento di termini per la MELL, denominato $\lambda$MELL-calculus, fondato sul paradigma "proposizioni-come-tipi". La metodologia centrale prevede:

1. Fondazione Logica: Partendo dal frammento intuizionistico della Logica Lineare Moltiplicativa (MLL), gli autori introducono una regola di modus tollens lineare. Mentre la standard eliminazione dell'implicazione lineare (modus ponens) permette di derivare $B$ da $A \multimap B$ e $A$, la nuova regola permette di derivare $A^\perp$ da $A \multimap B$ e $B^\perp$. Questa aggiunta recupera la MLL classica.
2. Operazione Innovativa: Contra-Sostituzione: Per fornire un'interpretazione computazionale della regola del modus tollens, gli autori definiscono una nuova operazione chiamata contra-sostituzione, denotata con $t\{a \backslash s\}$.
   • Intuizione: Se la standard sostituzione $t\{a := s\}$ sostituisce un'occorrenza unica della variabile $a$ in $t$ con $s$, la contra-sostituzione "afferra" l'occorrenza unica di $a$ in $t$ e "tira" da essa, efficacemente capovolgendo il termine $t$ "dentro fuori" (come un calzino) prima di sostituire $a$ con $s$.
   • Meccanismo: Questa operazione è definita per induzione strutturale sui termini lineari. Ad esempio, se $t = \langle u, a \rangle$ e $s : A \multimap B^\perp$, allora $\langle u, a \rangle\{a \backslash s\}$ risulta in $s \bullet u : B^\perp$.
3. Costruzione del Calcolo: Il calcolo include le standard costruzioni lineari (tensore, implicazione lineare, astrazione lambda) insieme alla nuova contra-applicazione ($t \blacktriangledown s$), che corrisponde all'eliminazione del modus tollens. Per la MELL, il calcolo viene esteso includendo le modalità esponenziali ($!$ e $?$) e le unità, richiedendo una definizione raffinata di linearità e una relazione di equivalenza strutturale.
4. Equivalenza Strutturale: Per garantire la confluenza in presenza di esponenziali e percorsi di riduzione complessi, gli autori definiscono un'equivalenza strutturale ($\equiv$) che agisce come un forte bisimulazione rispetto alla pre-riduzione. Questa equivalenza include assiomi per la propagazione degli eliminatori e la gestione delle unità (ad esempio, $t[\star := s] \equiv s[\star := t]$ per termini di tipo 1).

Contributi Chiave

1. Il $\lambda$MELL-Calculus: Una presentazione a lato singolo della MELL dove i teoremi sono modellati come espressioni funzionali. Introduce la costruzione di contra-applicazione e l'operazione di contra-sostituzione.
2. Correttezza e Completezza: Gli autori dimostrano che il calcolo è corretto e completo rispetto alla MELL. Nello specifico, qualsiasi sequente MELL valido può essere letto come un giudizio di tipizzazione in $\lambda$MELL selezionando qualsiasi formula come tesi e le negazioni delle altre come ipotesi.
3. Proprietà Metatestuali: Il calcolo soddisfa le proprietà standard di un linguaggio di programmazione tipizzato:
   • Riduzione del Soggetto (Subject Reduction): La riduzione preserva la tipizzazione.
   • Confluenza: La relazione di riduzione è confluenza (modulo equivalenza strutturale).
   • Normalizzazione Forte: Ogni sequenza di riduzione termina.
4. Codifica di Sistemi Classici: Il saggio dimostra che diversi noti assegnamenti di termini per la logica classica possono essere codificati in $\lambda$MELL, inclusi:
   • Il $\lambda\mu$-calcolo di Parigot (tramite sia le traduzioni T che Q).
   • Il $\lambda\mu\tilde{\mu}$-calcolo di Curien e Herbelin.
   • Il $\mu$DCLL di Hasegawa.

Risultati
I risultati primari sono le prove delle proprietà metatestuali. Gli autori stabiliscono la normalizzazione forte utilizzando la tecnica dei candidati di riducibilità, definendo insiemi di termini associati a ciascun tipo. La confluenza è provata tramite il Lemma di Newman stabilendo la confluenza locale, che si basa sull'equivalenza strutturale che agisce come una forte bisimulazione per la pre-riduzione. Il saggio fornisce anche prove costruttive per la completezza del calcolo, mostrando come recuperare i termini dalle derivazioni MLL prive di tagli (cut-free).

Significatività
Il saggio rivendica significatività offrendo un'interpretazione "funzionale" della logica lineare classica che preserva le sue simmetrie intrinseche senza ricorrere a calcoli di processi o a deduzioni naturali a conclusione multipla. Introducendo la contra-sostituzione, gli autori forniscono un meccanismo per gestire computazionalmente il principio classico di contrapposizione all'interno di un framework a conclusione singola. Questo lavoro suggerisce una base per linguaggi di programmazione funzionale lineare e assistenti alla dimostrazione che possano supportare nativamente il ragionamento classico e la sensibilità alle risorse. Gli autori notano che estendere l'approccio ai connettivi additivi è non banale a causa della dipendenza dalla linearità per la contra-sostituzione, ma il sistema attuale gestisce con successo i frammenti moltiplicativi ed esponenziali. Questo lavoro colma il divario tra la simmetria del calcolo dei sequenti e la natura funzionale dei $\lambda$-calcoli.