文章基本信息

标题：The Difference Î»-Calculus: A Language for Difference Categories
本地全文：下载
作者：Mario Alvarez-Picallo ; C.-H. Luke Ong
期刊名称：LIPIcs : Leibniz International Proceedings in Informatics
电子版ISSN：1868-8969
出版年度：2020
卷号：167
页码：32:1-32:21
DOI：10.4230/LIPIcs.FSCD.2020.32
出版社：Schloss Dagstuhl -- Leibniz-Zentrum fuer Informatik
摘要：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.
关键词：Cartesian difference categories; Cartesian differential categories; Change actions; Differential lambda-calculus; Difference lambda-calculus