Integration in Cones

TL;DR

This paper develops a theory of integration for measurable cones, enabling their use as models for probabilistic programming languages with features like sampling and continuous data types.

Contribution

It introduces a Pettis integral adaptation for cones, establishing a new model of Linear Logic with two exponential comonads based on integrable functions.

Findings

Integrable cones form a model of Linear Logic.

Two exponential comonads are constructed for these cones.

The theory supports interpretation of sampling primitives in 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.