论文标题
差异lambda-calculus：差异类别的语言
The Difference Lambda-Calculus: A Language for Difference Categories
论文作者
论文摘要
笛卡尔差异类别是对笛卡尔差异类别的最新概括，这些类别引入了满足Kock-Lawvere Axiom的类似物的“无限”箭头的概念，而笛卡尔差异类别的公理只能满足“无限性触及扰动”。在这项工作中，我们本着配备有句法无限量的差分lambda-alculus的精神构建了一个简单的演算，并展示了其模型如何与lambda类别的差异相对应，Lambda类别是笛卡尔差异类别，配备了适当的行为良好的外交。
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.
