A lambda-calculus foundation for universal probabilistic programming
From MaRDI portal
Theory of programming languages (68N15) Functional programming and lambda calculus (68N18) Other programming paradigms (object-oriented, sequential, concurrent, automatic, etc.) (68N19) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30) Semantics in the theory of computing (68Q55) Learning and adaptive systems in artificial intelligence (68T05)
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
(31)- A probabilistic semantics for the pure \(\lambda\)-calculus
- On bisimilarity in lambda calculi with continuous probabilistic choice
- A denotational semantics for low-level probabilistic programs with nondeterminism
- Correctness of sequential Monte Carlo inference for probabilistic programming languages
- Densities of almost surely terminating probabilistic programs are differentiable almost everywhere
- Bayesian strategies: probabilistic programs as generalised graphical models
- Relational reasoning for Markov chains in a probabilistic guarded lambda calculus
- Running probabilistic programs backwards
- An application of computable distributions to the semantics of probabilistic programming languages
- Probabilistic operational semantics for the lambda calculus
- Contextual equivalence for probabilistic programs with continuous random variables and scoring
- Commutative semantics for probabilistic programming
- Probabilistic programming language and its incremental evaluation
- Semantics for probabilistic programming: higher-order functions, continuous distributions, and soft constraints
- The geometry of Bayesian programming
- Fully abstract models of the probabilistic -calculus
- On the Taylor expansion of probabilistic λ-terms
- Differentials and distances in probabilistic coherence spaces
- Differentials and distances in probabilistic coherence spaces
- Stochastic lambda calculus and monads of probability distributions
- A provably correct sampler for probabilistic programs
- A probabilistic language based upon sampling functions
- Two decades of automatic amortized resource analysis
- A linear exponential comonad in s-finite transition kernels and probabilistic coherent spaces
- Fast and correct gradient-based optimisation for probabilistic programming via smoothing
- Automatic alignment in higher-order probabilistic programming languages
- A fibrational tale of operational logical relations: pure, effectful and differential
- A possible worlds semantics for trustworthy non-deterministic computations
- The geometry of Bayesian programming
- Checking trustworthiness of probabilistic computations in a typed natural deduction system
- Trustworthiness preservation by copies of machine learning systems
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)
