Document Open Access Logo

How to Play the Accordion: Uniformity and the (Non-)Conservativity of the Linear Approximation of the λ-Calculus

Authors Rémy Cerda , Lionel Vaux Auclair

PDF

File

Thumbnail PDF
PDF
LIPIcs.STACS.2025.23.pdf
  • Filesize: 1.06 MB
  • 21 pages

Document Identifiers

Related Versions

  • A short abstract of a preliminary version of this work has been presented at the 7th International Workshop on Trends in Linear Logic and its Applications (TLLA'23). Most of this work has also appeared in the first author’s PhD thesis, with the noticeable difference that Theorem 27 was only proved in a qualitative setting.
  • Previous Version (Short abstract presented at TLLA'23) https://lipn.univ-paris13.fr/TLLA/2023/abstracts/05-Final.pdf
  • Previous Version (PhD thesis version, see Chapter 5) https://hal.science/tel-04664728

Subject Classification

ACM Subject Classification
  • Theory of computation → Rewrite systems
  • Theory of computation → Lambda calculus
  • Theory of computation → Proof theory
  • Theory of computation → Linear logic
Keywords
  • program approximation
  • quantitative semantics
  • lambda-calculus
  • linear approximation
  • Taylor expansion
  • conservativity

Metrics

  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    0
    PDF Downloads
    0
    Metadata Views

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 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.

Cite As Get BibTex

Rémy Cerda and Lionel Vaux Auclair. How to Play the Accordion: Uniformity and the (Non-)Conservativity of the Linear Approximation of the λ-Calculus. In 42nd International Symposium on Theoretical Aspects of Computer Science (STACS 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 327, pp. 23:1-23:21, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025) https://doi.org/10.4230/LIPIcs.STACS.2025.23

Author Details

Rémy Cerda
  • Aix-Marseille Université, CNRS, I2M, France
  • Université Paris Cité, CNRS, IRIF, F-75013, Paris, France
Lionel Vaux Auclair
  • Aix-Marseille Université, CNRS, I2M, France

Funding

  • Cerda, Rémy: Partially supported by the French ANR project RECIPROG (ANR-21-CE48-019).
  • Vaux Auclair, Lionel: Partially supported by the French ANR projects LambdaComb (ANR-21-CE48-0017), RECIPROG (ANR-21-CE48-019), and PPS (ANR-19-CE48-0014).

References

  1. Davide Barbarossa. Resource approximation for the λμ-calculus. In Proceedings of the 37th Annual ACM/IEEE Symposium on Logic in Computer Science, 2022. URL: https://doi.org/10.1145/3531130.3532469.
  2. Davide Barbarossa and Giulio Manzonetto. Taylor Subsumes Scott, Berry, Kahn and Plotkin. In 47th Symposium on Principles of Programming Languages, 2020. URL: https://doi.org/10.1145/3371069.
  3. Henk P. Barendregt. The Lambda Calculus. Elsevier, Amsterdam, 2 edition, 1984. Google Scholar
  4. Henk P. Barendregt and Giulio Manzonetto. A Lambda Calculus Satellite. Number 94 in Mathematical logic and foundations. College publications, 2022. Google Scholar
  5. Lison Blondeau-Patissier, Pierre Clairambault, and Lionel Vaux Auclair. Extensional Taylor Expansion, 2024. URL: https://arxiv.org/abs/2305.08489v2.
  6. Rémy Cerda. Nominal algebraic-coalgebraic data types, with applications to infinitary λ-calculi. To appear in the proceedings of the 12th International Workshop on Fixed Points in Computer Science (FICS'24). Google Scholar
  7. Rémy Cerda. Taylor Approximation and Infinitary λ-Calculi. PhD thesis, Aix-Marseille Université, 2024. URL: https://hal.science/tel-04664728.
  8. Rémy Cerda and Lionel Vaux Auclair. Finitary Simulation of Infinitary β-Reduction via Taylor Expansion, and Applications. Logical Methods in Computer Science, 19, 2023. URL: https://doi.org/10.46298/LMCS-19(4:34)2023.
  9. Jules Chouquet and Christine Tasson. Taylor expansion for call-by-push-value. In 28th EACSL Annual Conference on Computer Science Logic, 2020. URL: https://doi.org/10.4230/LIPICS.CSL.2020.16.
  10. Ugo Dal Lago and Thomas Leventis. On the Taylor Expansion of Probabilistic Lambda Terms. In Herman Geuvers, editor, 4th International Conference on Fromal Structures for Computation and Deduction, 2019. URL: https://doi.org/10.4230/LIPIcs.FSCD.2019.13.
  11. Daniel de Carvalho. Execution time of λ-terms via denotational semantics and intersection types. Mathematical Structures in Computer Science, 28(7):1169-1203, 2017. URL: https://doi.org/10.1017/s0960129516000396.
  12. Aloÿs Dufour and Damiano Mazza. Böhm and Taylor for All! In 9th International Conference on Formal Structures for Computation and Deduction (FSCD 2024), 2024. URL: https://doi.org/10.4230/LIPICS.FSCD.2024.29.
  13. Thomas Ehrhard. On Köthe sequence spaces and linear logic. Mathematical Structures in Computer Science, 12(5):579-623, 2002. URL: https://doi.org/10.1017/s0960129502003729.
  14. Thomas Ehrhard. Finiteness spaces. Mathematical Structures in Computer Science, 15(4):615-646, 2005. URL: https://doi.org/10.1017/S0960129504004645.
  15. Thomas Ehrhard and Giulio Guerrieri. The bang calculus: an untyped lambda-calculus generalizing call-by-name and call-by-value. In Proceedings of the 18th International Symposium on Principles and Practice of Declarative Programming, 2016. URL: https://doi.org/10.1145/2967973.2968608.
  16. Thomas Ehrhard and Laurent Regnier. The differential lambda-calculus. Theoretical Computer Science, 309(1):1-41, 2003. URL: https://doi.org/10.1016/S0304-3975(03)00392-X.
  17. Thomas Ehrhard and Laurent Regnier. Differential interaction nets. Electronic Notes in Theoretical Computer Science, 123:35-74, 2005. URL: https://doi.org/10.1016/j.entcs.2004.06.060.
  18. Thomas Ehrhard and Laurent Regnier. Böhm Trees, Krivine’s Machine and the Taylor Expansion of Lambda-Terms. In Arnold Beckmann, Ulrich Berger, Benedikt Löwe, and John V. Tucker, editors, Logical Approaches to Computational Barriers, pages 186-197. Springer, 2006. URL: https://doi.org/10.1007/11780342_20.
  19. Thomas Ehrhard and Laurent Regnier. Uniformity and the Taylor expansion of ordinary lambda-terms. Theoretical Computer Science, 403(2):347-372, 2008. URL: https://doi.org/10.1016/j.tcs.2008.06.001.
  20. Jean-Yves Girard. Linear logic. Theoretical Computer Science, 50:1-102, 1987. URL: https://doi.org/10.1016/0304-3975(87)90045-4.
  21. Martin Hyland. A syntactic characterization of the equality in some models for the lambda calculus. Journal of the London Mathematical Society, s2-12:361-370, 1976. URL: https://doi.org/10.1112/jlms/s2-12.3.361.
  22. Richard Kennaway, Jan Willem Klop, Ronan Sleep, and Fer-Jan de Vries. Infinitary lambda calculus. Theoretical Computer Science, 175(1):93-125, 1997. URL: https://doi.org/10.1016/S0304-3975(96)00171-5.
  23. Axel Kerinec, Giulio Manzonetto, and Michele Pagani. Revisiting Call-by-value Böhm trees in light of their Taylor expansion. Logical Methods in Computer Science, 16:1860-5974, 2020. URL: https://lmcs.episciences.org/6638, URL: https://doi.org/10.23638/LMCS-16(3:6)2020.
  24. Axel Kerinec and Lionel Vaux Auclair. The algebraic λ-calculus is a conservative extension of the ordinary λ-calculus, 2023. https://arxiv.org/abs/2305.01067, URL: https://doi.org/10.48550/arXiv.2305.01067.
  25. Jean-Louis Krivine. Lambda-calcul, types et modèles. Masson, 1990. Google Scholar
  26. Damiano Mazza. An axiomatic notion of approximation for programming languages and machines, 2021. Unpublished. URL: https://www.lipn.fr/~mazza/papers/ApxAxiom.pdf.
  27. Jean-Baptiste Midez. Une étude combinatoire du lambda-calcul avec ressources uniforme. PhD thesis, Aix-Marseille Université, 2014. URL: http://www.theses.fr/2014AIXM4093.
  28. Gerd Mitschke. The standardization theorem for λ‐calculus. Zeitschrift für mathematische Logik und Grundlagen der Mathematik, 25:29-31, 1979. URL: https://doi.org/10.1002/malq.19790250104.
  29. Dana Scott. A type-theoretical alternative to ISWIM, CUCH, OWHY. Theoretical Computer Science, 121(1–2):411-440, 1993. URL: https://doi.org/10.1016/0304-3975(93)90095-b.
  30. Terese. Term Rewriting Systems. Cambridge University Press, 2003. Google Scholar
  31. Lionel Vaux. Normalizing the Taylor expansion of non-deterministic λ-terms, via parallel reduction of resource vectors. Logical Methods in Computer Science, 15:9:1-9:57, 2019. URL: https://doi.org/10.23638/LMCS-15(3:9)2019.
  32. Christopher P. Wadsworth. Approximate reduction and lambda calculus models. SIAM Journal on Computing, 7(3):337-356, 1978. URL: https://doi.org/10.1137/0207028.
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail
© 2023-2025 Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact