Measurable Cones and Stable, Measurable Functions

TL;DR

This paper introduces a new category of stable and measurable maps between cones, providing a denotational model for probabilistic functional programming with soundness and adequacy proofs.

Contribution

It defines a novel category of stable, measurable functions between cones that supports probabilistic programming primitives and proves its soundness and adequacy.

Findings

The category is cpo-enriched and cartesian closed.

It models probabilistic features like distributions, sampling, and conditioning.

The model is proven sound and adequate with respect to operational semantics.

Abstract

We define a notion of stable and measurable map between cones endowed with measurability tests and show that it forms a cpo-enriched cartesian closed category. This category gives a denotational model of an extension of PCF supporting the main primitives of probabilistic functional programming, like continuous and discrete probabilistic distributions, sampling, conditioning and full recursion. We prove the soundness and adequacy of this model with respect to a call-by-name operational semantics and give some examples of its denotations.