The Difference Lambda-Calculus: A Language for Difference Categories
Mario Alvarez-Picallo, C.-H. Luke Ong

TL;DR
This paper introduces a new simply-typed calculus with syntactic infinitesimals that models Cartesian difference categories, extending differential lambda-calculus to incorporate difference categories with well-behaved exponentials.
Contribution
It develops a novel calculus with syntactic infinitesimals and establishes a correspondence with difference lambda-categories, broadening the theoretical framework of differential lambda-calculus.
Findings
Constructed a simply-typed calculus with syntactic infinitesimals.
Established models of the calculus as difference lambda-categories.
Extended differential lambda-calculus to include difference categories with exponentials.
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 lambda-calculus equipped with syntactic infinitesimals and show how its models correspond to difference lambda-categories, a family of Cartesian difference categories equipped with suitably well-behaved exponentials.
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.
Taxonomy
TopicsLogic, programming, and type systems
