2026-07-20T05:24:08Z https://drops.dagstuhl.de/oai

oai:drops-oai.dagstuhl.de:22848 2025-10-02T13:35:24Z ddc:004 open_access

How to Play the Accordion: Uniformity and the (Non-)Conservativity of the Linear Approximation of the λ-Calculus Cerda, Rémy Vaux Auclair, Lionel program approximation quantitative semantics lambda-calculus linear approximation Taylor expansion conservativity 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 write the Taylor formula in various λ-calculi, hence providing a theory of linear approximations for these calculi. In the standard λ-calculus, this linear approximation is expressed by results stating that the (possibly) infinitary β-reduction of λ-terms is simulated by the reduction of their Taylor expansion: in terms of rewriting systems, the resource reduction (operating on Taylor approximants) is an extension of the β-reduction. In this paper, we address the converse property, conservativity: are there reductions of the Taylor approximants that do not arise from an actual β-reduction of the approximated term? 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. Schloss Dagstuhl – Leibniz-Zentrum für Informatik Rémy Cerda and Lionel Vaux Auclair 2025 Is Part Of LIPIcs, Volume 327, 42nd International Symposium on Theoretical Aspects of Computer Science (STACS 2025) InProceedings Text doc-type:ResearchArticle publishedVersion application/pdf doi:10.4230/LIPIcs.STACS.2025.23 urn:nbn:de:0030-drops-228480 https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.STACS.2025.23 eng https://creativecommons.org/licenses/by/4.0/legalcode