,
Jean-Simon Pacaud Lemay
Creative Commons Attribution 4.0 International license
In a differential category and in Differential Linear Logic, the exponential conjunction ! admits structural maps, characterizing quantitative operations and symmetric co-structural maps, characterizing differentiation. In this paper, we introduce the notion of a Laplace distributor, which is an extra structural map which distributes the linear negation operation (_)^∗ over ! and transforms the co-structural rules into the structural rules. Laplace distributors are directly inspired by the well-known Laplace transform, which is all-important in numerical analysis. In the star-autonomous setting, a Laplace distributor induces a natural transformation from ! to the exponential disjunction ?, which we then call a Laplace transformation. According to its semantics, we show that Laplace distributors correspond precisely to the notion of a generalized exponential function e^x on the monoidal unit. We also show that many well-known and important examples have a Laplace distributor/transformation, including (weighted) relations, finiteness spaces, Köthe spaces, and convenient vector spaces.
@InProceedings{kerjean_et_al:LIPIcs.FSCD.2024.9,
author = {Kerjean, Marie and Lemay, Jean-Simon Pacaud},
title = {{Laplace Distributors and Laplace Transformations for Differential Categories}},
booktitle = {9th International Conference on Formal Structures for Computation and Deduction (FSCD 2024)},
pages = {9:1--9:21},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-323-2},
ISSN = {1868-8969},
year = {2024},
volume = {299},
editor = {Rehof, Jakob},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2024.9},
URN = {urn:nbn:de:0030-drops-203382},
doi = {10.4230/LIPIcs.FSCD.2024.9},
annote = {Keywords: Differential Categories, Differential Linear Logic, Laplace Distributor, Laplace Transformation, Exponential Function}
}