Measurable cones and stable, measurable functions: a model for probabilistic higher-order programming

2017/11/27 by Thomas Ehrhard, Michele Pagani, Christine Tasson · 2 citations
Computer Science · #Algebra over a field #Cartesian closed category #Constraint Satisfaction and Optimization #Denotational semantics #Extension (predicate logic) #Logic, Reasoning, and Knowledge #Logic, programming, and type systems #Measurable function #Probabilistic logic #Semantics (computer science) #Soundness #cs.LO #cs.PL

paper · pdf · doi:10.1145/3158147

arxiv created 2017/11/27 · arxiv updated 2017/11/28 · openalex created_date 2017/12/04 · openalex publication_date 2017/12/27 · openalex updated_date 2026/08/05

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.

Citations

• LCF considered as a programming language
• Semantics of probabilistic programs

Cited by

• Densities of Almost Surely Terminating Probabilistic Programs are Differentiable Almost Everywhere
• A Monad for Probabilistic Point Processes