Intuitionistic BV (Extended version)

Riassunto Tecnico: Intuitionistic BV (IBV)

1. Il Problema (Problem)

Il punto di partenza è la logica BV, un'estensione conservativa della logica lineare moltiplicativa con mix (MLLmix) che introduce un connettivo non commutativo e auto-duale ($\rhd$), chiamato seq. La logica BV è fondamentale per la formalizzazione di algebra dei processi, tipi per il lambda calcolo lineare e computazione quantistica.

Tuttavia, esiste un ostacolo teorico nel definire una versione intuizionistica di BV. In BV classico, l'unità $I$ è auto-duale e condivisa da tutti i connettivi ($\otimes, \wp, \rhd$). Nelle logiche lineari, il passaggio da una versione classica a una intuizionistica avviene solitamente tramite la polarizzazione delle formule. Ma l'auto-dualità di $I$ e di $\rhd$ impedisce una polarizzazione standard, poiché renderebbe i connettivi collassare (rendendo $\otimes$ e $\rhd$ logicamente equivalenti).

2. Metodologia (Methodology)

Gli autori risolvono il problema introducendo una nuova struttura in cui l'unità $I$ non è più una "unità piena", ma una "mezza unità". In IBV, non si ha più l'equivalenza $A \rhd I \equiv A \equiv I \rhd A$, ma solo le implicazioni $A \multimap (A \rhd I)$ e $A \multimap (I \rhd A)$.

Per analizzare questa logica, il lavoro adotta due approcci formali:

• Deep Inference (Inferenza Profonda): Viene sviluppato un sistema di derivazione basato sul calculus of structures. A differenza dei calcoli di Gentzen (sequent calculus), l'inferenza profonda permette di applicare regole direttamente all'interno delle formule, gestendo la non-commutatività attraverso la distinzione tra contesti positivi e negativi.
• Sequent Calculus (Calcolo dei Sequenti): Per la variante non associativa della logica (INML), viene utilizzato un calcolo dei sequenti a conclusione singola per facilitare la dimostrazione della taglio-eliminazione.

3. Contributi Chiave (Key Contributions)

• Definizione di IBV: Introduzione formale della logica BV intuizionistica, estendendo l'IMLL (Intuitionistic Multiplicative Linear Logic) con il connettivo $\rhd$ che valida la legge di distribuzione: $((A \rhd B) \otimes (C \rhd D)) \multimap ((A \otimes C) \rhd (B \otimes D))$.
• Sistema di Inferenza Profonda per IBV: Presentazione di un sistema completo di regole (regole di switch, ref, sq, q, ecc.) che distingue tra derivazioni positive e negative.
• Sistema SIBV: Introduzione di una versione simmetrica (SIBV) che include le regole "up" (per la direzione opposta rispetto alle regole "down"), dimostrando che IBV e SIBV sono equivalenti.
• Logica INML: Introduzione di una variante in cui il connettivo $\rhd$ non è associativo, fornendo un calcolo dei sequenti privo di tagli (cut-free).

4. Risultati Principali (Results)

• Taglio-Eliminazione (Cut Elimination): Gli autori dimostrano che la regola del taglio è admissibile in IBV attraverso l'uso di un "Splitting Lemma" (Lemma di scomposizione), un risultato tecnico complesso che permette di scomporre le formule in componenti più semplici durante la riduzione del taglio.
• Conservatività:
  • IBV è un'estensione conservativa di IMLL (ogni formula di IMLL dimostrabile in IBV è dimostrabile in IMLL).
  • La versione priva di unità di IBV ($IBV^-$) è un'estensione conservativa della versione priva di unità di BV ($BV^-$).
• Equivalenza tra Sistemi: Viene dimostrato che la logica INML (non associativa) può essere trasformata in IBV aggiungendo regole di "taglio associativo" (a-cut), stabilendo un legame profondo tra le due strutture.

5. Significato e Implicazioni (Significance)

Il lavoro colma una lacuna importante nella teoria della logica lineare, fornendo una base formale per trattare la sequenzialità in contesti intuizionistici.

L'importanza risiede nella capacità di modellare l'ordine temporale o l'ordine di esecuzione delle istruzioni senza perdere le proprietà costruttive tipiche della logica intuizionistica. Questo ha potenziali applicazioni nel design di linguaggi di programmazione imperativi dove la sequenzialità delle operazioni deve essere garantita dal sistema di tipi (typing disciplines), offrendo un framework logico per la gestione della causalità e dell'ordine degli eventi.