PaperlayerView exact revision on arXiv

Source-linked AI summary

A Lambda-Calculus Foundation for Universal Probabilistic Programming

Johannes Borgström, Ugo Dal Lago, Andrew D. Gordon, Marcin Szymczak

arXiv:1512.08990v5cs.PL

TL;DR

Previous formal semantics for untyped probabilistic lambda-calculi did not rigorously treat continuous distributions together with constraints. This paper defines sampling-based and distribution-based semantics for a calculus with these features and proves trace MCMC correctness. The algorithm’s value distribution matches the calculus semantics conditional on successful termination.

  • Problem

    Previous formal semantics for untyped probabilistic lambda-calculi did not rigorously treat continuous distributions together with constraints, a combination common in machine-learning models.

    Source: §1.2 · p. 4

  • Method

    The paper defines an untyped probabilistic lambda-calculus with continuous draws and constraints, develops sampling-based and step-indexed distribution-based semantics, and formalizes trace MCMC.

    Source: §2.2 · p. 7, §4.2 · p. 24, §7 · p. 40

  • Results

    Trace MCMC converges to a stationary distribution whose induced value distribution equals the distribution-based semantics conditional on successful termination.

    Source: §1.3 · p. 5

  • Takeaways & Limitations

    The calculus and correctness results provide a formal foundation for probabilistic inference in languages such as Church.

    Source: §7 · p. 40

    The semantics restricts scores to positive values bounded by one because recursion with unbounded scores can yield return-value measures that are not σ-finite.

    Source: §4.9 · p. 32

Abstract

from arXiv · show

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.

1 Introduction

Probabilistic programming uses programs to specify probabilistic models for inference, but prior formal semantics did not rigorously address continuous distributions together with constraints in untyped probabilistic lambda-calculi. The paper introduces a calculus and semantics for these features, relates its sampling-based and distribution-based formulations, and proves trace MCMC correctness.

1.1 Universal Probabilistic Programming in Church

  • Church and related functional languages express probabilistic models as programs, including queries that specify a distribution subject to a Boolean constraint.The Church family includes Venture, Anglican, and Web Church; queries can describe distributions with unbounded discrete support or continuous distributions.Source: §1.1 · p. 3

1.2 Problem 1: Semantics of Church Queries

  • The semantics for continuous distributions and constraints address a combination that previous formal accounts of untyped probabilistic lambda-calculi did not rigorously treat.The calculus includes primitives for continuous random draws and hard and soft constraints.Source: §1.2 · p. 4
  • The paper defines sampling-based and distribution-based semantics and proves their equivalence, alongside equivalence results for their big-step and small-step formulations.Theorem 1 equates the sampling-based formulations, Theorem 2 equates the distribution-based formulations, and Theorem 3 links the two styles.Source: §1.2 · p. 4

1.3 Problem 2: Correctness of Trace MCMC

  • Trace MCMC converges to a stationary distribution whose induced value distribution equals the calculus semantics conditional on successful termination.The proof establishes aperiodicity and irreducibility and applies a classic result of Tierney.Source: §1.3 · p. 5

1.4 Contributions of the Paper

  • The contributions include an untyped calculus capable of encoding core Church, equivalent semantics, and the first trace-MCMC correctness proof for a lambda-calculus.The paper contrasts its untyped approach with prior simply typed work that does not cover recursion or MCMC [35], and with Hur et al., whose work does not establish convergence for the setting considered here.Source: §1.4 · p. 5

1.5 Structure of the Paper

  • The paper proceeds from trace-based sampling semantics to step-indexed distribution semantics, then formalizes trace MCMC and proves its correctness.The sampling-based distribution is obtained by integrating weights over traces; the distribution-based meaning is the supremum of step-indexed semantics.Source: §1.5 · pp. 5–6

2 A Foundational Calculus for Church

The calculus gives probabilistic programs trace-based semantics and translates Church constructs into a foundation for Turing-complete probabilistic languages. Its core examples show how continuous draws, hard and soft constraints, and Church models are represented.

2 A Foundational Calculus for Church

  • Church constructs translate into the calculus, which the paper presents as a foundation for Turing-complete probabilistic languages.The authors demonstrate the translation with probabilistic models, including examples with recursion and continuous distributions.Source: §2 · p. 6, §2.3 · p. 8

2.1 Syntax of the Calculus

  • Terms include continuous-distribution draws, measurable function applications, conditionals, soft-constraint scores, and hard-constraint failure.A distribution identifier is equipped with a density function; score(c) uses a positive probability weight, while fail models a failed hard constraint.Source: §2.1 · p. 6

2.2 Big-step Sampling-based Semantics

  • Evaluation with a finite trace returns a value or failure and a weight, which is a density for continuous distributions.Random-draw rules consume trace elements and use the corresponding density; score sets the weight, while subcomputation weights are multiplied.Source: §2.2 · pp. 7–8

2.3 Encoding Church

  • The Church encoding uses translation rules, a call-by-value fixpoint combinator for recursion, and density functions for distribution identifiers.The translation also permits let and sequencing as syntactic sugar; stochastic memoization is omitted, though the authors say it could be added with state-passing style.Source: §2.3 · pp. 8–9

2.4 Example: Geometric Distribution

  • For the program’s given trace, the final-line if-condition is satisfied, so it reduces to value 2 with weight 1; this is a trace weight, not an outcome probability.Every trace that returns an integer has weight 1; outcome probability comes from an integral over the space of traces.Source: §2.4 · p. 9

2.5 Soft Constraints and score

  • The score primitive implements soft constraints without dummy samples or additional failing traces.For the stated conditioning example, execution continues with weight exp(−(x − c)^2); the authors also note that score admits the possibility of gradient-based inference methods.Source: §2.5 · pp. 9–10

2.6 Example: Linear Regression

  • The linear-regression example models noisy observations with Gaussian priors on slope and intercept, and uses score-based soft equality constraints.When softeq is used only to define positive constraints, it can be implemented with score(squash(x, y)) rather than a flip.Source: §2.6 · p. 10

3 Sampling-Based Operational Semantics

This section develops sampling-based operational semantics in measure-theoretic terms, defining trace-driven outcomes and distributions over program results. It proves the small-step sampling semantics equivalent to the big-step formulation.

3.1 Small-step Sampling-based Semantics

  • For a fixed trace, small-step transitions and multi-step reductions are deterministic in the resulting term, weight, and remaining trace.The one-step and generalized-value determinism results establish unique outcomes for the same initial configuration.Source: §3.1 · p. 12
  • Reduction lifts through evaluation contexts when the result is not failure, while a reduction to failure propagates through any context.The non-failure condition is required for context lifting; failure has a separate propagation result.Source: §3.1 · p. 13
  • Appending unused trace samples preserves reductions, and multiplying the initial weight by a nonnegative factor scales the resulting weight.These properties are established for single-step and multi-step reductions.Source: §3.1 · p. 14
  • Small-step and big-step sampling semantics compute the same traces with the same weights: M ⇓_s w G iff (M, 1, s) ⇒ (G, w, []).The section establishes this equivalence after showing that each small-step transition preserves the big-step semantics.Source: §3.1 · p. 16
  • The small-step semantics evaluates terms against explicit random traces, propagating weights and producing failure when a random transition fails or evaluation reaches fail.The proof passages show trace concatenation for application and assign zero weight to random failure.Source: §3.1 · p. 17

3.2 Some Measure-Theoretic Preliminaries.

  • The measure-theoretic preliminaries provide Borel σ-algebras for metric spaces and define measures, including sub-probability distributions with total mass at most one.These definitions supply the measurable-space and measure framework used for traces and program results.Source: §3.2 · p. 18

3.3 Measure Space of Program Traces

  • Program traces are sequences of real numbers of arbitrary finite length, equipped with a σ-algebra and a σ-finite stock measure built from Lebesgue measures.The empty trace uses a Dirac measure; positive-length traces use Lebesgue measure on the corresponding Euclidean space.Source: §3.3 · pp. 19–20

3.4 Distributions ⟨⟨M⟩⟩and JMKS Given by Sampling-Based Semantics

  • For each closed term, the trace-based outcome and density functions are measurable, and the resulting trace and value semantics are measures.The result distribution over generalized values is obtained by integrating termination density over traces yielding values of interest.Source: §3.4 · p. 21

4 Distribution-Based Operational Semantics

The section develops distribution-based operational semantics for continuous distributions and establishes equivalence between its small-step and big-step formulations. Its small-step account uses sub-probability kernels and step-indexed approximations.

4 Distribution-Based Operational Semantics

  • The small-step and big-step distribution-based semantics define the same result distribution.Their step-indexed families approximate their respective suprema, which Theorem 2 proves equal.Source: §4 · p. 21

4.1 Sub-Probability Kernels

  • Sub-probability kernels assign a sub-probability distribution to each input and measurable probabilities to measurable output sets; composition and products of kernels are also kernels.These kernel properties support the correspondence proof.Source: §4.1 · p. 22

4.2 Approximation Small-Step Semantics

  • One-step reduction is a sub-probability kernel, and every closed term is either a generalized value or has a unique one-step distribution.Source: §4.2 · p. 23
  • At each finite step index, small-step reduction yields a unique distribution, with the index ensuring the continuous-case integral is defined.Term distributions are propagated through evaluation contexts by push-forward.Source: §4.2 · pp. 22, 24, 25

4.3 Approximation Big-Step Semantics

Section 4.3 defines step-indexed big-step approximations for terms and result distributions. Section 4.4 relates the small-step and big-step approximations through monotonicity and application-specific lemmas.

4.3 Approximation Big-Step Semantics

  • The big-step semantics is a step-indexed family of relations between terms and result distributions, inductively defined by the rules in Figure 7.These relations provide approximations indexed by n.Source: §4.3 · p. 25
  • The application rule is the most complex, with three exceptional terms in addition to the normal case.The text explains the rule by replacing general applications with a let construct and applications of values to values.Source: §4.3 · p. 25
  • The inductive comparison is hardest for applications, where composition and product properties of kernels are key ingredients.The existence of the application-rule integral is also established by a lemma analogous to Lemma 30.Source: §4.3 · p. 25

4.4 Beyond Approximations

  • The small-step approximations are monotone in the index: increasing the index yields a distribution at least as large in the pointwise order.For M ⇒n D and m ≥ n with M ⇒m E, Lemma 33 gives E ≥ D.Source: §4.4 · p. 26
  • Application-specific admissibility and inversion lemmas relate the small-step and big-step approximations in both directions.The proof handles application cases using inductive lemmas about evaluating function, argument, and substituted body.Source: §4.4 · pp. 26–28

4.5 Geometric Distribution, Revisited

The geometric-distribution revisit introduces a monotonically increasing index map. The next section proves that integrating the sampling-based semantics over all traces gives the distribution-based semantics.

4.5 Geometric Distribution, Revisited

  • The geometric-distribution revisit introduces a monotonically increasing map f:N→N for its indexed construction.Source: §4.5 · p. 28

4.6 Distribution-based and Sampling-based Semantics are Equivalent

  • The proof of semantic equivalence proceeds through sample traces of bounded length, each equipped with a measure space and a result distribution.The paper defines JMKnS on the trace space Sn for traces of length at most n.Source: §4.6 · p. 28
  • The all-trace integral is the limit of integrals over bounded-length traces.This limit supports the result that the sampling-based and distribution-based semantics are equal.Source: §4.6 · p. 28
  • Deterministic convergence preserves the approximated and full semantics across the distribution-based and sampling-based formulations.The stated preservation covers indexed distributions, indexed sampling semantics, and both full semantics.Source: §4.6 · p. 29

4.7 An Application of the Distribution-Based Semantics

The distribution-based semantics equates the value distributions of hard and soft constraints, and the paper relates rejection sampling to repeated program evaluation. It restricts scores to at most one because recursion with larger scores can yield non-σ-finite return-value measures.

4.7 An Application of the Distribution-Based Semantics

  • The value distributions of score(V) and MV agree, so they can be used interchangeably when only distribution-based behavior on values matters.The paper uses this equation to encode soft constraints with score instead of flip, reducing nuisance parameters for inference.Source: §4.7 · p. 31

4.8 Rejection Sampling

  • Re-evaluating the whole program whenever a Boolean predicate fails yields the same normalized distribution on successful runs, corresponding to rejection sampling.Source: §4.8 · p. 31

4.9 Motivation for 1-Bounded Scores

  • With recursion, scores above one can yield non-σ-finite return-value measures, so the paper restricts scores to positive values bounded by one.The stated alternative is to admit unbounded scores only for programs whose value measures are finite.Source: §4.9 · p. 32

5 Inference

Section 5 defines a trace-based Metropolis–Hastings algorithm for probabilistic programs and proves that its samples converge to the program’s semantics conditioned on success. The proof formalizes the proposal and transition kernels, then establishes the Markov-chain conditions needed for convergence.

5.1 A Metropolis-Hastings Sampling Algorithm

  • The algorithm proposes a new trace from a proposal density, then accepts it with the Hastings probability or retains the current trace.The proposal density is chosen to satisfy conditions used to prove Markov-chain convergence.Source: §5.1 · p. 32

5.2 Proposal Density

  • For each trace, the proposal perturbs its entries with independent Gaussian draws, partially evaluates the program, and assigns density using the draw densities and resulting run weight.If partial evaluation cannot proceed in the specified cases, the proposal density is zero or the proposed trace is empty.Source: §5.2 · p. 33

5.3 A Metropolis-Hastings Proposal Kernel

  • The proposal density is measurable, and integrating it gives a probability kernel after probability is assigned to transitions ending in the empty trace.These properties make the proposal kernel suitable for defining the algorithm’s Markov chain.Source: §5.3 · pp. 33–34

5.4 Transition Kernel of the Markov Chain

  • The transition kernel combines the proposal kernel with the Hastings acceptance probability; the proof assumes positive success probability and rules out deterministic programs.The transition construction is for traces of a fixed program.Source: §5.4 · p. 34

5.5 Correctness of Inference

  • Theorem 4 proves that, from every successful starting trace, the chain’s value distribution converges to the program semantics conditioned on success.The proof establishes irreducibility and aperiodicity before applying a Markov-chain convergence result.Source: §5.5 · pp. 35–36

5.6 Examples

  • For the geometric-distribution example, every valid proposed trace is accepted because its acceptance probability is the indicator that the trace is valid.The Gaussian proposal densities cancel in the acceptance ratio.Source: §5.6 · p. 37
  • In the linear-regression-with-flip example, acceptance requires four trace values to fall within small intervals, which can make proposals inefficient and the chain slowly mixing.The zero gradients for those four components also preclude efficient gradient-based search over them.Source: §5.6 · pp. 37–38
  • For linear regression with score, the acceptance ratio is positive for all proposals, non-zero gradients exist almost everywhere, and there are four fewer nuisance parameters, making inference more tractable in practice.The comparison is with the preceding linear-regression example using flip.Source: §5.6 · p. 38

6 Related Work

The related work spans probabilistic-program semantics and trace-MCMC inference. The authors distinguish their higher-order correctness result from prior justification for imperative trace MCMC and from implementations without formal correctness claims.

Trace MCMC

  • Hur et al. justify trace MCMC for the imperative language R2, but their result does not cover higher-order languages or prove convergence of the resulting chain.Their proof checks that the acceptance ratio matches Hastings’ formula; the paper notes that irreducibility and aperiodicity depend on algorithm parameters.Source: §6 · pp. 38–39
  • Church, Venture [25], WebPPL, and Anglican use trace-MCMC inference, but these works do not state formal correctness claims for their implementations.Source: §6 · p. 39

Trace-based semantics

  • Kozen’s trace semantics and later extensions study measurable probabilistic-program interpretations, while Park et al. do not investigate measure-theoretic properties and Scibior et al. provide no formal inference-correctness results.Source: §6 · p. 39

Probabilistic-language semantics

  • Prior semantics address different language fragments: some treat discrete choice or restricted first-order continuous programs, while others treat continuous distributions without recursion.The paper situates its operational semantics among work on discrete and continuous probabilistic languages.Source: §6 · p. 39

7 Conclusions and Remarks

The paper presents a continuous-distribution probabilistic λ-calculus, semantics for its programs, and a correctness proof for trace MCMC. An F# implementation helped develop and debug the definitions, while more efficient algorithms remain future work.

Conclusions

  • The calculus supports continuous draws and hard and soft constraints, interprets programs as distributions on terms, and provides a foundation for inference in languages such as Church.Source: §7 · p. 40

Implementation

  • The authors report that their F# implementation is correct and effective, but not optimized.They implemented it to develop intuitions and debug definitions.Source: §7 · p. 40

Future work

  • Extending the proofs to cover more efficient algorithms, including approaches inspired by Wingate et al. and Kiselyov, is future work.Source: §7 · p. 40

A Proofs of Measurability

The appendix establishes measurability properties needed for the semantics and inference construction. It builds on a metric-space account of terms and proves bounds for substitution and measurability of expression classes.

A Proofs of Measurability

  • The appendix represents the relevant product σ-algebra through a metric and establishes that the term space is separable and its metric generates the stated σ-algebra.Separability follows from a countable dense subset built using terms with rational constants.Source: A Proofs of Measurability · pp. 40–41
  • The measurability proofs split expression spaces into subspaces by type and use continuity where convenient, rather than decomposing every function into reusable measurable operators.The authors say the overhead of defining and proving many such operators would outweigh their limited reuse.Source: A Proofs of Measurability · pp. 40–41

Detailed definition of substitution

  • Context substitution preserves the metric with equality, while substituting into terms is bounded by the original distance plus the maximum variable multiplicity times the value distance.The latter bound applies to the two terms and substituted values described in Lemma 66.Source: Detailed definition of substitution · p. 42
  • The appendix proves that the listed expression classes, including erroneous redexes and values, are measurable.Source: Detailed definition of substitution · pp. 43–44

A.1 Deterministic reduction as a measurable function

The deterministic redex cases are assembled into a one-step reduction function, and each component is shown measurable. The proof establishes measurability mainly by showing continuity or by composing measurable functions.

A.1 Deterministic reduction as a measurable function

  • Application reduction is measurable because substitution changes the term-space distance by at most a factor determined by variable multiplicity.The bound uses k, the maximum multiplicity of the substituted variable in the two bodies.Source: §A.1 · p. 44
  • Primitive reduction is measurable when each primitive function is measurable, since splitting and recombining a context and redex are measurable.Source: §A.1 · p. 44
  • Conditional branches, failure, and error reductions are measurable; the conditional and error cases are continuous, while failure is constant.Source: §A.1 · p. 45
  • The deterministic one-step function is the union of application, primitive, conditional, failure, and error reductions.Source: §A.1 · p. 45

A.2 Small- step reduction as a measurable function

The small-step transition space is partitioned into value, deterministic, score, and random cases, with a residual set for stuck triples. The transition functions for these cases are measurable.

A.2 Small-step reduction as a measurable function

  • The transition domains for values, deterministic steps, scores, and random steps are measurable, and the remaining non-reducible triples form a measurable stuck set.Source: §A.2 · p. 46
  • Random transitions are measurable by partitioning over the countable set of distributions and using each distribution's measurable probability density.Source: §A.2 · p. 46
  • The random-step function returns the sampled value, updates the weight by multiplying by the distribution density, and removes the consumed trace sample.Source: §A.2 · p. 46
  • The score transition replaces the score expression with true, multiplies the weight by the score, and preserves the trace; this function is measurable.Source: §A.2 · p. 47
  • The one-step function agrees with the reduction relation when a step exists, and every non-failure output corresponds to a reduction step.Source: §A.2 · p. 47

A.3 Measurability of P and O

Step-indexed approximations support the measurability proofs for the output and weight functions. The resulting functions are measurable, and the associated semantics define measures.

A.3 Measurability of P and O

  • A positive limiting weight implies that the state reaches a value with an empty trace; completed reductions determine the corresponding output and weight.Source: §A.3 · p. 48
  • The step-indexed approximations are measurable, and their suprema are measurable using the result for measurable chains into a flat ωCPO.Source: §A.3 · pp. 48–49
  • For every closed term, the output function O_M and weight function P_M are measurable functions of the trace.Source: §A.3 · p. 49
  • The semantics induced by P_M and O_M define measures on traces and outcomes, including the restriction of the outcome measure to values.Source: §A.3 · p. 49

A.4 Measurability of peval

The alternative trace evaluator peval is defined through a measurable one-step function and step-indexed approximations. Its measurability and agreement with reduction-based evaluation are established, alongside its compositional behavior on traces.

A.4 Measurability of peval

  • When reduction consumes a nonempty trace and reaches an empty trace, peval′ returns the resulting term; the converse characterization holds except for failure.Source: §A.4 · pp. 50–51
  • The alternative evaluator peval agrees with peval′, so the trace-based and reduction-based definitions produce the same term.Source: §A.4 · p. 51
  • The alternative evaluator peval is measurable as a function of a closed term and its trace.The proof defines finite approximants using a measurable one-step function; the underlying functional is continuous.Source: §A.4 · pp. 50–52
  • Evaluating a term on a trace and then on another trace equals evaluating it on their concatenation.Source: §A.4 · p. 54

A.5 Measurability of q and Q

The section establishes that the transition density q is measurable for every closed program and that the associated Q is a probability kernel. Its proofs use measurable Gaussian factors and evaluations, then verify the kernel properties.

A.5 Measurability of q and Q

  • For every closed program M, the transition density q(s, t) is measurable on S × S.The proof handles cases according to the lengths of s and t, and treats the empty trace using an integral of q over nonempty traces.Source: §A.5 · p. 58
  • The length-based cases establish measurability through products of Gaussian densities and compositions involving peval, projections, and measurable indicator functions.For the empty-trace case, the proof uses Fubini’s theorem to obtain measurability from the nonempty-trace case.Source: §A.5 · p. 58
  • Q is a probability kernel: Q(s, ·) is a probability distribution, and Q(·, B) is non-negative and measurable for each measurable B.The proof defines Q by integrating q and verifies that Q(s, S) = 1.Source: §A.5 · p. 58
Loading 1512.08990v5…