Commutative Monads for Probabilistic Programming Languages
arXiv:2102.00510 · doi:10.1109/LICS52264.2021.9470611
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.
References in corpus (10)
- Semantics for probabilistic programming: higher-order functions, continuous distributions, and soft constraints
- A Convenient Category for Higher-Order Probability Theory
- A Domain Theory for Statistical Probabilistic Programming
- Mixed powerdomains for probability and nondeterminism
- Commutative Monads for Probabilistic Programming Languages
- Quantum sets
- LNL-FPC: The Linear/Non-linear Fixpoint Calculus
- Domains and Stochastic Processes
- Completing Simple Valuations in K-categories
- Convexity and Order in Probabilistic Call-by-Name FPC
Cited by in corpus (8)
- Commutative Monads for Probabilistic Programming Languages
- Semantics for Variational Quantum Programming
- Quantum Expectation Transformers for Cost Analysis
- Probabilistic programming interfaces for random graphs: Markov categories, graphons, and nominal sets
- A model of stochastic memoization and name generation in probabilistic programming: categorical semantics via monads on presheaf categories
- A Cartesian Closed Category for Random Variables
- Continuous R-valuations
- Universal Semantics for the Stochastic Lambda-Calculus