Integration in Cones
Thomas Ehrhard, Guillaume Geoffroy
TL;DR
This work extends denotational semantics for probabilistic programming by introducing a Pettis-inspired integration theory on cones, yielding integrable cones that support sampling primitives for continuous data types. It constructs a robust categorical framework where integrable cones form a symmetric monoidal closed category with two exponential comonads, enabling interpretations of call-by-name, call-by-value, and call-by-push-value languages with probabilistic effects. A key novelty is the integration-preserving linear maps and the dual notions of stable and analytic nonlinear morphisms, which together realize a rich semantic landscape bridging measures, paths, and functional programs. The results position integrable cones as a versatile alternative to quasi-Borel spaces and probabilistic coherence spaces, with strong links to linear logic and the operational semantics of probabilistic programming.
Abstract
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.