@article{blute_differential_2019,
title = {Differential {Categories} {Revisited}},
issn = {1572-9095},
url = {https://doi.org/10.1007/s10485-019-09572-y},
doi = {10/ggdm44},
abstract = {Differential categories were introduced to provide a minimal categorical doctrine for differential linear logic. Here we revisit the formalism and, in particular, examine the two different approaches to defining differentiation which were introduced. The basic approach used a deriving transformation, while a more refined approach, in the presence of a bialgebra modality, used a codereliction. The latter approach is particularly relevant to linear logic settings, where the coalgebra modality is monoidal and the Seely isomorphisms give rise to a bialgebra modality. Here, we prove that these apparently distinct notions of differentiation, in the presence of a monoidal coalgebra modality, are completely equivalent. Thus, for linear logic settings, there is only one notion of differentiation. This paper also presents a number of separating examples for coalgebra modalities including examples which are and are not monoidal, as well as examples which do and do not support differential structure. Of particular interest is the observation that—somewhat counter-intuitively—differential algebras never induce a differential category although they provide a monoidal coalgebra modality. On the other hand, Rota–Baxter algebras—which are usually associated with integration—provide an example of a differential category which has a non-monoidal coalgebra modality.},
language = {en},
urldate = {2019-11-28},
journal = {Applied Categorical Structures},
author = {Blute, R. F. and Cockett, J. R. B. and Lemay, J.-S. P. and Seely, R. A. G.},
month = jul,
year = {2019},
note = {ZSCC: NoCitationData[s1]},
keywords = {Differential Linear Logic, Differentiation, Linear logic}
}
@article{ehrhard_differentials_2019,
title = {Differentials and distances in probabilistic coherence spaces},
url = {http://arxiv.org/abs/1902.04836},
abstract = {In probabilistic coherence spaces, a denotational model of probabilistic functional languages, mor-phisms are analytic and therefore smooth. We explore two related applications of the corresponding derivatives. First we show how derivatives allow to compute the expectation of execution time in the weak head reduction of probabilistic PCF (pPCF). Next we apply a general notion of "local" differential of morphisms to the proof of a Lipschitz property of these morphisms allowing in turn to relate the observational distance on pPCF terms to a distance the model is naturally equipped with. This suggests that extending probabilistic programming languages with derivatives, in the spirit of the differential lambda-calculus, could be quite meaningful.},
urldate = {2019-11-28},
journal = {arXiv:1902.04836 [cs]},
author = {Ehrhard, Thomas},
month = feb,
year = {2019},
note = {ZSCC: 0000000
arXiv: 1902.04836},
keywords = {Coherence spaces, Denotational semantics, Differential Linear Logic, Differentiation, Linear logic, Probabilistic programming, Programming language theory}
}
@inproceedings{kerjean_higher-order_2019,
address = {Cham},
series = {Lecture {Notes} in {Computer} {Science}},
title = {Higher-{Order} {Distributions} for {Differential} {Linear} {Logic}},
isbn = {978-3-030-17127-8},
doi = {10/ggdmrj},
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, which 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 the interpretation of differential linear logic without promotion.},
language = {en},
booktitle = {Foundations of {Software} {Science} and {Computation} {Structures}},
publisher = {Springer International Publishing},
author = {Kerjean, Marie and Pacaud Lemay, Jean-Simon},
editor = {Bojańczyk, Mikołaj and Simpson, Alex},
year = {2019},
note = {ZSCC: NoCitationData[s1]},
keywords = {Denotational semantics, Differential Linear Logic, Differentiation, Linear logic},
pages = {330--347}
}
@article{ehrhard_introduction_2016,
title = {An introduction to {Differential} {Linear} {Logic}: proof-nets, models and antiderivatives},
shorttitle = {An introduction to {Differential} {Linear} {Logic}},
url = {http://arxiv.org/abs/1606.01642},
abstract = {Differential Linear Logic enriches Linear Logic with additional logical rules for the exponential connectives, dual to the usual rules of dereliction, weakening and contraction. We present a proof-net syntax for Differential Linear Logic and a categorical axiomatization of its denotational models. We also introduce a simple categorical condition on these models under which a general antiderivative operation becomes available. Last we briefly describe the model of sets and relations and give a more detailed account of the model of finiteness spaces and linear and continuous functions.},
urldate = {2019-11-28},
journal = {arXiv:1606.01642 [cs]},
author = {Ehrhard, Thomas},
month = jun,
year = {2016},
note = {ZSCC: 0000002
arXiv: 1606.01642},
keywords = {Denotational semantics, Differential Linear Logic, Differentiation, Linear logic}
}
@article{blute_convenient_2010,
title = {A convenient differential category},
url = {http://arxiv.org/abs/1006.3140},
abstract = {In this paper, we show that the category of Mackey-complete, separated, topological convex bornological vector spaces and bornological linear maps is a differential category. Such spaces were introduced by Fr{\textbackslash}"olicher and Kriegl, where they were called convenient vector spaces. While much of the structure necessary to demonstrate this observation is already contained in Fr{\textbackslash}"olicher and Kriegl's book, we here give a new interpretation of the category of convenient vector spaces as a model of the differential linear logic of Ehrhard and Regnier. Rather than base our proof on the abstract categorical structure presented by Fr{\textbackslash}"olicher and Kriegl, we prefer to focus on the bornological structure of convenient vector spaces. We believe bornological structures will ultimately yield a wide variety of models of differential logics.},
urldate = {2019-11-28},
journal = {arXiv:1006.3140 [cs, math]},
author = {Blute, Richard and Ehrhard, Thomas and Tasson, Christine},
month = jun,
year = {2010},
note = {ZSCC: 0000054
arXiv: 1006.3140},
keywords = {Differential Linear Logic, Differentiation, Linear logic}
}
@article{fiore_cartesian_2008,
title = {The cartesian closed bicategory of generalised species of structures},
volume = {77},
issn = {00246107},
url = {http://doi.wiley.com/10.1112/jlms/jdm096},
doi = {10/bd2mr9},
abstract = {The concept of generalised species of structures between small categories and, correspondingly, that of generalised analytic functor between presheaf categories are introduced. An operation of substitution for generalised species, which is the counterpart to the composition of generalised analytic functors, is also put forward. These deﬁnitions encompass most notions of combinatorial species considered in the literature—including of course Joyal’s original notion—together with their associated substitution operation. Our ﬁrst main result exhibits the substitution calculus of generalised species as arising from a Kleisli bicategory for a pseudo-comonad on profunctors. Our second main result establishes that the bicategory of generalised species of structures is cartesian closed.},
language = {en},
number = {1},
urldate = {2019-11-28},
journal = {Journal of the London Mathematical Society},
author = {Fiore, M. and Gambino, N. and Hyland, M. and Winskel, G.},
month = feb,
year = {2008},
note = {ZSCC: 0000067},
keywords = {Denotational semantics, Differential Linear Logic, Differentiation, Linear logic},
pages = {203--220}
}
@inproceedings{fiore_differential_2007,
address = {Berlin, Heidelberg},
series = {Lecture {Notes} in {Computer} {Science}},
title = {Differential {Structure} in {Models} of {Multiplicative} {Biadditive} {Intuitionistic} {Linear} {Logic}},
isbn = {978-3-540-73228-0},
doi = {10/c8vgx8},
abstract = {In the first part of the paper I investigate categorical models of multiplicative biadditive intuitionistic linear logic, and note that in them some surprising coherence laws arise. The thesis for the second part of the paper is that these models provide the right framework for investigating differential structure in the context of linear logic. Consequently, within this setting, I introduce a notion of creation operator (as considered by physicists for bosonic Fock space in the context of quantum field theory), provide an equivalent description of creation operators in terms of creation maps, and show that they induce a differential operator satisfying all the basic laws of differentiation (the product and chain rules, the commutation relations, etc.).},
language = {en},
booktitle = {Typed {Lambda} {Calculi} and {Applications}},
publisher = {Springer},
author = {Fiore, Marcelo P.},
editor = {Della Rocca, Simona Ronchi},
year = {2007},
note = {ZSCC: NoCitationData[s1]},
keywords = {Differential Linear Logic, Differentiation, Linear logic},
pages = {163--177}
}
@article{ehrhard_differential_2006,
series = {Logic, {Language}, {Information} and {Computation}},
title = {Differential interaction nets},
volume = {364},
issn = {0304-3975},
url = {http://www.sciencedirect.com/science/article/pii/S0304397506005299},
doi = {10/bg5g4b},
abstract = {We introduce interaction nets for a fragment of the differential lambda-calculus and exhibit in this framework a new symmetry between the of course and the why not modalities of linear logic, which is completely similar to the symmetry between the tensor and par connectives of linear logic. We use algebraic intuitions for introducing these nets and their reduction rules, and then we develop two correctness criteria (weak typability and acyclicity) and show that they guarantee strong normalization. Finally, we outline the correspondence between this interaction nets formalism and the resource lambda-calculus.},
language = {en},
number = {2},
urldate = {2019-11-28},
journal = {Theoretical Computer Science},
author = {Ehrhard, T. and Regnier, L.},
month = nov,
year = {2006},
note = {ZSCC: 0000146},
keywords = {Differential Linear Logic, Differentiation, Linear logic},
pages = {166--195}
}