Semantics for probabilistic programming: higher-order functions, continuous distributions, and soft constraints
We study the semantic foundation of expressive probabilistic programming languages, that support higher-order functions, continuous distributions, and soft constraints (such as Anglican, Church, and Venture). We define a metalanguage (an idealised version of Anglican) for probabilistic computation with the above features, develop both operational and denotational semantics, and prove soundness, adequacy, and termination. They involve measure theory, stochastic labelled transition systems, and functor categories, but admit intuitive computational readings, one of which views sampled random variables as dynamically allocated read-only variables. We apply our semantics to validate nontrivial equations underlying the correctness of certain compiler optimisations and inference algorithms such as sequential Monte Carlo simulation. The language enables defining probability distributions on higher-order functions, and we study their properties.
Code (0)
등록된 구현이 없습니다.
Tasks
Probabilistic ProgrammingSimilar Papers 제목 키워드 기반
$ω$PAP Spaces: Reasoning Denotationally About Higher-Order, Recursive Probabilistic and Differentiable Programs
We introduce a new setting, the category of $\omega$PAP spaces, for reasoning denotationally about expressive differentiable and probabilistic programming languages. Our semantics is general enough to assign meanings to …
Probabilistic ProgrammingMinimum Model Semantics for Extensional Higher-order Logic Programming with Negation
Extensional higher-order logic programming has been introduced as a generalization of classical logic programming. An important characteristic of this paradigm is that it preserves all the well-known properties of tradit…
NegationLinear Models of Computation and Program Learning
We consider two classes of computations which admit taking linear combinations of execution runs: probabilistic sampling and generalized animation. We argue that the task of program learning should be more tractable for …
Probabilistic ProgrammingProbabilistic Programming with Densities in SlicStan: Efficient, Flexible and Deterministic
Stan is a probabilistic programming language that has been increasingly used for real-world scalable projects. However, to make practical inference possible, the language sacrifices some of its usability by adopting a bl…
Probabilistic ProgrammingSemantics of higher-order probabilistic programs with conditioning
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, …