The Difference Lambda-Calculus: A Language for Difference Categories
Logic in Computer Science
2020-12-01 v1 Programming Languages
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.
Cite
@article{arxiv.2011.14476,
title = {The Difference Lambda-Calculus: A Language for Difference Categories},
author = {Mario Alvarez-Picallo and C. -H. Luke Ong},
journal= {arXiv preprint arXiv:2011.14476},
year = {2020}
}
Comments
40 pages, to be submitted to a special issue of LMCS