(Towards a) Statistical Probabilistic Lazy Lambda Calculus

TL;DR

The work addresses the challenge of giving a rigorous semantics for statistical probabilistic programming languages that combine higher-order features with randomness and conditioning. It advances a framework that unites open bisimulation from lazy lambda calculus with probabilistic simulation, implemented in an untyped lazy calculus $\Lambda$ equipped with countable sums and a Lawson-topology-based completion to reason about convergence of distributions. The core technical contributions include a labeled transition system for terms, a liftable notion of probabilistic simulation that is a precongruence, and a continuous-domain perspective that yields a meaningful notion of normalization and conditioning in $StatProb$ languages. The approach aims to provide a principled foundation for approximate reasoning and symbolic manipulation in probabilistic programming, while situating itself among related semantic theories (e.g., probabilistic powerdomains, Quasi Borel Spaces, environmental bisimulation) as a direction for future work.

Abstract

We study the desiderata on a model for statistical probabilistic programming languages. We argue that they can be met by a combination of traditional tools, namely open bisimulation and probabilistic simulation.