A Denotational Semantics for Low-Level Probabilistic Programs with Nondeterminism

Probabilistic programming is an increasingly popular formalism for modeling randomness and uncertainty. Designing semantic models for probabilistic programs has been extensively studied, but is technically challenging. Particular complications arise when trying to account for (i) unstructured control-flow, a natural feature in low-level imperative programs; (ii) general recursion, an extensively used programming paradigm; and (iii) nondeterminism, which is often used to represent adversarial actions in probabilistic models, and to support refinement-based development. This paper presents a denotational-semantics framework that supports the three features mentioned above, while allowing nondeterminism to be handled in different ways. To support both probabilistic choice and nondeterministic choice, the semantics is given over control-flow hyper-graphs. The semantics follows an algebraic approach: it can be instantiated in different ways as long as certain algebraic properties hold. In particular, the semantics can be instantiated to support nondeterminism among either program states or state transformers. We develop a new formalization of nondeterminism based on powerdomains over sub-probability kernels. Semantic objects in the powerdomain enjoy a notion we call generalized convexity, which is a generalization of convexity. As an application, the paper sketches an algebraic framework for static analysis of probabilistic programs, which has been proposed in a companion paper.