Semantics of higher-order probabilistic programs with conditioning
This work provides a foundational framework for reasoning about probabilistic programming languages, which is incremental as it builds on existing Banach space theory and Scott semantics.
The authors tackled the problem of defining a formal semantics for higher-order probabilistic programs with conditioning, and they developed a denotational semantics using linear operators between Banach spaces, treating randomness as a resource.
We present a denotational semantics for higher-order probabilistic programs in terms of linear operators between Banach spaces. Our semantics is rooted in the classical theory of Banach spaces and their tensor products, but bears similarities with the well-known Scott semantics of higher-order programs through the use ordered Banach spaces which allow definitions in terms of fixed points. Being based on a monoidal rather than cartesian closed structure, our semantics effectively treats randomness as a resource.