Thomas Ehrhard ; Guillaume Geoffroy - Integration in Cones

lmcs:10815 - Logical Methods in Computer Science, January 3, 2025, Volume 21, Issue 1 - https://doi.org/10.46298/lmcs-21(1:1)2025
Integration in ConesArticle

Authors: Thomas Ehrhard ; Guillaume Geoffroy

    Measurable cones, with linear and measurable functions as morphisms, are a model of intuitionistic linear logic and of call-by-name probabilistic PCF which accommodates "continuous data types" such as the real line. So far however, they lacked a major feature to make them a model of more general probabilistic programming languages (notably call-by-value and call-by-push-value languages): a theory of integration for functions whose codomain is a cone, which is the key ingredient for interpreting the sampling programming primitives. The goal of this paper is to develop such a theory: our definition of integrals is an adaptation to cones of Pettis integrals in topological vector spaces. We prove that such integrable cones, with integral-preserving linear maps as morphisms, form a model of Linear Logic for which we develop two exponential comonads: the first based on a notion of stable and measurable functions introduced in earlier work and the second based on a new notion of integrable analytic function on cones.


    Volume: Volume 21, Issue 1
    Published on: January 3, 2025
    Accepted on: September 27, 2024
    Submitted on: January 16, 2023
    Keywords: Computer Science - Logic in Computer Science

    Consultation statistics

    This page has been seen 260 times.
    This article's PDF has been downloaded 86 times.