Categorical Models of the Differential λ-Calculus Revisited
| Autor: | Jonathan Gallagher, J. R. B. Cockett |
|---|---|
| Rok vydání: | 2016 |
| Předmět: |
Pure mathematics
General Computer Science 010102 general mathematics Structure (category theory) Differential structure Differential Lambda Calculus 0102 computer and information sciences Extension (predicate logic) 01 natural sciences Theoretical Computer Science Cartesian closed category 010201 computation theory & mathematics Computer Science::Logic in Computer Science Idempotence Scott-Koymans 0101 mathematics Categorical Models Inexact differential Turing computer Differential (mathematics) Computer Science(all) Mathematics computer.programming_language |
| Zdroj: | MFPS |
| ISSN: | 1571-0661 |
| DOI: | 10.1016/j.entcs.2016.09.032 |
| Popis: | The paper shows that the Scott-Koymans theorem for the untyped λ-calculus extends to the differential λ-calculus. The main result is that every model of the untyped differential λ-calculus may be viewed as a differential reflexive object in a Cartesian closed differential category. This extension of the Scott-Koymans theorem depends critically on unravelling the somewhat subtle issue of which idempotents can be split so that differential structure lifts to the idempotent splitting. The paper uses (total) Turing categories with “canonical codes” as the basic categorical semantics for the λ-calculus. It shows how the main result may be developed in a modular fashion by first adding left-additive structure to a Turing category, and then – on top of that – differential structure. For both levels of structure it is necessary to identify how “canonical codes” behave with respect to the added structure and, furthermore, how “universal objects” behave. The latter is closely tied to the question – which is the crux of the paper – of which idempotents can be split in these more structured settings. |
| Databáze: | OpenAIRE |
| Externí odkaz: |
|
Full Text from ScienceDirect