The Difference Lambda-Calculus: A Language for Difference Categories

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.