Document Open Access Logo

The Difference λ-Calculus: A Language for Difference Categories

Authors Mario Alvarez-Picallo , C.-H. Luke Ong

PDF
Thumbnail PDF

File

LIPIcs.FSCD.2020.32.pdf
  • Filesize: 0.57 MB
  • 21 pages

Document Identifiers

Author Details

Mario Alvarez-Picallo
  • University of Oxford, UK
C.-H. Luke Ong
  • University of Oxford, UK

Cite AsGet BibTex

Mario Alvarez-Picallo and C.-H. Luke Ong. The Difference λ-Calculus: A Language for Difference Categories. In 5th International Conference on Formal Structures for Computation and Deduction (FSCD 2020). Leibniz International Proceedings in Informatics (LIPIcs), Volume 167, pp. 32:1-32:21, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020)
https://doi.org/10.4230/LIPIcs.FSCD.2020.32

Abstract

Cartesian difference categories are a recent generalisation of Cartesian differential categories which introduce a notion of "infinitesimal" arrows satisfying an analogue of the Kock-Lawvere axiom, with the axioms of a Cartesian differential category being satisfied only "up to an infinitesimal perturbation". In this work, we construct a simply-typed calculus in the spirit of the differential λ-calculus equipped with syntactic "infinitesimals" and show how its models correspond to difference λ-categories, a family of Cartesian difference categories equipped with suitably well-behaved exponentials.

Subject Classification

ACM Subject Classification
  • Theory of computation → Type theory
  • Theory of computation → Categorical semantics
  • Theory of computation → Lambda calculus
Keywords
  • Cartesian difference categories
  • Cartesian differential categories
  • Change actions
  • Differential lambda-calculus
  • Difference lambda-calculus

Metrics

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

References

  1. Mario Alvarez-Picallo. Change actions: from incremental computation to discrete derivatives, 2020. URL: http://arxiv.org/abs/2002.05256.
  2. Mario Alvarez-Picallo and Jean-Simon P. Lemay. Cartesian difference categories. In International Conference on Foundations of Software Science and Computation Structures, page to appear. Springer, 2020. Google Scholar
  3. Mario Alvarez-Picallo and Jean-Simon Pacaud Lemay. Cartesian difference categories: Extended report, 2020. URL: http://arxiv.org/abs/2002.01091.
  4. Mario Alvarez-Picallo and C.-H. Luke Ong. Change actions: models of generalised differentiation. In International Conference on Foundations of Software Science and Computation Structures, pages 45-61. Springer, 2019. Google Scholar
  5. Mario Alvarez-Picallo, Michael Peyton-Jones, Alexander Eyers-Taylor, and C.-H. Luke Ong. Fixing incremental computation. In European Symposium on Programming. Springer, 2019. in press. Google Scholar
  6. P Arrighi and G Dowek. Linear-algebraic lambda-calculus: higher-order, encodings and confluence in A. Voronkov, Rewriting techniques and applications. Lecture Notes in Computer Science, Springer-Verlag, 2008. Google Scholar
  7. Pablo Arrighi and Gilles Dowek. A computational definition of the notion of vectorial space. Electronic Notes in Theoretical Computer Science, 117:249-261, 2005. Google Scholar
  8. Richard F. Blute, J. Robin B. Cockett, and Robert A. G. Seely. Cartesian differential categories. Theory and Applications of Categories, 22(23):622-672, 2009. Google Scholar
  9. Antonio Bucciarelli, Thomas Ehrhard, and Giulio Manzonetto. Categorical models for simply typed resource calculi. Electronic Notes in Theoretical Computer Science, 265:213-230, 2010. Google Scholar
  10. J Robin B Cockett and J-S Lemay. Integral categories and calculus categories. Mathematical Structures in Computer Science, 29(2):243-308, 2019. Google Scholar
  11. Thomas Ehrhard. An introduction to differential linear logic: proof-nets, models and antiderivatives. Mathematical Structures in Computer Science, 28(7):995-1060, 2018. Google Scholar
  12. Thomas Ehrhard and Laurent Regnier. The differential lambda-calculus. Theoretical Computer Science, 309(1-3):1-41, 2003. URL: https://doi.org/10.1016/S0304-3975(03)00392-X.
  13. Thomas Ehrhard and Laurent Regnier. Uniformity and the Taylor expansion of ordinary lambda-terms. Theoretical Computer Science, 403(2):347-372, 2008. Google Scholar
  14. René Lavendhomme. Basic concepts of synthetic differential geometry, volume 13. Springer Science & Business Media, 2013. Google Scholar
  15. Jean-Simon Pacaud Lemay. Exponential functions in cartesian differential categories. arXiv preprint arXiv:1911.04790, 2019. Google Scholar
  16. Giulio Manzonetto. What is a Categorical Model of the Differential and the Resource λ-Calculi? Mathematical Structures in Computer Science, 22(03):451-520, 2012. Google Scholar
  17. Lionel Vaux. λ-calculus in an algebraic setting. unpublished note, 2006. Google Scholar
  18. Lionel Vaux. The algebraic lambda calculus. Mathematical Structures in Computer Science, 19(05):1029-1059, 2009. Google Scholar
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-2024 Schloss Dagstuhl – LZI GmbH Imprint Privacy Contact