A lambda-calculus foundation for universal probabilistic programming
From MaRDI portal
Learning and adaptive systems in artificial intelligence (68T05) Theory of programming languages (68N15) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30) Functional programming and lambda calculus (68N18) Other programming paradigms (object-oriented, sequential, concurrent, automatic, etc.) (68N19) Semantics in the theory of computing (68Q55)
Abstract: We develop the operational semantics of an untyped probabilistic lambda-calculus with continuous distributions, as a foundation for universal probabilistic programming languages such as Church, Anglican, and Venture. Our first contribution is to adapt the classic operational semantics of lambda-calculus to a continuous setting via creating a measure space on terms and defining step-indexed approximations. We prove equivalence of big-step and small-step formulations of this distribution-based semantics. To move closer to inference techniques, we also define the sampling-based semantics of a term as a function from a trace of random samples to a value. We show that the distribution induced by integrating over all traces equals the distribution-based semantics. Our second contribution is to formalize the implementation technique of trace Markov chain Monte Carlo (MCMC) for our calculus and to show its correctness. A key step is defining sufficient conditions for the distribution induced by trace MCMC to converge to the distribution-based semantics. To the best of our knowledge, this is the first rigorous correctness proof for trace MCMC for a higher-order functional language.
Recommendations
- Probabilistic operational semantics for the lambda calculus
- A probabilistic semantics for the pure \(\lambda\)-calculus
- Probabilistic -calculus and Quantitative Program Analysis
- Stochastic lambda calculus and monads of probability distributions
- A Type Theory for Probabilistic \lambda –calculus
- Decomposing probabilistic lambda calculi
- On Probabilistic λ-Calculi
- Foundations of probabilistic programming
- scientific article; zbMATH DE number 1104373
- scientific article; zbMATH DE number 3890702
Cited in
(30)- Running probabilistic programs backwards
- scientific article; zbMATH DE number 7559283 (Why is no real title available?)
- Probabilistic programming language and its incremental evaluation
- Bayesian strategies: probabilistic programs as generalised graphical models
- A fibrational tale of operational logical relations: pure, effectful and differential
- A linear exponential comonad in s-finite transition kernels and probabilistic coherent spaces
- scientific article; zbMATH DE number 7577566 (Why is no real title available?)
- A provably correct sampler for probabilistic programs
- Correctness of sequential Monte Carlo inference for probabilistic programming languages
- Densities of almost surely terminating probabilistic programs are differentiable almost everywhere
- An application of computable distributions to the semantics of probabilistic programming languages
- Commutative semantics for probabilistic programming
- scientific article; zbMATH DE number 7533341 (Why is no real title available?)
- Contextual equivalence for probabilistic programs with continuous random variables and scoring
- On bisimilarity in lambda calculi with continuous probabilistic choice
- A possible worlds semantics for trustworthy non-deterministic computations
- Two decades of automatic amortized resource analysis
- Stochastic lambda calculus and monads of probability distributions
- Relational reasoning for Markov chains in a probabilistic guarded lambda calculus
- The geometry of Bayesian programming
- A probabilistic semantics for the pure \(\lambda\)-calculus
- Probabilistic operational semantics for the lambda calculus
- A probabilistic language based upon sampling functions
- A denotational semantics for low-level probabilistic programs with nondeterminism
- Semantics for probabilistic programming: higher-order functions, continuous distributions, and soft constraints
- Checking trustworthiness of probabilistic computations in a typed natural deduction system
- The geometry of Bayesian programming
- On the Taylor expansion of probabilistic λ-terms
- Automatic alignment in higher-order probabilistic programming languages
- Fast and correct gradient-based optimisation for probabilistic programming via smoothing
This page was built for publication: A lambda-calculus foundation for universal probabilistic programming
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2981999)
