Proof Nets for PiL (Full Version)

Sintesi Tecnica: Reti di Prova per PiL

Enunciato del Problema
Il documento affronta la sfida di fornire una rappresentazione canonica, basata su grafi, per le dimostrazioni in PiL, un sistema logico che estende la logica lineare moltiplicativa additiva del primo ordine (MALL1). PiL è stato introdotto per offrire una codifica superficiale dei processi nel calcolo $\pi$, specificamente per dimostrare la completezza della programmazione coreografica rispetto ai processi privi di race condition e privi di deadlock.

La difficoltà principale risiede negli operatori unici di PiL:

1. L'operatore $\blacktriangleleft$: Un connettivo non commutativo, non associativo e autoduale che modella la composizione sequenziale.
2. Quantificatori Nominali ($\new$ e $\ya$): Quantificatori che modellano il vincolo di nomi e la freschezza, richiedendo una rigorosa gestione dell'uso delle variabili per garantire che i nomi siano condivisi da al più una coppia di quantificatori duali.

Le esistenti formalizzazioni delle reti di prova per MALL (come le reti di Girard o le reti di conflitto) faticano a gestire la combinazione di additivi, quantificatori e connettivi non commutativi/non associativi. Inoltre, le derivazioni standard del calcolo dei sequenti soffrono di non-canonicità a causa di permutazioni indipendenti delle regole, il che oscura la semantica sottostante degli alberi di esecuzione dei processi. Il documento mira a definire reti di prova che collassino tali permutazioni in un singolo oggetto sintattico, gestendo al contempo i vincoli specifici dei quantificatori nominali e dell'operatore $\blacktriangleleft$.

Metodologia
Gli autori adottano le reti di conflitto come quadro fondazionale, estendendole al contesto del primo ordine di PiL. La metodologia coinvolge tre componenti principali:

1. Definizione della Struttura (Pre-strutture e Reti di Prova):

   • Collegamenti e Dualizzatori: Gli autori definiscono i collegamenti (connessioni assiomatiche tra sotto-sequenti) e li associano ai dualizzatori (sostituzioni). I dualizzatori mappano le variabili in un collegamento su testimoni esistenziali o nominali, imponendo la dualità e gestendo l'unificazione richiesta dai quantificatori.
   • Coco-alberi: La struttura sottostante è un "albero concordia-conflitto" (coco-albero) dove le foglie sono collegamenti e i nodi interni sono etichettati con relazioni di concordia ($\smile$) o conflitto ($\#$).
   • Coalescenza: Viene definita una procedura di riscrittura (coalescenza) per ridurre una struttura di prova a una forma banale (una singola foglia). Questo processo imita la costruzione dal basso verso l'alto di una derivazione dei sequenti. Una rete di prova è definita come una struttura di prova che ammette un percorso di coalescenza verso una pre-struttura banale.

2. Correttezza e Sequenzializzazione:

   • Viene stabilito un criterio di correttezza in tempo polinomiale: una struttura è una rete di prova valida se e solo se è coalescente.
   • Viene fornita una procedura di sequenzializzazione, che traduce una rete di prova valida in una derivazione del calcolo dei sequenti in PiL. Ciò dimostra la completezza della formalizzazione delle reti rispetto alla logica.
   • Un algoritmo di traduzione delle prove traduce le derivazioni di PiL in reti di conflitto, stabilendo la correttezza.

3. Reti a Fette e Appiattimento:

   • Per ottenere una forma più canonica, gli autori introducono le reti a fette, una sottoclasse di reti di conflitto in cui il coco-albero sottostante è "piatto" (contenente al più un nodo $\#$ alla radice).
   • Viene definita una procedura di appiattimento come una regola di riscrittura che sposta i nodi di concordia sopra i nodi di conflitto. Gli autori dimostrano che l'appiattimento è fortemente normalizzante, confluenente e preserva la coalescenza. Ciò permette di trasformare qualsiasi rete di conflitto in una singola rete a fette canonica.

Contributi Chiave

• Definizione di Reti di Conflitto per PiL: Il documento definisce la prima formalizzazione di reti di prova per una logica che combina additivi, quantificatori del primo ordine e il connettivo non commutativo/non associativo $\blacktriangleleft$.
• Correttezza in Tempo Polinomiale: Fornisce un criterio di correttezza in tempo polinomiale (specificamente $O(n^5)$) basato sulla coalescenza di coco-alberi con mappe di testimoni.
• Sequenzializzazione e Traduzione: Stabilisce una traduzione bidirezionale tra le derivazioni dei sequenti di PiL e le reti di prova, dimostrando che le reti sono sia corrette che complete.
• Rappresentazione Canonica (Reti a Fette): Introduce le reti a fette e la procedura di appiattimento, dimostrando che ogni rete di conflitto si riduce a una singola rete a fette.
• Risultati di Canonicità: Il documento dimostra due livelli distinti di canonicità:
  • Canonicità Locale: Le reti di conflitto forniscono una rappresentazione canonica delle derivazioni modulo permutazioni di regole locali (scambi di regole indipendenti).
  • Canonicità Forte: Le reti a fette forniscono una rappresentazione canonica modulo sia permutazioni di regole locali che non locali.

Risultati

• Teorema 1: Un sequente $\Gamma$ è dimostrabile in PiL se e solo se esiste una rete di conflitto per $\Gamma$.
• Teorema 2: L'appiattimento preserva la coalescenza, garantendo che la trasformazione dalle reti di conflitto alle reti a fette mantenga la validità.
• Teorema 3: Un sequente $\Gamma$ è dimostrabile in PiL se e solo se esiste una rete a fette per $\Gamma$.
• Teorema 4:
  • Due derivazioni $D$ e $D'$ sono localmente equivalenti ($D \approx D'$) se e solo se le loro reti di conflitto associate sono isomorfe.
  • Due derivazioni $D$ e $D'$ sono fortemente equivalenti ($D \simeq D'$) se e solo se le loro reti a fette associate sono isomorfe.

Significato e Affermazioni
Il documento afferma che le reti di prova per PiL forniscono una rappresentazione canonica delle derivazioni del calcolo dei sequenti, collassando efficacemente classi di derivazioni che differiscono solo per permutazioni indipendenti delle regole. Ciò è significativo per la semantica dei calcoli dei processi perché:

• Si allinea con la semantica degli alberi di esecuzione nel calcolo $\pi$, dove l'ordine delle azioni indipendenti non dovrebbe influenzare il significato del processo.
• Distingue tra canonicità locale (rilevante dove l'ordine dei rami è importante) e canonicità forte (rilevante per equivalenze come la bisimulazione dove l'ordine dei rami è irrilevante).
• Offre una base per lo sviluppo di nuovi strumenti per studiare la semantica dei sistemi concorrenti e delle coreografie, trattando le reti di prova come rappresentanti degli alberi di esecuzione, ignorando gli intrecci irrilevanti pur preservando fenomeni osservabili come le race condition.

Gli autori dichiarano esplicitamente di non studiare l'eliminazione del taglio in questo lavoro, poiché il loro focus è sulle prove senza taglio che rappresentano alberi di calcolo. Notano che l'eliminazione del taglio per PiL comporta una gestione non banale dei quantificatori nominali e degli archivi, lasciata per lavori futuri. Allo stesso modo, sebbene suggeriscano che il loro quadro potrebbe essere esteso alla MALL generale del primo ordine, non affermano di aver risolto il caso generale in questo documento.