How to play the Accordion: Uniformity and the (non-)conservativity of the linear approximation of the λ-calculus (extended version)
Rémy Cerda, Lionel Vaux Auclair
TL;DR
The paper investigates whether the Taylor-based linear approximation of the λ-calculus conservatively captures β-reduction. It proves that the approximation is conservative for finite terms and reductions, but not in the infinitary setting, via the Accordion counterexample. To recover conservativity in the infinitary regime, it introduces a uniformity constraint on Taylor-approximant reductions, showing that uniform linear-approximation provides a conservative extension for infinitary β-reduction and extends to β⊥-reductions. The results clarify the limits of standard Taylor approximation and establish a robust, uniform framework that preserves execution behavior under infinitary and β⊥-reduction contexts. The work also presents a simulation poset organizing the various reduction systems and highlights directions for extending these techniques to richer calculi and nonuniform settings.
Abstract
Twenty years after its introduction by Ehrhard and Regnier, differentiation in $λ$-calculus and in linear logic is now a celebrated tool. In particular, it allows to establish a Taylor expansion formula for various $λ$-calculi, hence providing a theory of linear approximations for these calculi. In the pure $λ$-calculus, the linear approximants of $λ$-terms supporting this Taylor expansion are the terms of a so-called resource calculus, which is equipped with a finitary (strongly normalising) reduction; and the efficiency of this linear approximation is expressed by results stating that the (possibly) infinitary $β$-reduction of $λ$-terms is simulated by the reduction of their Taylor expansions, which is induced by the iterated reduction of resource terms. In terms of rewriting systems, resource reduction (operating on infinite linear combinations of Taylor approximants) is an extension of $β$-reduction. In this article, we address the converse property, conservativity: do all reductions between Taylor expansions arise from actual $β$-reductions? We show that if we restrict the setting to finite terms and $β$-reduction sequences, then the linear approximation is conservative. However, as soon as one allows infinitary reduction sequences this property is broken. We design a counter-example, the Accordion. Then we show how restricting the reduction of the Taylor approximants allows to build a conservative extension of the $β$-reduction preserving good simulation properties; this restriction relies on uniformity, a property that was already at the core of Ehrhard and Regnier's pioneering work. Finally, we extend our work to $β\bot$-reductions, which play a key role in $λ$-calculus as they relate a $λ$-term to its Böhm tree.