Stable, measurable functions and probabilistic programs

In 2014, we proved that the denotational model PCoh of probabilistic coherence spaces and entire functions is fully abstract with respect to the functional “ideal” language PCF enriched with discrete probabilistic distributions (such as a term “coin” evaluating to true or to false with equal probability 0.5). Full abstraction means that the equality in the model corresponds with the contextual equality between programs.

This year, we will present at Popl an extension of the PCoh model supporting also continuous probabilistic distributions, as well as sampling and conditioning. The main issue in working out this extension was to generalize the notion of entire function, at the core of the PCoh model, in order to handle data types associated with uncountable sets, like the set of real numbers. We solve this issue by defining stable maps as Scott-continuous and absolutely monotonic maps between complete normed cones.

In the PPS talk I will try to give more details about the challenge of extending PCoh to “continuous” data types as well as about the crucial role played by the notion of absolute monotonicity in giving the solution. As far as we know, this is the first time that this concept appears in the setting of denotational semantics, although it is standard in mathematics and it shares an intriguing link with Berry’s notion of stability (so justifying our terminology).

You can find an extended version of the popl paper here. In particular, the introduction (section 1) and the related work conclusion (section 8) can be used as a self-contained extended abstract to this talk.

(Joint work with Thomas Ehrhard and Christine Tasson at IRIF, Paris Diderot University, France)

This entry was posted in Uncategorized. Bookmark the permalink.