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

Technische Samenvatting: Spellen, Mobile Processen en Functies

Probleemstelling
Het artikel adresseert het ontbreken van een strakke, formele correspondentie tussen twee prominente semantische kaders voor hogere-orde talen: Operationele Spelsemantic (OGS) en de $\pi$-calculus (specifiek de Interne $\pi$-calculus, $I\pi$). Hoewel beide modellen worden gebruikt om het gedrag van $\lambda$-calculus-termen te karakteriseren, verschillen ze aanzienlijk in hun constructie. OGS biedt intensionele modellen waarbij programmadenotaties composiet worden afgeleid uit configuraties die interacties met een omgeving voorstellen, vaak met nadruk op eigenschappen zoals alternatie en goed-gehaakte structuur. Daarentegen modelleert de $\pi$-calculus functies als processen via Milner's coderingen, waarbij gebruik wordt gemaakt van algebraïsche structuren en procesequivalenties zoals bisimilariteit. De auteurs beogen een precieze operationele correspondentie tussen deze modellen te vestigen voor de ongetypeerde call-by-value $\lambda$-calculus ($\Lambda_V$) en call-by-name, en te demonstreren dat ze dezelfde gedragsvergelijkingen induceren en dat technieken uit het ene model naar het andere kunnen worden overgebracht.

Methodologie
De auteurs maken gebruik van een vergelijkende analyse van de operationele semantiek van $\Lambda_V$ onder drie verschillende OGS-varianten en twee $I\pi$-varianten:

1. OGS-varianten:
   • Alternating OGS (A-OGS): Dwingt strikte alternatie af tussen het programma (Speler) en de omgeving (Opponent).
   • Concurrent OGS (C-OGS): Staat toe dat meerdere termen parallel draaien binnen een configuratie.
   • Well-Bracketed OGS (WB-OGS): Dwingt een stack-discipline af op continuaties, waarbij de Opponent wordt beperkt tot antwoorden in een last-in-first-out volgorde.
2. $I\pi$-varianten:
   • Standaard $I\pi$ LTS: Het standaard gelabelde transitiesysteem voor de Interne $\pi$-calculus.
   • Output-Prioritised $I\pi$ LTS (opLTS): Een beperkt LTS waarbij input-acties alleen zichtbaar zijn als er geen output of interne actie op wacht, waardoor sequentiële beperkingen worden afgedwongen.

De kernmethodologie omvat het definiëren van een mapping ($\mathcal{V}$) van OGS-configuraties (inclusief omgevingen en draaiende termen) naar $I\pi$-processen. Deze mapping breidt Milner's codering van $\lambda$-termen uit. De auteurs bewijzen vervolgens operationele correspondentiestellingen die aantonen dat transities in OGS overeenkomen met transities in $I\pi$ (en omgekeerd) onder specifieke voorwaarden. Cruciaal maken ze gebruik van "up-to"-technieken (specifiek up-to context en up-to composition) die uit $I\pi$ zijn overgenomen om bisimilariteitsbewijzen in OGS te vereenvoudigen. Ze introduceren ook een tensorproduct voor OGS-configuraties om de verweving van sporen te modelleren, analoog aan parallelle compositie in procescalculi.

Belangrijkste Bijdragen

1. Operationele Correspondentie: Het artikel vestigt strakke operationele correspondenties tussen:

   • A-OGS en $I\pi$ onder de output-prioritised LTS (opLTS).
   • C-OGS en $I\pi$ onder de standaard LTS.
     Deze correspondenties gelden voor zowel sterke als zwakke transities, waarbij gebruik wordt gemaakt van de expansierelatie ($\lesssim$) om interne reducties in rekening te brengen.

2. Samenvallen van Equivalentie: De auteurs bewijzen dat de gedragsvergelijkingen die door al deze modellen op $\lambda$-termen worden geïnduceerd, samenvallen. Specifiek:

   • Trace-equivalentie en bisimilariteit in A-OGS, C-OGS en $I\pi$ (zowel standaard als opLTS) definiëren allemaal dezelfde relatie op $\Lambda_V$-termen.
   • Deze geïnduceerde equivalentie wordt geïdentificeerd als Lassen's eager normal-form bisimilariteit (vaak gevisualiseerd als Lassen's bomen).
   • Voor volledige sporen (sporen die beëindigde interacties beschrijven) vallen de semantiek van Alternating, Concurrent en Well-Bracketed OGS eveneens samen.

3. Overdracht van Technieken:

   • Up-to Composition: De auteurs importeren de "up-to context" en "expansion" technieken uit $I\pi$ naar OGS. Ze definiëren een nieuwe techniek genaamd "up-to composition" voor OGS, die bisimilariteitsbewijzen toestaat om een complexe configuratie op te splitsen in elementaire componenten (singleton-configuraties) en onafhankelijk over hen te redeneren.
   • Congruentie en Compositie: Door gebruik te maken van de correspondentie met $I\pi, leidt het artikel congruentie-eigenschappen af voor OGS (bijvoorbeeld: als$M \sim N$, dan $C[M] \sim C[N]$) en definieert het een tensorproduct voor configuraties dat verwevingen van sporen berekent.

4. Volledige Abstractie voor Store: Het onderzoek naar volledige sporen in de Well-Bracketed OGS wordt gekoppeld aan contextuele equivalentie voor $\lambda$-calculi met mutabele opslag. Het artikel toont aan dat de codering van $\lambda$-termen naar $I\pi$ een resultaat van volledige abstractie oplevert met betrekking tot contexten geschreven in een $\lambda$-calculus uitgebreid met een store.

5. Call-by-Name Uitbreiding: Het artikel schetst een vergelijkbare correspondentie voor de ongetypeerde call-by-name $\lambda$-calculus, en toont aan dat de geïnduceerde equivalentie samenvalt met Lévy-Longo Bomen.

Resultaten

• Stelling 6.7 & 7.3: Vestigen de operationele correspondentie tussen OGS-configuraties en $I\pi$-processen onder de respectievelijke LTS's.
• Corollarium 6.12 & 7.7: Demonstreren dat trace-equivalentie en bisimilariteit in A-OGS, C-OGS en $I\pi$ identiek zijn voor $\lambda$-termen.
• Stelling 8.1: Bewijst direct dat C-OGS-bisimilariteit samenvalt met Lassen's eager normal-form bisimilariteit met gebruikmaking van de "up-to composition" techniek.
• Stelling 12.2: Bewijst dat volledige-spore-equivalentie identiek is tussen WB-OGS, A-OGS en C-OGS.
• Lemma 7.16 & Stelling 7.17: Bewijzen de geldigheid van "bisimilariteit up-to reductie en compositie" voor C-OGS, overgenomen uit $I\pi$.

Beteekenis
Het artikel stelt dat de primaire betekenis ligt in het vestigen van een "strakke en precieze correspondentie" tussen OGS en de $\pi$-calculus. Deze verbinding maakt de overdracht van resultaten en technieken tussen de twee modellen mogelijk. Specifiek:

• Het stelt OGS in staat te profiteren van de rijke algebraïsche structuur en krachtige bewijstechnieken (zoals up-to technieken) van de $\pi$-calculus, die vaak moeilijk direct binnen het speltheoretische kader te ontwikkelen zijn.
• Het stelt de $\pi$-calculus in staat te profiteren van de nabijheid van OGS aan de brontaal en zijn flexibiliteit bij het modelleren van specifieke computationele effecten (zoals controle-operatoren of store).
• Het biedt een verenigd beeld van $\lambda$-calculus semantiek, en toont aan dat de "Semantic Cube"-voorwaarden (alternatie, goed-gehaakte structuur) in OGS en de sequentiële beperkingen in $I\pi$ (via opLTS) twee kanten van dezelfde medaille zijn, die beide dezelfde onderliggende gedragsvergelijking karakteriseren (Lassen's bomen voor call-by-value).

De auteurs merken op dat hoewel analogieën tussen spelsemantic en procescalculi eerder zijn onderzocht (bijvoorbeeld het vertalen van strategieën naar processen), dit werk zich onderscheidt door de directe vergelijking van de interpretatie van functies en de systematische overdracht van bewijstechnieken om nieuwe resultaten voor OGS af te leiden.