Games, mobile processes, and functionss -- alternating, concurrent, and well-bracketed semantics

Riepilogo Tecnico: Giochi, Processi Mobili e Funzioni

Enunciato del Problema
Il lavoro affronta la mancanza di una stretta corrispondenza formale tra due quadri semantici prominenti per i linguaggi di ordine superiore: la Semantica Operativa dei Giochi (OGS) e il $\pi$-calcolo (in particolare il $\pi$-calcolo Interno, $I\pi$). Sebbene entrambi i modelli siano utilizzati per caratterizzare il comportamento dei termini del $\lambda$-calcolo, differiscono significativamente nella loro costruzione. L'OGS fornisce modelli intensionali in cui le denotazioni dei programmi sono derivate in modo composizionale da configurazioni che rappresentano interazioni con un ambiente, enfatizzando spesso proprietà come l'alternanza e la corretta parentesi (well-bracketing). Al contrario, il $\pi$-calcolo modella le funzioni come processi tramite le codifiche di Milner, sfruttando strutture algebriche e equivalenze di processi come la bisimulazione. Gli autori mirano a stabilire una precisa corrispondenza operativa tra questi modelli per il $\lambda$-calcolo non tipato a chiamata per valore ($\Lambda_V$) e a chiamata per nome, dimostrando che inducono le stesse equivalenze comportamentali e che le tecniche di uno possono essere trasferite all'altro.

Metodologia
Gli autori impiegano un'analisi comparativa della semantica operativa di $\Lambda_V$ sotto tre varianti distinte di OGS e due varianti di $I\pi$:

1. Varianti OGS:
   • OGS Alternante (A-OGS): Impone un'alternanza rigorosa tra il programma (Giocatore) e l'ambiente (Avversario).
   • OGS Concorrente (C-OGS): Consente a più termini di essere eseguiti in parallelo all'interno di una configurazione.
   • OGS a Corretta Parentesi (WB-OGS): Impone una disciplina a pila sulle continuazioni, limitando l'Avversario a rispondere in ordine ultimo-in-primo-uscito (LIFO).
2. Varianti $I\pi$:
   • LTS Standard $I\pi$: Il sistema di transizioni etichettate standard per il $\pi$-calcolo Interno.
   • LTS $I\pi$ a Priorità di Output (opLTS): Un LTS vincolato in cui le azioni di input sono visibili solo se non sono in attesa azioni di output o interne, imponendo vincoli di sequenzialità.

La metodologia centrale consiste nel definire una mappatura ($\mathcal{V}$) dalle configurazioni OGS (inclusi ambienti e termini in esecuzione) ai processi $I\pi$. Questa mappatura estende la codifica dei termini $\lambda$ di Milner. Gli autori dimostrano quindi teoremi di corrispondenza operativa che mostrano come le transizioni in OGS corrispondano alle transizioni in $I\pi$ (e viceversa) sotto condizioni specifiche. Crucialmente, essi utilizzano tecniche "up-to" (in particolare up-to context e up-to composition) importate da $I\pi$ per semplificare le dimostrazioni di bisimulazione in OGS. Introducono inoltre un prodotto tensoriale per le configurazioni OGS per modellare l'intercalamento delle tracce, analogo alla composizione parallela nei calcoli di processo.

Contributi Chiave

1. Corrispondenza Operativa: Il lavoro stabilisce strette corrispondenze operative tra:

   • A-OGS e $I\pi$ sotto l'LTS a priorità di output (opLTS).
   • C-OGS e $I\pi$ sotto l'LTS standard.
     Queste corrispondenze valgono sia per le transizioni forti che per quelle deboli, utilizzando la relazione di espansione ($\lesssim$) per tenere conto delle riduzioni interne.

2. Coincidenza delle Equivalenze: Gli autori dimostrano che le equivalenze comportamentali indotte sui termini $\lambda$ da tutti questi modelli coincidono. Nello specifico:

   • L'equivalenza di traccia e la bisimulazione in A-OGS, C-OGS e $I\pi$ (sia standard che opLTS) definiscono tutte la stessa relazione sui termini $\Lambda_V$.
   • Questa equivalenza indotta è identificata come bisimulazione eager normal-form di Lassen (spesso visualizzata come alberi di Lassen).
   • Per le tracce complete (tracce che descrivono interazioni terminanti), la semantica di OGS Alternante, Concorrente e a Corretta Parentesi coincide anch'essa.

3. Trasferimento di Tecniche:

   • Up-to Composition: Gli autori importano le tecniche "up-to context" e "expansion" da $I\pi$ verso OGS. Definiscono una tecnica innovativa chiamata "up-to composition" per OGS, che permette alle dimostrazioni di bisimulazione di dividere una configurazione complessa in componenti elementari (configurazioni singleton) e ragionare su di esse indipendentemente.
   • Congruenza e Composizionalità: Sfruttando la corrispondenza con $I\pi$, il lavoro deriva proprietà di congruenza per OGS (ad esempio, se $M \sim N$, allora $C[M] \sim C[N]$) e definisce un prodotto tensoriale per le configurazioni che calcola gli intercalamenti delle tracce.

4. Astrattezza Completa per lo Store: Lo studio delle tracce complete nell'OGS a Corretta Parentesi è collegato all'equivalenza contestuale per i $\lambda$-calcoli con store mutabile. Il lavoro dimostra che la codifica dei termini $\lambda$ in $I\pi$ produce un risultato di astrattezza completa rispetto ai contesti scritti in un $\lambda$-calcolo esteso con uno store.

5. Estensione a Chiamata per Nome: Il lavoro abbozza una corrispondenza simile per il $\lambda$-calcolo non tipato a chiamata per nome, dimostrando che l'equivalenza indotta coincide con gli Alberi di Lévy-Longo.

Risultati

• Teoremi 6.7 e 7.3: Stabiliscono la corrispondenza operativa tra configurazioni OGS e processi $I\pi$ sotto i rispettivi LTS.
• Corollari 6.12 e 7.7: Dimostrano che l'equivalenza di traccia e la bisimulazione in A-OGS, C-OGS e $I\pi$ sono identiche per i termini $\lambda$.
• Teorema 8.1: Dimostra direttamente che la bisimulazione C-OGS coincide con la bisimulazione eager normal-form di Lassen utilizzando la tecnica "up-to composition".
• Teorema 12.2: Dimostra che l'equivalenza delle tracce complete è identica tra WB-OGS, A-OGS e C-OGS.
• Lemma 7.16 e Teorema 7.17: Dimostrano la correttezza della "bisimulazione up-to riduzione e composizione" per C-OGS, importata da $I\pi$.

Significato
Il lavoro afferma che il suo significato primario risiede nel stabilire una "corrispondenza stretta e precisa" tra OGS e il $\pi$-calcolo. Questa connessione permette il trasferimento di risultati e tecniche tra i due modelli. Nello specifico:

• Permette all'OGS di beneficiare della ricca struttura algebrica e delle potenti tecniche dimostrative (come le tecniche up-to) del $\pi$-calcolo, che sono spesso difficili da sviluppare direttamente all'interno del quadro teorico dei giochi.
• Permette al $\pi$-calcolo di beneficiare della vicinanza dell'OGS al linguaggio sorgente e della sua flessibilità nel modellare specifici effetti computazionali (come gli operatori di controllo o lo store).
• Fornisce una visione unificata della semantica del $\lambda$-calcolo, mostrando che le condizioni del "Cubo Semantico" (alternanza, corretta parentesi) nell'OGS e i vincoli di sequenzialità nell'$I\pi$ (tramite opLTS) sono due facce della stessa medaglia, caratterizzando entrambe la stessa equivalenza comportamentale sottostante (gli alberi di Lassen per la chiamata per valore).

Gli autori notano che, sebbene le analogie tra la semantica dei giochi e i calcoli di processo siano state esplorate in precedenza (ad esempio, traducendo strategie in processi), questo lavoro si distingue per il suo confronto diretto dell'interpretazione delle funzioni e per il suo trasferimento sistematico di tecniche dimostrative per derivare nuovi risultati per l'OGS.