Technische Samenvatting: Benaderingstheorie voor Distant Bang Calculus

1. Probleemstelling

Benaderingstheorie dient als een centrale benadering voor de semantiek van $\lambda$-calculus, waarbij het gedrag van programma's wordt gekarakteriseerd via eindige of oneindige middelen. Hoewel dit goed gevestigd is voor Call-by-Name (CbN) via Böhm-bomen en Taylor-expansie, heeft de Call-by-Value (CbV) setting historisch gezien achtergebleven. Recente ontwikkelingen in CbV Böhm-bomen (bijv. Kerinec [29, 28]) toonden aan dat de standaard CbV-reductie (Plotkin's $\beta_v$) "te zwak" is, wat vaak leidt tot het vastlopen van de reductie wanneer argumenten in normale vorm zijn maar geen waarden. Dit noodzaakte alternatieve kaders, zoals de $\lambda\sigma_v$-calculus met permutatieregels ($\sigma$-regels) of afstand-gebaseerde calculi (dCbV).

De Bang-calculus (Bang) werd voorgesteld als een verenigend kader dat zowel CbN als CbV omvat via Lineaire Logica-translaties. Echter, de standaard Bang-calculus erft het CbV-probleem van slecht gevormde redexen die de evaluatie blokkeren. Hoewel $\sigma$-regels dit theoretisch zouden kunnen oplossen, falen zij in het behouden van convergentie (confluence) in de Bang-setting. De distant Bang-calculus (dBang) [15] biedt een oplossing door gebruik te maken van expliciete substituties en "distante" reducties, wat convergentie garandeert zonder $\sigma$-regels.

Ondanks de vooruitgang in dBang met betrekking tot convergentie en betekenisvolheid [30, 9, 15], bleef een uitgebreide benaderingstheorie voor dBang onderontwikkeld. Specifiek ontbrak er een verenigd kader dat Böhm-achtige benaderingsbomen en Taylor-expansies voor dBang definieert, noch een bewijs van de Commutatie-stelling die hen relateert. Bovendien, hoewel recente generieke benaderingen (Mazza & Dufour [19]) bestaan, missen zij een direct begrip van betekenisvolheid en relateren zij niet duidelijk terug naar de specifieke notions van oplosbaarheid/onderzoekbaarheid (solvability/scrutability) van CbN en CbV.

2. Methodologie

De auteurs ontwikkelen een verenigde benaderingstheorie voor dBang door twee centrale paradigma's te integreren: Taylor-expansie (resource-sensitieve semantiek) en Benaderingsbomen (Böhm-traditie).

2.1 De Resource Calculus ($\delta$Bang)

De auteurs definiëren een resource calculus $\delta$Bang als het doelwit voor Taylor-expansie. Deze calculus vervangt exponenten ($!M$) door eindige multisets (bags) van resource-termen.

• Benaderingsrelatie ($\triangleleft!$): Een multilineaire relatie wordt gedefinieerd tussen resource-termen en dBang-termen.
• Reductie: De reductie-relatie $\Rightarrow_\delta$ is niet-deterministisch vanwege permutaties van bags, maar is sterk normaliserend vanwege lineariteit.
• Taylor Normale Vorm (TNF): Gedefinieerd als de verzameling volledige normale vormen van alle resource-approximanten van een term.

2.2 Benaderingsbomen

De auteurs definiëren Benaderingsbomen voor dBang door de calculus uit te breiden met een symbool $\bot$ dat ongedefinieerde berekening representeert.

• Approximanten: Een grammatica van termen die $\bot$ bevat, wordt gedefinieerd, waarbij de termen potentiële ongedefinieerde subtermen representeren.
• Ideale Volledigheid: De verzameling approximanten voor een term $M$, aangeduid als $A(M)$, vormt een ideaal onder een contextuele preordening $\sqsubseteq$. De benaderingsboom $AT!(M)$ is het supremum van dit ideaal, wat de limiet van het gedrag van de term representeert.
• Onderscheid: In tegenstelling tot klassieke CbN Böhm-bomen, die approximanten beperken tot head normal forms, hanteren de auteurs een bredere definitie (vergelijkbaar met Lévy-Longo bomen in CbN en CbV Böhm-bomen in CbV) om de specifieke semantiek en embeddings van dBang te accommoderen.

2.3 Translaties

Om het kader te valideren, maken de auteurs gebruik van bestaande translaties van distant Call-by-Name (dCbN) en distant Call-by-Value (dCbV) naar dBang. Zij bewijzen dat deze translaties reductiestappen en betekenisvolheid behouden, waardoor resultaten afgeleid uit dBang teruggeprojecteerd kunnen worden op dCbN en dCbV.

3. Belangrijkste Bijdragen en Resultaten

3.1 Simulatie en Commutatie

Het artikel stelt een rigoureuze link vast tussen de operationele reductie van dBang en zijn benaderingen:

• Simulatie-stelling (Theorem 21): De Taylor-expansie van een dBang-term simuleert zijn reductie. Specifiek, als $M \to! N$, dan reduceert de verzameling Taylor-expansies $T(M)$ naar $T(N)$ via parallelle resource-reductie.
• Commutatie-stelling (Theorem 46): Dit is de centrale resultaat. Het stelt dat de Taylor-expansie van de benaderingsboom van een term gelijk is aan de Taylor-normale vorm van de term zelf:
  $$T(AT!(M)) = TNF(M)$$
  Dit bevestigt dat de oneindige semantiek (bomen) en de resource-sensitieve semantiek (Taylor-expansie) consistent zijn binnen het dBang-kader.

3.2 Herstel van CbN en CbV gevallen

Door dCbN en dCbV naar dBang te translateren, herstellen de auteurs de benaderingstheorieën voor deze specifieke calculi:

• Theorem 59: De benaderingsboom van een getranslateerde term in dBang komt exact overeen met de translatie van de benaderingsboom in de bron-calculus.
• Theorem 60: De Commutatie-stelling geldt voor zowel dCbN als dCbV als een direct gevolg van het dBang-resultaat.

3.3 Betekenisvolheid en Taylor-expansie

Het artikel onderzoekt de relatie tussen betekenisvolheid (het vermogen van een term om tot een waarde te reduceren onder een test-context) en de niet-leegheid van de Taylor-normale vorm.

• Theorem 61: Als een dBang-term betekenisvol is, is zijn Taylor-normale vorm niet-leeg ($TNF(M) \neq \emptyset$).
• Het Omgekeerde: Het omgekeerde geldt niet voor de algemene dBang-calculus; er bestaan betekenisloze termen met niet-lege Taylor-normale vormen (bijv. termen met "clashes" zoals $xx$).
• Fragmenten: Echter, voor de specifieke fragmenten die overeenkomen met dCbN ($dBang_N$) en dCbV ($dBang_V$), wordt de equivalentie hersteld:
  • Corollary 68 (dCbN): $M$ is betekenisvol iff $TNF(M) \neq \emptyset$.
  • Corollary 73 (dCbV): $M$ is betekenisvol iff $TNF(M) \neq \emptyset$.

4. Betekenis en Claims

Het artikel claimt een verenigend kader te bieden voor benaderingstheorie dat zowel oneindige als resource-sensitieve semantiek voor CbN en CbV binnen één systeem (dBang) vangt.

• Unificatie: Het demonstreert dat de afzonderlijke ontwikkelingen voor CbN en CbV kunnen worden ondergebracht onder de dBang-calculus, wat de historische behoefte aan aparte semantische theorieën oplost.
• Robuustheid: Door de distant variant (dBang) te gebruiken, vermijden de auteurs de convergentie-problemen geassocieerd met $\sigma$-regels in de standaard Bang-calculus, wat een schoner kader biedt voor benaderingstheorie.
• Overbrugging van Semantiek: De Commutatie-stelling vestigt een diepe brug tussen de "vorm-gebaseerde" oneindige semantiek (Benaderingsbomen) en de "resource-gebaseerde" differentiële semantiek (Taylor-expansie) in een verenigde setting.
• Karakterisering van Betekenisvolheid: Het werk biedt een syntactische karakterisering van betekenisvolheid voor dCbN en dCbV via niet-lege Taylor-normale vormen, waarmee bekende resultaten van standaard CbN/CbV worden uitgebreid naar hun distant-varianten.

De auteurs merken bescheiden op dat hoewel de equivalentie tussen betekenisvolheid en niet-lege Taylor-normale vormen geldt voor de getranslateerde fragmenten, het een open vraag blijft of een groter, generiek fragment van dBang (voorbij de translaties) op een vergelijkbare wijze kan worden gekarakteriseerd. Zij suggereren ook toekomstig werk voor het uitbreiden van deze notions naar proof structures, voortbouwend op het werk van Mazza en Dufour.