HAL will be down for maintenance from Friday, June 10 at 4pm through Monday, June 13 at 9am. More information
Skip to Main content Skip to Navigation
Preprints, Working Papers, ...

Higher-order distributions for differential linear logic.

Abstract : Linear Logic was introduced as the computational counterpart of the algebraic notion of linearity. Differential Linear Logic refines Linear Logic with a proof-theoretical interpretation of the geometrical process of differentiation. In this article, we construct a polarized model of Differential Linear Logic satisfying computational constraints such as an interpretation for higher-order functions, as well as constraints inherited from physics such as a continuous interpretation for spaces. This extends what was done previously by Kerjean for first order Differential Linear Logic without promotion. Concretely, we follow the previous idea of interpreting the exponential of Differential Linear Logic as a space of higher-order distributions with compact-support, and is constructed as an inductive limit of spaces of distributions on Euclidean spaces. We prove that this exponential is endowed with a co-monadic like structure, with the notable exception that it is functorial only on isomorphisms. Interestingly, as previously argued by Ehrhard, this still allows one to interpret differential linear logic without promotion.
Document type :
Preprints, Working Papers, ...
Complete list of metadata

Cited literature [23 references]  Display  Hide  Download

https://hal.inria.fr/hal-01969262
Contributor : Marie Kerjean Connect in order to contact the contributor
Submitted on : Wednesday, January 16, 2019 - 4:02:07 PM
Last modification on : Wednesday, April 27, 2022 - 3:46:03 AM

File

Higher-order-iso.pdf
Files produced by the author(s)

Identifiers

  • HAL Id : hal-01969262, version 2

Citation

Marie Kerjean, Jean-Simon Lemay. Higher-order distributions for differential linear logic.. 2019. ⟨hal-01969262v2⟩

Share

Metrics

Record views

262

Files downloads

375