How to play the Accordion: Uniformity and the (non-)conservativity of the linear approximation of the λ-calculus (extended version)

Technische Samenvatting: "How to Play the Accordion: Uniformity and the (Non-)Conservativity of the Linear Approximation of the $\lambda$-Calculus"

Probleemstelling
Het artikel onderzoekt de conservativiteit van de lineaire benadering van de $\lambda$-calculus, specifiek binnen het kader van de differentiële $\lambda$-calculus en de resource calculus van Ehrhard en Regnier. Hoewel het algemeen bekend is dat de Taylor-expansie $T(M)$ van een $\lambda$-term $M$ de simulatie van $\beta$-reductie mogelijk maakt (d.w.z. als $M \to_\beta N$, dan $T(M) \twoheadrightarrow_r T(N)$), blijft de omgekeerde vraag open: Is elke reductie tussen Taylor-expansies geïnduceerd door een werkelijke reductie in de bron-$\lambda$-calculus?

Formeel gezien: als er een reductie $T(M) \twoheadrightarrow_r T(N)$ bestaat in de resource calculus (die werkt op oneindige lineaire combinaties van resource-termen), bestaat er dan een $\beta$-reductiesequentie $M \to_\beta N$? De auteurs maken onderscheid tussen twee instellingen:

1. Eindige $\lambda$-calculus: Termen zijn eindig en reducties zijn eindige sequenties.
2. Infinitaire $\lambda$-calculus ($\lambda^{001}$): Termen kunnen oneindig zijn (coïnductief) en reducties kunnen oneindige sequenties zijn ($\to^{001}_\beta$), mits redexen worden afgevuurd op toenemende diepten.

Het centrale probleem is of de lineaire benadering een conservatieve uitbreiding is van de broncalculus in deze instellingen.

Methodologie
De auteurs maken gebruik van een combinatie van herschrijvingstheorie, coïnductieve definities en de "mashup"-techniek (het relateren van brontermen aan hun resource-benaderingen).

1. Analyse van het eindige geval: Voor eindige termen passen de auteurs de "mashup"-bewijstechniek toe die gebruikt wordt door Kerinec en Vaux Auclair. Ze definiëren een relatie $\vdash$ die een $\lambda$-term verbindt met zijn resource-benaderingen. Door te bewijzen dat als $T(M) \twoheadrightarrow_r T(N)$, dan $M \vdash T(N)$, en vervolgens dat $M \vdash T(N)$ impliceert dat $M \to^*_\beta N$, vestigen zij de conservativiteit voor het eindige geval.
2. Infinitair tegenvoorbeeld (De Accordion): Om het infinitaire geval aan te pakken, construeren de auteurs een specifiek tegenvoorbeeld, de Accordion ($A$). Deze term is ontworpen om een oneindige reductiesequentie te simuleren die de structuur "uitrekt" en "samendrukt".
   • De term $A$ reduceert naar een sequentie van termen $A_n$ die een oneindige term $\bar{A} = (\langle T \rangle)(\langle F \rangle)\omega$ benaderen.
   • Cruciaal is dat terwijl $T(A) \twoheadrightarrow_r T(\bar{A})$ geldt, de auteurs bewijzen dat er geen geldige infinitaire $\beta$-reductie $A \to^{001}_\beta \bar{A}$ bestaat. De reductiepaden van $A$ vereisen "globale" stappen op begrensde diepten die de stratificatievoorwaarde schenden die vereist is voor infinitaire $\beta$-reductie (Lemma 2.5).
3. Uniformiteit en Coherentie: Om de conservativiteit in de infinitaire instelling te herstellen, introduceren de auteurs uniformiteit, een eigenschap die oorspronkelijk centraal stond in het werk van Ehrhard en Regnier. Ze definiëren een coherentierelatie ($\bowtie$) op resource-termen en beperken de reductierelatie tot uniforme sommen (sommen waarbij alle elementen paarwijs coherent zijn).
   • Ze definiëren een uniforme resource-reductie ($\to^{\curvearrowright}_r$) en de infinitaire afsluiting daarvan ($\to^{\curvearrowright \infty}_r$).
   • Deze beperking zorgt ervoor dat reducties in de resource calculus strikt overeenkomen met reducties in de broncalculus, waardoor "niet-uniforme" paden die niet naar werkelijke $\beta$-reducties leiden, worden geëlimineerd.
4. Extensie naar $\beta_\perp$: De auteurs breiden deze resultaten uit naar $\beta_\perp$-reductie (die onoplosbare termen naar $\bot$ laat inklappen) en tonen aan dat uniformiteit de conservativiteit behoudt, zelfs wanneer $\bot$-reducties betrokken zijn.

Kernbijdragen

1. Conservativiteit voor eindige termen: Het artikel levert een rigoureus bewijs dat de lineaire benadering conservatief is ten opzichte van de eindige $\lambda$-calculus (Theorem 3.1).
2. Niet-conservativiteit voor infinitaire termen: De auteurs tonen aan dat de standaard pointwise resource-reductie ($\twoheadrightarrow_r$) niet conservatief is ten opzichte van de infinitaire $\lambda$-calculus. Ze construeren het Accordion-tegenvoorbeeld (Theorem 4.4) en bewijzen dat $T(A) \two^rightarrow_r T(\bar{A})$ niet impliceert dat $A \to^{001}_\beta \bar{A}$.
3. Herstel via Uniformiteit: Het artikel identificeert uniformiteit als het ontbrekende ingrediënt om de conservativiteit in de infinitaire instelling te herstellen. Door de resource calculus te beperken tot uniforme reducties ($\to^{\curvearrowright \infty}_r$), bewijzen de auteurs dat de lineaire benadering een conservatieve uitbreiding is van de infinitaire $\lambda$-calculus (Theorem 5.10).
4. Extensie naar $\beta_\perp$: De resultaten worden gegeneraliseerd naar $\beta_\perp$-reducties, waarbij wordt aangetoond dat de uniforme benadering ook conservatief blijft voor $\beta_\perp$-reducties (die betrokken zijn bij de relatie met Böhm-bomen).

Resultaten

• Eindige instelling: De simulatie van eindige $\beta$-reductie door resource-reductie is conservatief.
• Infinitaire instelling (Standaard): De simulatie van infinitaire $\beta$-reductie door standaard pointwise resource-reductie is niet-conservatief. De Accordion-term $A$ reduceert naar $\bar{A}$ in de resource calculus, maar niet in de $\lambda$-calculus.
• Infinitaire instelling (Uniform): De simulatie van infinitaire $\beta$-reductie door uniforme resource-reductie is conservatief.
• $\beta_\perp$ Instelling: De niet-conservativiteit van de standaard reductie strekt zich uit tot $\beta_\perp$-reductie, terwijl de uniforme reductie ook voor $\beta_\perp$ conservatief blijft.

Betekenis
Dit artikel verheldert de precieze voorwaarden waaronder de lineaire benadering dient als een getrouwe modellering van de dynamica van de $\lambda$-calculus. Het lost een vermoeden op uit de PhD-thesis van de eerste auteur betreffende de niet-conservativiteit van de kwantitatieve lineaire benadering in de infinitaire instelling.

De primaire betekenis ligt in de identificatie van uniformiteit, niet alleen als een semantische eigenschap van Taylor-expansies, maar als een noodzakelijke syntactische beperking op de reductierelatie zelf om conservativiteit te waarborgen. Zonder deze beperking staat de resource calculus "geest-reducties" toe die geen tegenhanger hebben in de broncalculus, met name in de aanwezigheid van oneindige termen. Het werk verfijnt het begrip van het "commutation theorem" (normalisatie commuteert met benadering) door onderscheid te maken tussen simulatie en conservativiteit, waarbij wordt aangetoond dat hoewel simulatie algemeen geldt, conservativiteit een striktere uniforme framework vereist.