Probabilistic Stable Functions on Discrete Cones are Power Series (long version)

TL;DR

This paper demonstrates that measurable stable functions on discrete cones can be represented as generalized power series, establishing a connection between probabilistic coherence spaces and the category of measurable cones.

Contribution

It introduces a functor embedding probabilistic coherence spaces into the category of measurable cones, generalizing Bernstein's theorem to discrete cones.

Findings

Stable functions on discrete cones are representable as power series.

Probabilistic coherence spaces embed fully and faithfully into Cstabm.

The model supports higher-order languages with discrete probabilities and recursion.

Abstract

We study the category Cstabm of measurable cones and measurable stable functions, which is a denotational model of an higher-order language with continuous probabilities and full recursion. We look at Cstabm as a model for discrete probabilities, by showing the existence of a cartesian closed, full and faithful functor which embeds probabilistic coherence spaces (a fully abstract denotational model of an higher-order language with full recursion and discrete probabilities) into Cstabm. The proof is based on a generalization of Bernstein's theorem from real analysis allowing to see stable functions between discrete cones as generalized power series.