Extensional Denotational Semantics of Higher-Order Probabilistic Programs, Beyond the Discrete Case

TL;DR

This paper introduces a mathematical framework for the extensional denotational semantics of higher-order probabilistic programs that extends beyond discrete probabilities and supports recursion and integration.

Contribution

It presents a novel model based on propositional linear logic that handles continuous probabilities and recursion, surpassing previous models limited to discrete cases.

Findings

Supports integration in probabilistic semantics

Provides least fixed points for recursion

Compatible with higher-order probabilistic programming

Abstract

We describe a mathematical structure that can give extensional denotational semantics to higher-order probabilistic programs. It is not limited to discrete probabilities, and it is compatible with integration in a way the models that have been proposed before are not. It is organised as a model of propositional linear logic in which all the connectives have intuitive probabilistic interpretations. In addition, it has least fixed points for all maps, so it can interpret recursion.