The difference λ-calculus: a language for difference categories
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 inf...
| Huvudupphovsmän: | , |
|---|---|
| Materialtyp: | Conference item |
| Språk: | English |
| Publicerad: |
Schloss Dagstuhl - Leibniz-Zentrum für Informatik
2020
|
| _version_ | 1826260087467933696 |
|---|---|
| author | Alvarez-Picallo, M Ong, CL |
| author_facet | Alvarez-Picallo, M Ong, CL |
| author_sort | Alvarez-Picallo, M |
| collection | OXFORD |
| description | 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. |
| first_indexed | 2024-03-06T19:00:03Z |
| format | Conference item |
| id | oxford-uuid:1336b551-8a05-4a6a-966c-23e9b8f890f9 |
| institution | University of Oxford |
| language | English |
| last_indexed | 2024-03-06T19:00:03Z |
| publishDate | 2020 |
| publisher | Schloss Dagstuhl - Leibniz-Zentrum für Informatik |
| record_format | dspace |
| spelling | oxford-uuid:1336b551-8a05-4a6a-966c-23e9b8f890f92022-03-26T10:12:39ZThe difference λ-calculus: a language for difference categoriesConference itemhttp://purl.org/coar/resource_type/c_5794uuid:1336b551-8a05-4a6a-966c-23e9b8f890f9EnglishSymplectic ElementsSchloss Dagstuhl - Leibniz-Zentrum für Informatik2020Alvarez-Picallo, MOng, CLCartesian 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. |
| spellingShingle | Alvarez-Picallo, M Ong, CL The difference λ-calculus: a language for difference categories |
| title | The difference λ-calculus: a language for difference categories |
| title_full | The difference λ-calculus: a language for difference categories |
| title_fullStr | The difference λ-calculus: a language for difference categories |
| title_full_unstemmed | The difference λ-calculus: a language for difference categories |
| title_short | The difference λ-calculus: a language for difference categories |
| title_sort | difference λ calculus a language for difference categories |
| work_keys_str_mv | AT alvarezpicallom thedifferencelcalculusalanguagefordifferencecategories AT ongcl thedifferencelcalculusalanguagefordifferencecategories AT alvarezpicallom differencelcalculusalanguagefordifferencecategories AT ongcl differencelcalculusalanguagefordifferencecategories |