Commutative Monads for Probabilistic Programming Languages

TL;DR

This paper introduces three new commutative monads for probability on DCPO categories, providing a sound denotational semantics for a probabilistic lambda calculus and connecting to existing valuation monads and continuous Kegelspitzen.

Contribution

It presents three novel commutative monads for probability on DCPO, along with a general construction, and applies them to semantics of a probabilistic lambda calculus.

Findings

All three monads coincide with the valuations monad on continuous dcpo's.

The induced Eilenberg-Moore categories are isomorphic to the category of continuous Kegelspitzen.

The monads provide a sound and adequate semantics for PFPC.

Abstract

A long-standing open problem in the semantics of programming languages supporting probabilistic choice is to find a commutative monad for probability on the category DCPO. In this paper we present three such monads and a general construction for finding even more. We show how to use these monads to provide a sound and adequate denotational semantics for the Probabilistic FixPoint Calculus (PFPC) -- a call-by-value simply-typed lambda calculus with mixed-variance recursive types, term recursion and probabilistic choice. We also show that in the special case where we consider continuous dcpo's, then all three monads coincide with the valuations monad of Jones and we fully characterise the induced Eilenberg-Moore categories by showing that they are all isomorphic to the category of continuous Kegelspitzen of Keimel and Plotkin.