Universal Semantics for the Stochastic Lambda-Calculus

TL;DR

This paper introduces sound and adequate semantics for the stochastic lambda calculus, establishing a formal link between operational and denotational views, and resolving a key open problem in probabilistic higher-order programming.

Contribution

It provides the first adequacy theorem connecting operational and denotational semantics for the stochastic lambda calculus.

Findings

Established sound and adequate semantics for stochastic lambda calculus

Proved an adequacy theorem relating operational and denotational semantics

Resolved a major open problem in probabilistic higher-order programming semantics

Abstract

We define sound and adequate denotational and operational semantics for the stochastic lambda calculus. These two semantic approaches build on previous work that used similar techniques to reason about higher-order probabilistic programs, but for the first time admit an adequacy theorem relating the operational and denotational views. This resolves the main issue left open in (Bacci et al. 2018).