PaperlayerView exact revision on arXiv

Source-linked AI summary

Bayes Rule for Conditioning Probabilistic Programs

Feras A. Saad

arXiv:2610.10792v1cs.PLcs.LO

TL;DR

A rigorous statistical account of conditioning on zero-probability observations is needed because soft conditioning can conflict with statistical theory for mixed-type variables and observations in conditional branches. The paper develops a disintegration-based semantics with an explicit Bayes rule, proving a theorem for a large family of models and strong consistency of likelihood weighting under stated conditions.

  • Problem

    A rigorous statistical account of conditioning on zero-probability observations is needed because soft conditioning can conflict with statistical theory for mixed-type variables and observations in conditional branches.

    Source: §1 · p. 1, §1.1 · p. 2

  • Method

    The paper models traces and observations as measurable spaces linked by an observation map, then uses disintegration to construct a conditional semantics with an explicit Bayes rule.

    Source: §1.4 · p. 5, §4 · p. 15

  • Results

    For bounded measurable f and observations with 0 < p_Z(z) < ∞, likelihood weighting is strongly consistent for the conditional expectation, and the paper proves a disintegration theorem for a large family of models.

    Source: §1.4 · p. 5, §7.4 · p. 23

  • Takeaways & Limitations

    The explicit Bayes rule can be used by inference algorithms, connecting the measure-theoretic construction to computational inference.

    Source: §1.4 · p. 5

    The article establishes a measure-theoretic foundation rather than a language implementation, and complex fibers lack a default proposal strategy.

    Source: §1.4 · p. 4, §8 · p. 24

Abstract

from arXiv · show

Probabilistic programs provide a rigorous programming-language foundation for expressing rich probabilistic models and offer language-level support for solving challenging statistical inference problems. A key theoretical challenge that probabilistic programs inherit from probability theory is conditioning a probability distribution on an observation that has probability zero. Many languages address this challenge by using computational rules for conditioning that may work well for some problems but are statistically unsound for others. This article introduces a principled mathematical approach for conditioning probabilistic programs. We first show that existing techniques based on "soft conditioning" and "neighborhood limits" exhibit semantic issues from the perspective of measure theory and produce inference results that disagree with sound statistical reasoning. By leveraging tools from geometric measure theory, we construct a novel disintegration-based semantics for probabilistic program traces that enables sound conditioning. The theory delivers an explicit Bayes rule representation of the conditional distribution, which is directly compatible with widely used probabilistic inference algorithms that require access to unnormalized posterior densities. Our Bayes rule handles probabilistic models with loops, branches, discrete, continuous, and mixed-type distributions, observations on manifolds, differentiable structure, and additional modeling motifs that arise in practice.

1 Introduction

The section frames zero-probability observations as a central conditioning challenge: density-based and neighborhood-limit rules can depart from statistical semantics, motivating a disintegration-based foundation.

1 Introduction

  • Continuous observations have probability zero, yet probabilistic languages use conditioning rules that can lack a reasonable statistical interpretation and yield unsound inference.For discrete observations, the usual Bayes rule applies when the observation has positive probability; continuous observations instead have probability zero.Source: §1 · p. 1

1.1 Conditioning Probabilistic Programs using Probability Densities

  • Density-based soft conditioning fails for exact, mixed-type, and branch-local observations, so its semantics is statistically sound only in a restricted language fragment.For the example of conditioning a normal variable on its square, the density-based rule assigns atom probabilities that sum to four.Source: §1.1 · p. 2

1.2 Conditioning Probabilistic Programs via Neighborhood Limits

  • Neighborhood limits can have a rigorous statistical interpretation when null events arise from one statistic, but generally their pointwise conditional probabilities do not form a coherent posterior distribution.The limiting result can depend on the chosen family of positive-probability neighborhoods.Source: §1.2 · p. 3

1.3 Conditioning Probabilistic Programs via Disintegration

  • Disintegration factors the prior through the observation distribution using conditional laws; values at null observations remain undetermined, while statistical meaning concerns random observations.This provides a coherent semantics for inference procedures using a fixed statistic Z=t(X).Source: §1.3 · pp. 3–4

1.4 This Work: A Measure-Theoretic Foundation for Conditioning by Disintegration

  • A disintegration theorem gives an explicit Bayes rule for broad probabilistic models, and likelihood weighting is proved strongly consistent for bounded measurable functions when pZ(z) is finite and positive.The framework covers loops, branches, discrete, continuous, and mixed-type variables, as well as manifold-supported and mixed-dimensional variables.Source: §1.4 · pp. 4–5
  • The article establishes a mathematical foundation rather than building a language implementation.Its focus is measure-theoretic rather than language-design aspects.Source: §1.4 · p. 4

2 Conditioning Probabilistic Programs using Probability Densities

The section introduces soft conditioning, a common way to express inference in probabilistic programs, and explains why its density semantics do not generally equal statistical conditioning. The resulting unnormalized densities remain useful to inference algorithms, but interpreting them as posterior densities can yield undefined or statistically incoherent results.

2 Conditioning Probabilistic Programs using Probability Densities

  • Soft conditioning uses sample and observe constructs to represent probabilistic models and observations; the paper restricts attention to programs that halt almost surely, though they may have infinitely many control-flow paths.A sample draws from a distribution, while observe records a measurement of a draw.Source: §2 · p. 5

2.1 Semantics of Straight-Line Programs

  • A straight-line program’s density weights sampled traces by observation densities, using product base measures that are Lebesgue for continuous variables and counting measure for discrete variables.The density is defined when its normalizing constant is finite and positive.Source: §2.1 · pp. 5–6

2.2 Inference with Densities

  • Approximate inference algorithms can use the unnormalized density, including likelihood weighting, MCMC, sequential Monte Carlo, and variational inference, without knowing the normalizing constant.Likelihood weighting samples from the prior and weights each trace by the observe densities.Source: §2.2 · p. 6

2.3 Soft Conditioning and Statistical Inference in Generative Models

  • Soft-conditioning semantics can depend on arbitrary density values at null sets, leaving some programs without meaningful conditional distributions and producing inferences that disagree with statistical theory.The section presents the target as an unnormalized density, not intrinsically as statistical conditioning.Source: §2.3 · p. 6

2.4 Failure to Denote a Conditional Distribution

The examples show that density semantics can fail to denote a meaningful conditional distribution, either through an infinite normalizer or through dependence on arbitrary choices at probability-zero observations. Exact conditions pose a distinct problem: ordinary sample-and-observe constructs may assign them zero weight despite a statistically well-defined posterior.

2.4 Failure to Denote a Conditional Distribution

  • For the gamma-normal program, the normalizing constant is infinite because the inner integral is infinite for every u in (0, 0.5], a set of positive uniform-prior measure.The density semantics therefore does not define a distribution for the intended posterior.Source: §2.4 · p. 7, Figure 2 · p. 7

2.4.2 Scoring with Arbitrary Values.

  • Equivalent score and observe formulations can imply different generative stories, so the program text alone cannot determine the statistical inference problem.Density values at null sets are underdetermined, and changing the density representative can change the normalizing constant.Source: §2.4 · p. 7, §2.4.2 · p. 8

2.4.3 Exact Conditions.

  • For the exact condition 2X−Y=z, the posterior is statistically supported on a line segment, but sample-and-observe with a Bernoulli indicator gives the observation weight zero almost surely.The joint distribution is singular with respect to three-dimensional Lebesgue measure, and the elementary Bayes rule’s domination assumption does not hold.Source: §2.4.3 · p. 8

2.5 Incorrect Statistical Inferences

The section shows that density semantics can produce incorrect inferences when different control-flow paths involve different types or numbers of observations. Correct comparisons require a shared base measure across paths; neighborhood limits expose examples where density-based calculations disagree with statistical conditioning.

2.5.1 Semantics of Programs with Control Flow.

  • With control flow, a program’s execution paths are represented as straight-line programs constrained by the guards that determine which path runs.A correct base measure for observations may require information about their distributions across all paths.Source: §2.5.1 · p. 9, §2.5.2 · p. 10

2.5.2 Mixed-Type Distributions.

  • The density semantics assigns posterior probability 1/3 to X=1 in the mixed-type example, while statistical theory assigns it probability one because the observation is a probability mass rather than a density.The paths use different base measures, so the pathwise densities do not form a valid Bayes rule.Source: §2.5.2 · pp. 9–10

2.5.3 Continuous Observations Along Different Paths.

  • In the continuous-observation example, neighborhood probabilities scale as ε² on one branch and ε on the other, leaving only the X=1 branch with posterior probability one in the limit.More generally, these neighborhood limits retain paths with the fewest continuous observations.Source: §2.5.3 · p. 10

2.5 Incorrect Statistical Inferences

  • The density semantics is best understood as an unnormalized measure whose total mass sums prior path probabilities times expected observation scores, not generally as a conditional probability density.Interpreting it as a conditional density can yield results that disagree with statistical theory.Source: §2.5.3 · p. 10

3 Conditioning Probabilistic Programs Using Neighborhood Limits

Neighborhood limits approximate conditioning on a null event through positive-probability events, but the result depends on the chosen neighborhoods. The section shows that these limits generally fail to define coherent conditional distributions and that bare null events may not specify a meaningful statistical inference problem.

3.1 Theory of Conditional Probability via Neighborhood Limits

  • A neighborhood-limit conditional probability is defined by taking limits over positive-probability events, but its value depends on the chosen sequence of neighborhoods.The practitioner must specify the neighborhoods converging to the null event.Source: §3.1 · p. 11

3.1.1 Limits Do Not Give Conditional Probability Distributions.

  • For decreasing positive-probability neighborhoods of a null event, the limit rule does not define a probability measure and yields isolated values without a coherent conditional distribution.Proposition 3.1 rules out a measure satisfying the proposed limit for all events.Source: §3.1.1 · pp. 11–12

3.1.2 Conditional Probability Given a Sigma-Algebra.

  • Conditional probabilities given a sigma-algebra are unique only up to null sets, so program semantics must not depend on their unconstrained values there.Regular conditional probabilities combine individual conditional probabilities into a probability measure almost surely.Source: §3.1.2 · p. 12

3.1.3 The Sigma-Algebra Structure of a Neighborhood.

  • The sigma-algebra generated by nested neighborhoods leaves conditional values on the limiting null event arbitrary, so neighborhood-limit semantics depend on an undetermined choice.The generated structure determines arbitrary constants that the neighborhoods alone cannot fix.Source: §3.1.3 · p. 12

3.2 Revisiting the “Type 1” Paradox

  • In the Type 1 example, soft conditioning exhibits unit anomalies, while interpreting branch-specific observations as conditioning on a bare null event raises a deeper semantic problem.Jacobs’ example uses different noisy observations in different control-flow branches.Source: §3.2 · p. 13

3.2.1 Bare Null Events as Observations.

  • Because no unified statistic encodes the branch-specific event family, the program cannot state consistency properties as its observation constants change.The individual event encodings depend on the particular observation value.Source: §3.2.1 · pp. 13–14
  • The event family for different observation values generally cannot be represented as conditioning one fixed random variable on corresponding values.Proposition 3.2 establishes this for the two-branch height-and-weight observations.Source: §3.2.1 · pp. 13–14

3.2.2 Ambiguity of Null Set Conditioning.

  • A bare null event needs additional structure to specify inference, yet representing it through an indicator leaves the target null fiber unconstrained.For the indicator encoding, the regular conditional distribution at zero is the prior, while the value at the event of interest is unconstrained; neighborhood shrinkage rates can also affect branch probabilities.Source: §3.2.2 · p. 14

4 Disintegration Theory

Disintegration formalizes conditioning through a measurable observation map, expressing conditional distributions on the map’s fibers. Under suitable base-measure assumptions, the paper gives this conditional law an explicit generalized Bayes-rule density representation.

4 Disintegration Theory

  • Disintegration models traces as a probability measure and observations as a measurable map, with the conditional distribution supported on the corresponding fiber.The observation’s marginal is the pushforward of the trace measure.Source: §4 · p. 15
  • A disintegration induces a regular conditional distribution given the sigma-algebra generated by the observation map.For standard Borel spaces, disintegrations exist and their versions agree almost surely under the observation marginal.Source: §4 · p. 15

4.1 Generalized Bayes Rule

  • Theorem 4.2 represents the disintegration with a generalized Bayes rule when the trace measure has a density and compatible sigma-finite base measures and transition kernels exist.The representation provides densities for both the observation marginal and the conditional trace distribution.Source: §4.1 · p. 16

5 A Probabilistic Language with Observation Maps

The proposed language makes observations explicit through return values and uses disintegration to define conditioning across program paths. Its primitive distributions cover discrete and Lebesgue-density continuous cases, with singular continuous distributions represented through lower-dimensional coordinates.

5 A Probabilistic Language with Observation Maps

  • The language replaces inline observations with a return value that defines the observation map and an observe statement that fixes its value.Semantics rely on the disintegration property rather than specific observation constants, for almost every random data vector in the prior support.Source: §5 · p. 16
  • The semantics first construct a local disintegration for each program path, then combine those local objects into a global disintegration across paths.The global construction must identify measure-theoretic structure satisfying the generalized Bayes-rule theorem’s hypotheses.Source: §5 · pp. 16–17

5.1 Primitive Probability Distributions

  • Primitive distributions use counting measure for discrete carriers and Lebesgue measure for Euclidean continuous carriers, with jointly measurable densities.The primitives distinguish discrete and continuous distribution families.Source: §5.1 · p. 17
  • The semantics omit standalone continuous primitives singular to Lebesgue measure, but such distributions can be implemented through lower-dimensional coordinate parametrizations.A uniform distribution on a circle is given as an example of this representation.Source: §5.1 · p. 17

6 Disintegration within a Single Probabilistic Program Path

For a single program path, the paper constructs a disintegration by modeling mixed discrete and continuous traces, restricting them to path guards, and mapping them to observations. A coarea-based construction yields a density representation on the observation fiber that supports comparisons and standard inference algorithms.

6.1 Measure Structure

  • A path’s trace space is built from its ordered sample sites, with a density formed from the distributions encountered along execution.The path trace separates discrete and continuous sample coordinates.Source: §6.1 · pp. 17–18

6.2 Incorporating Path Guards

  • Path guards restrict the unconstrained trace space to path-compatible traces, yielding a subprobability measure; zero-measure paths can be ignored.The path’s guard values determine the restriction.Source: §6.2 · p. 18

6.3 Observation Map

  • Each path’s return expression defines a measurable observation map, with continuous coordinates subject to a C1 constant-rank assumption that can be handled by stratification when needed.A path returns a real vector of fixed length, though other paths may return vectors of different lengths.Source: §6.3 · pp. 18–19

6.4 Local Disintegration

  • The local disintegration uses the coarea formula and a Hausdorff-measure observation base, then sums over discrete coordinates.The resulting base measure is shown to be sigma-finite.Source: §6.4 · pp. 19–20
  • Moving the Jacobian factor into the density gives a unified representation for comparing points on an observation fiber, compatible with importance sampling and MCMC.The representation uses an unweighted geometric reference measure.Source: §6.4 · p. 20

7 Disintegration of Full Probabilistic Programs

The section builds a global disintegration for traces across program paths, yielding a posterior density and Bayes rule. Its observation-space measure aligns path contributions by rank, while the projection-observation case supports a consistency result for likelihood weighting.

7.1 Observation Base Measure

  • A sigma-finite observation base measure counts raw observation values once, using strata defined by output dimension and observation rank.It is built from Hausdorff measures restricted to rank-stratified sets.Source: §7.1 · pp. 20–21

7.2 Unifying the Pathwise Base Measures

  • Only paths of minimal observation rank contribute at an observation, allowing their pathwise measures to be compared through the global base measure.The construction uses a change of measure to identify the global disintegration.Source: §7.2 · p. 21

7 Disintegration of Full Probabilistic Programs

  • The global trace measure disintegrates through a shared observation-space measure, furnishing a posterior density that inference algorithms can use.The construction combines pathwise objects into a global disintegration.Source: §7 · p. 20, §7.2 · p. 21

7.3 Relationship to Neighborhood Limits

  • Neighborhood limits are sound when derived from a coherent observation map, whereas branch-dependent neighborhoods can introduce arbitrary scale factors.The global map and shared base measure compare all paths through the same observation-space derivative.Source: §7.3 · p. 22

7.4 Projection Observations and Likelihood Weighting

  • For projection observations, likelihood weighting is strongly consistent for bounded measurable functions when the observation density is positive and finite.The method estimates the unknown observation rank from samples and eventually restricts weighting to minimal-rank paths.Source: §7.4 · pp. 22–23

8 Language Design Considerations

The theory is not supported in full generality by existing probabilistic programming languages, and implementation choices involve tradeoffs among expressiveness, runtime performance, and static verification. Practical systems may need structured guards, path stratification, derivative information, and strategies for exploring posterior fibers.

Language Design Considerations

  • No existing probabilistic programming language is known to support the full geometric conditioning semantics, and implementations may trade expressiveness against runtime performance and static verification.The theory identifies implementation considerations for inference algorithms that use its Bayes rule.Source: §8 · p. 23
  • Although the theory permits arbitrary positive-measure guard domains, implementations may restrict guards to structured classes to make path analysis and inference tractable.Piecewise-analytic-under-analytic-partition functions are given as an example.Source: §8 · p. 23
  • Constant-rank observation maps may require explicit branch stratification, while practical Jacobian computation requires typing discrete and continuous coordinates for differentiation.The example x ↦ x² has rank zero at zero and rank one elsewhere; automatic differentiation may compute the Jacobian once coordinates are typed.Source: §8 · pp. 23–24
  • Posterior samples must lie on the observation fiber; projections permit prior-based importance sampling, but general fibers may require user guidance or specialized inference methods.The text lists constraint solvers, fiber reparameterizations, and programmable inference kernels as possible supports.Source: §8 · p. 24
  • Computing observation ranks may use known model structure in restricted languages, but more flexible languages may need program analysis and statistical estimation.Source: §8 · p. 24

9 Related Work

The related work contrasts the paper’s trace-level disintegration with geometric density methods, existing probabilistic programming systems, and alternative semantic frameworks. Its distinctions center on countable paths, overlapping path images, noninjective observation maps, and explicit posterior kernels.

9.1 Geometric Densities and Base Measures

  • Unlike fixed-manifold sampling, the theory disintegrates entire probabilistic program traces, including countably many paths, mixed distributions, overlapping path images, and a global sigma-finite base measure.The base measure supports a Bayes rule over program traces.Source: §9.1 · p. 24
  • Positive-measure overlaps between same-rank path images retain uncertainty about the generating path, while each observation value is measured once.The construction retains every minimal-rank path that can produce the observation.Source: §9.1 · p. 25
  • The theory handles noninjective constant-rank maps, including maps with multiple preimages or positive-dimensional fibers, using a coarea formula with a Jacobian correction.Source: §9.1 · p. 25

9.2 Probabilistic Programming Systems with Disintegration

  • Hakaru systems produce disintegrations through semantics-preserving transformations, while other systems address restricted settings such as projection observations or Bayesian and sum-product networks.The paper supplies a measure-theoretic foundation and handles modeling constructs outside several existing solver-based implementations.Source: §9.2 · p. 25

9.3 Language Semantics and Disintegration

  • The work complements higher-order categorical semantics and differs from operator-based conditioning by constructing explicit posterior kernels and densities for path-indexed traces.It uses a sigma-finite observation base measure because an s-finite one may not support the standard densities needed for its Bayes rule.Source: §9.3 · p. 25

A Technical Lemmas

The appendix records measure-space notation and establishes geometric facts used in the paper’s construction, including rectifiability of constant-rank images and a coarea-based integration result.

A Technical Lemmas

  • For a countable family of measure spaces, the appendix defines product and coproduct constructions, including a probability-mass condition for infinite products.The coproduct may be tagged unless its component sets are disjoint.Source: A Technical Lemmas · p. 28
  • A C1 map with constant rank m on an open domain has a Borel, countably m-rectifiable image.The proof uses local constant-rank neighborhoods and a countable cover.Source: A Technical Lemmas · pp. 28–29
  • For a restriction of a C1 constant-rank map to a measurable set, the coarea formula integrates over fibers using the Jacobian defined from nonzero singular values.The appendix establishes the result by applying coarea on a countable decomposition.Source: A Technical Lemmas · p. 29

B Deferred Proofs

The deferred results establish how disintegration yields conditional distributions for probabilistic program traces and characterize the associated base measures. They also prove strong consistency of likelihood weighting under stated conditions.

B Deferred Proofs

  • A disintegration μX|Z induces a regular conditional distribution given the sigma algebra generated by t.The conditional distribution is obtained by evaluating μX|Z(· | t(x)).Source: B Deferred Proofs · p. 30
  • For λZ-almost every observation, the transition kernel is uniformly σ-finite, and the marginal μZ is absolutely continuous with respect to λZ.The passage states that μZ has a density with respect to λZ.Source: B Deferred Proofs · p. 30
  • For each observation z, the conditional distribution μX|Z(· | z) is absolutely continuous with respect to the conditional base measure λX|Z(· | z).The theorem states that this conditional distribution has a density.Source: B Deferred Proofs · p. 30
  • The prior base measure λX disintegrates through λZ, with the trace-space construction handling program paths and their observation fibers.The path-specific events Bπ are defined by restricting an event B to path π.Source: B Deferred Proofs · p. 33
  • Likelihood weighting is strongly consistent for expectations of bounded measurable functions at observations where pZ(z) is finite and positive.The guarantee concerns the posterior μX|Z(· | z).Source: B Deferred Proofs · p. 33

C Singular Primitive Distributions

The formalism restricts primitive distributions to discrete or Lebesgue-absolutely-continuous cases. Extending it to primitives supported on lower-dimensional manifolds would require additional measure and geometric structure.

C Singular Primitive Distributions

  • Primitive distributions are restricted to discrete distributions or distributions absolutely continuous with respect to Lebesgue measure.This excludes singular primitives such as distributions supported on a parameterized circle.Source: C Singular Primitive Distributions · p. 35
  • Manifold-supported primitives also require tangent-space information to compute the appropriate coarea Jacobian.For non-manifold rectifiable supports, the tangent space and derivative must be replaced by their approximate counterparts.Source: C Singular Primitive Distributions · pp. 35–36
  • A lower-dimensional manifold support may prevent a unified σ-finite base measure, making densities across parameter values incomparable.For uniform distributions on circles of varying radii, a common dominating measure would assign positive measure to uncountably many disjoint circles.Source: C Singular Primitive Distributions · p. 35
  • The paper identifies fixed support with parameter-varying densities, or intrinsic-coordinate sampling followed by embedding, as alternatives for handling manifold primitives.The current assumption avoids these added geometric complexities.Source: C Singular Primitive Distributions · pp. 35–36
Loading 2610.10792v1…