Prerequisites. Direct starred prerequisites: none. No later core chapter depends on this route.
The source program 𝑒mix=𝖨𝖥𝖱𝖺𝗇𝖽𝗈𝗆(𝖡𝖾𝗋𝗇𝗈𝗎𝗅𝗅𝗂1/3)𝖳𝖧𝖤𝖭𝖱𝖺𝗇𝖽𝗈𝗆(𝖴𝗇𝗂𝖿𝗈𝗋𝗆𝖱𝖾𝖺𝗅⟨0,1⟩)𝖤𝖫𝖲𝖤𝖱𝖺𝗇𝖽𝗈𝗆(𝖴𝗇𝗂𝖿𝗈𝗋𝗆𝖱𝖾𝖺𝗅⟨1,2⟩) denotes a measure on ℝ. An inference backend does not consume measures; it consumes densities, and it will accept the expression 𝑓mix(𝑥)=13[0≤𝑥≤1]+23[1≤𝑥≤2] and evaluate it at whatever points its algorithm visits: 1/3 at 𝑥=1/2, 2/3 at 𝑥=3/2, 0 at 𝑥=−1. Producing 𝑓mix from 𝑒mix is a compilation, and its output is plausible. Plausible is not enough: an inference run reports numbers whatever density it is given, and a wrong density yields a wrong posterior silently.
What must be proved is an equation between two measures: the measure obtained by integrating the generated density against a fixed reference measure equals the measure denoted by the source program. Stating that equation requires a measure semantics for the source language, a notion of density with its side conditions, and a compiler whose output is a syntactic object rather than a mathematical function. The chapter builds the three, proves the soundness of the abstract compiler in its representative cases, records the exact statements of the machine-checked soundness lemmas, and keeps the executable refinement and the simplifier strictly separate from them.
This chapter uses 𝖯𝖬𝖪-map and 𝖯𝖬𝖪-bind of convention 172.27: measurable spaces and maps, subprobability measures, Dirac measures, pushforward, theorem 172.14, products and Tonelli, kernels with bind, lemma 172.19, and the monad laws theorem 172.20. The density interface below is introduced here, where the source-to-target problem forces it; it is not part of 𝖯𝖬𝖪. No quasi-Borel structure and no conditioning result is used.
Let 𝑁 be a measure on a measurable space 𝑋 and let 𝑓:𝑋→[0,∞] be measurable. The measure 𝑓⋅𝑁 is (𝑓⋅𝑁)(𝐴)=∫𝐴𝑓𝑑𝑁. Write hasDensity(𝑀,𝑁,𝑓) for the conjunction of four statements: 𝑀=𝑓⋅𝑁; 𝑀 is a subprobability measure; 𝑓 is measurable; and 𝑓≥0 on 𝑋.
Proof of Lemma 179.3 — f N is a measure, and densities compose with mixtures
Proof. For countable additivity of 𝑓⋅𝑁, let (𝐴𝑛) be disjoint; then 1⋃𝑛𝐴𝑛𝑓=∑𝑛1𝐴𝑛𝑓 pointwise, and monotone convergence applied to the partial sums (convention 172.12) gives ∫⋃𝐴𝑛𝑓𝑑𝑁=∑𝑛∫𝐴𝑛𝑓𝑑𝑁; also ∫∅𝑓𝑑𝑁=0. The two equations are additivity and homogeneity of the integral, applied inside ∫𝐴. ◻
Proof of Lemma 179.4 — Densities are unique almost everywhere
Proof. Let 𝐴={𝑓>𝑔}, measurable. On a set 𝐵⊆𝐴 of finite 𝑁-measure, ∫𝐵(𝑓−𝑔)𝑑𝑁=𝑀(𝐵)−𝑀(𝐵)=0 with a nonnegative integrand, so 𝑁(𝐵∩{𝑓>𝑔})=0; writing 𝐴 as a countable union of such 𝐵 by 𝜎-finiteness gives 𝑁(𝐴)=0. Exchanging 𝑓 and 𝑔 gives 𝑁({𝑔>𝑓})=0. ◻
Lemma 179.4 says that a compiler may not be judged by pointwise comparison against a hand-written density: two correct outputs may differ on a null set, and a fixture that checks values at finitely many points is checking one representative. The acceptance test in this chapter’s project therefore compares a generated syntax tree against a frozen expected tree, and evaluates both at named points; neither comparison is the soundness theorem, which is an equation between measures.
Types are 𝑡::=𝖴𝖭𝖨𝖳∣𝖡𝖮𝖮𝖫∣𝖨𝖭𝖳∣𝖱𝖤𝖠𝖫∣𝑡×𝑡; each type 𝑡 carries a stock measurestock(𝑡): counting measure on 𝖴𝖭𝖨𝖳,𝖡𝖮𝖮𝖫,𝖨𝖭𝖳, Lebesgue measure on 𝖱𝖤𝖠𝖫, and the product measure on a product type. Expressions are 𝑒::=𝖵𝖺𝗅𝑣∣𝖵𝖺𝗋𝑥∣⟨𝑒,𝑒⟩∣op𝑒∣𝖫𝖤𝖳𝑒𝖨𝖭𝑒∣𝖱𝖺𝗇𝖽𝗈𝗆dst𝑒∣𝖨𝖥𝑒𝖳𝖧𝖤𝖭𝑒𝖤𝖫𝖲𝖤𝑒∣𝖥𝖺𝗂𝗅𝑡, with built-in distributions dst among 𝖡𝖾𝗋𝗇𝗈𝗎𝗅𝗅𝗂, 𝖴𝗇𝗂𝖿𝗈𝗋𝗆𝖨𝗇𝗍, 𝖴𝗇𝗂𝖿𝗈𝗋𝗆𝖱𝖾𝖺𝗅, 𝖦𝖺𝗎𝗌𝗌𝗂𝖺𝗇, and others; each has a parameter type, a result type, and a density densdst(𝑝,𝑦) with respect to the stock measure of its result type. An expression is deterministic when it contains neither 𝖱𝖺𝗇𝖽𝗈𝗆 nor 𝖥𝖺𝗂𝗅. Typing Γ⊢𝑒:𝑡 is the evident system. The semantics [[𝑒]]𝜎 of a well-typed 𝑒 in a state 𝜎 is a subprobability measure on stock(𝑡), defined by [[𝖵𝖺𝗅𝑣]]𝜎=𝛿𝑣,[[𝖵𝖺𝗋𝑥]]𝜎=𝛿𝜎(𝑥),[[𝖥𝖺𝗂𝗅𝑡]]𝜎=0,[[𝖫𝖤𝖳𝑒1𝖨𝖭𝑒2]]𝜎=[[𝑒1]]𝜎≫=𝜆𝑣.[[𝑒2]]𝑣∙𝜎,[[𝖱𝖺𝗇𝖽𝗈𝗆dst𝑒]]𝜎=[[𝑒]]𝜎≫=𝜆𝑝.densdst(𝑝,−)⋅stock(𝑡),[[𝖨𝖥𝑏𝖳𝖧𝖤𝖭𝑒1𝖤𝖫𝖲𝖤𝑒2]]𝜎=[[𝑏]]𝜎≫=𝜆𝑣.(𝗂𝖿𝑣𝗍𝗁𝖾𝗇[[𝑒1]]𝜎𝖾𝗅𝗌𝖾[[𝑒2]]𝜎), all binds being those of definition 172.16. This is the frozen source calculus; the compiler below is claimed correct for it and for nothing else.
For 𝑒mix, the scrutinee denotes 13𝛿𝗍𝗍+23𝛿𝖿𝖿 and the two branches denote the uniform measures on [0,1] and on [1,2]. By the 𝖨𝖥 clause and example 172.26, [[𝑒mix]]=13Unif[0,1]+23Unif[1,2], a probability measure. By lemma 179.3 it has the density 𝑓mix of the chapter opening with respect to Lebesgue measure, since Unif[𝑎,𝑏] has density [𝑎≤𝑥≤𝑏]/(𝑏−𝑎) and both intervals have length 1. The compiler must produce a syntactic expression denoting that function, and the soundness theorem must certify the displayed equation rather than the plausibility of the formula.
The abstract compiler derives Δ⊢𝑑𝑒⇒𝑓, read: in the density context Δ=(𝑉,𝑉′,Γ,𝛿), whose random variables are 𝑉, whose parameters are 𝑉′, whose typing is Γ and whose accumulated density is 𝛿, the expression 𝑒 has density 𝑓, a function of the parameter state and the result value. Write bp(Δ) for the total mass accumulated by Δ and 𝑠 for the parameter type of dst. Four of the rules carry the argument:
The rules for variables, pairs, 𝖫𝖤𝖳, and the deterministic operations are those of the source, and the judgment is nondeterministic: an expression may have zero, one, or several derivations.
Branching. If [[𝑒𝑖]]=𝑔𝑖⋅𝑁 for 𝑖=1,2 and the scrutinee denotes 𝑝𝛿𝗍𝗍+(1−𝑝)𝛿𝖿𝖿, and if 𝑔1 already carries the factor 𝑝 and 𝑔2 the factor 1−𝑝, then [[𝖨𝖥𝑏𝖳𝖧𝖤𝖭𝑒1𝖤𝖫𝖲𝖤𝑒2]]=(𝑔1+𝑔2)⋅𝑁.
Sampling with a random parameter. If [[𝑒]]=𝑓⋅stock(𝑠) and dst has density densdst with respect to 𝑁, then [[𝖱𝖺𝗇𝖽𝗈𝗆dst𝑒]]=ℎ⋅𝑁 with ℎ(𝑦)=∫𝑓(𝑥)densdst(𝑥,𝑦)𝑑stock(𝑠)(𝑥).
Proof of Lemma 179.9 — Two representative soundness cases
Proof. (i) By the 𝖨𝖥 clause of convention 179.6 and example 172.26, the left-hand side is 𝑝[[𝑒1]]+(1−𝑝)[[𝑒2]], which by hypothesis is 𝑔1⋅𝑁+𝑔2⋅𝑁, and lemma 179.3 rewrites this as (𝑔1+𝑔2)⋅𝑁.
(ii) Write 𝐷(𝑥)=∫𝐴densdst(𝑥,𝑦)𝑑𝑁(𝑦) and 𝜆=stock(𝑠). For measurable 𝐴, [[𝖱𝖺𝗇𝖽𝗈𝗆dst𝑒]](𝐴)𝑐𝑜𝑛𝑣𝑒𝑛𝑡𝑖𝑜𝑛179.6=∫𝐷(𝑥)𝑑[[𝑒]](𝑥)ℎ𝑦𝑝𝑜𝑡ℎ𝑒𝑠𝑖𝑠𝑜𝑛𝑒=∫𝑓(𝑥)𝐷(𝑥)𝑑𝜆(𝑥)𝑇𝑜𝑛𝑒𝑙𝑙𝑖=∫𝐴(∫𝑓(𝑥)densdst(𝑥,𝑦)𝑑𝜆(𝑥))𝑑𝑁(𝑦)=(ℎ⋅𝑁)(𝐴), the second step by definition 179.2 and the three-stage ascent of theorem 172.14 applied to 𝐷, and the exchange by Tonelli (convention 172.12), whose 𝜎-finiteness hypothesis holds because stock measures are 𝜎-finite and the integrand is nonnegative and jointly measurable. ◻
The following are the machine-checked statements of the Archive of Formal Proofs entry accompanying Eberl–Hölzl–Nipkow, imported at exactly these signatures.
Abstract soundness, expr_has_density_sound: if (∅,∅,Γ,𝜆𝜌.1)⊢𝑑𝑒⇒𝑓, Γ⊢𝑒:𝑡, and 𝑒 has no free variables, then hasDensity([[𝑒]]𝜎,stock(𝑡),𝑓(𝜆𝑥.undefined)). It is proved from a generalized auxiliary lemma expr_has_density_sound_aux, stated for an arbitrary density context satisfying a well-formedness predicate, by induction on the derivation of definition 179.8.
Concrete soundness, expr_has_density_cexpr_sound: if ([],[],Γ,1)⊢𝑐𝑒⇒𝑓, Γ⊢𝑒:𝑡, and 𝑒 is ground, then hasDensity([[𝑒]]𝜎,stock(𝑡),𝜆𝑥.csem(𝑥∙𝜎)(𝑓)), and moreover 𝑓 is a well-typed target expression of type 𝖱𝖤𝖠𝖫 with FV(𝑓)⊆{0}.
Final result, expr_compiles_to_sound: writing 𝑒:𝑡⇒𝑐𝑓 for the conjunction of well-typedness, groundness, and compilation, it states [[𝑒]]𝜎=(𝜆𝑥.csem(𝑥∙𝜎′)(𝑓))⋅stock(𝑡),∀𝑥∈universe(𝑡).csem(𝑥∙𝜎′)(𝑓)≥0, together with Γ⊢𝑒:𝑡, 𝑡∙Γ′⊢𝑐𝑓:𝖱𝖤𝖠𝖫 and FV(𝑓)⊆{0}. This is the chapter’s endpoint and its sole principal system card. Lemma 179.9 proves two of the induction cases at the book’s signature; the import supplies the remaining cases and the refinement.
The judgment of definition 179.8 produces a mathematical function. An implementation must produce a syntax tree, and the passage between them is a separate development with its own invariant.
Target expressions cexpr are built from variables of de Bruijn index, constants, arithmetic and comparison operations, an indicator ⟨𝑏⟩, a conditional 𝖨𝖥𝑐⋅𝖳𝖧𝖤𝖭⋅𝖤𝖫𝖲𝖤⋅, and a bounded integral ∫𝑐𝑒𝜕𝑡; they are typed by Γ⊢𝑐𝑓:𝑡 and evaluated by csem(𝜎)(𝑓). The concrete compiler derives (⃗𝑉,⃗𝑉′,Γ,𝛿)⊢𝑐𝑒⇒𝑓 with the same rule shapes as definition 179.8, replacing every mathematical operation by its syntactic counterpart. The refinement invariant relating the two is: for every derivation of the concrete judgment there is a derivation of the abstract judgment with 𝑓abs(𝜌)(𝑥)=csem(𝑥∙𝜌)(𝑓con), and the concrete result is well-typed of type 𝖱𝖤𝖠𝖫 with free variables among the single result index.
The expression produced by the concrete compiler for example 179.7 is large: it contains integrals over the Boolean parameter, indicator products, and unevaluated constant subexpressions. Simplifying it to 𝑓mix is performed by a separate, separately verified simplifier, and no part of convention 179.10 is a statement about the simplified expression. A fixture that compares only the simplified output therefore tests the composition of two components; the project below compares the unsimplified output against a frozen expected tree first, and only then the simplified one.
Let 𝑒bhat=𝖫𝖤𝖳𝑥=𝖱𝖺𝗇𝖽𝗈𝗆(𝖴𝗇𝗂𝖿𝗈𝗋𝗆𝖱𝖾𝖺𝗅⟨0,1⟩)𝖨𝖭𝖫𝖤𝖳𝑦=𝖱𝖺𝗇𝖽𝗈𝗆(𝖡𝖾𝗋𝗇𝗈𝗎𝗅𝗅𝗂𝑥)𝖨𝖭𝖨𝖥𝑦𝖳𝖧𝖤𝖭𝑥+1𝖤𝖫𝖲𝖤𝑥. Its compiled density, after simplification, is 𝑓bhat(𝑥)=[1≤𝑥≤2]⋅(𝑥−1)+[0≤𝑥≤1]⋅(1−𝑥), with 𝑓bhat(1/2)=1/2, 𝑓bhat(3/2)=1/2, and 𝑓bhat(−1)=0. The value at 3/2 is the density of 𝑥+1 at 3/2, that is the density of 𝑥=1/2 weighted by the probability 𝑥=1/2 of taking the 𝗍𝗍 branch; the value at 1/2 is the density of 𝑥=1/2 weighted by the probability 1−𝑥=1/2 of the 𝖿𝖿 branch. Both weights are the Bernoulli density evaluated at the sampled 𝑥, which is what HD-RandDet inserts.
SlicStan is recorded as a comparison card and as a source of examples. Its shredding transformation, its density semantics, and its conditional-independence results are theorems about a different source language with a different semantics, and none of them is imported here. A translation between the two would require its own semantics-preservation theorem relating the measure semantics of convention 179.6 to SlicStan’s; no such theorem is constructed in this book, so no statement crosses between the two cards.
★☆☆ Verify from definition 179.2 that 𝑓mix is a density for the measure of example 179.7, by computing (𝑓mix⋅Leb)([0,3/2]) and comparing it with the measure of that interval.
★☆☆ Compute [[𝖥𝖺𝗂𝗅𝖱𝖤𝖠𝖫]] and check that HD-Fail produces a density for it. State which clause of hasDensity would fail if the rule produced a positive constant.
★★☆ In the proof of lemma 179.9(ii), replace the stock measure of the parameter type by a measure that is not 𝜎-finite and exhibit a failure of the exchange of integrals. State the hypothesis of convention 172.12 that is violated.
★★☆ Exhibit two syntactically different target expressions that both satisfy convention 179.10 for 𝑒mix, and identify the null set on which they differ. Explain what this implies for a checker that compares generated trees.
★★★Practical project.density-compiler-fixture-runner Implement the abstract compiler of definition 179.8 for the fragment containing 𝖵𝖺𝗅, 𝖵𝖺𝗋, 𝖫𝖤𝖳, 𝖨𝖥, addition of a constant, and 𝖱𝖺𝗇𝖽𝗈𝗆 at 𝖡𝖾𝗋𝗇𝗈𝗎𝗅𝗅𝗂 and 𝖴𝗇𝗂𝖿𝗈𝗋𝗆𝖱𝖾𝖺𝗅, producing a target expression as a syntax tree; then implement, as a separate pass, the simplifier that evaluates constant subexpressions and collapses indicator products.
The invariant to maintain is that the compiler pass never simplifies and the simplifier never compiles: the two outputs are recorded separately, and every numeric constant in both is a reduced rational.
The concrete result is the compiled and simplified density for two programs. The acceptance test is decidable and exact. For the mixture program 𝑒mix of the chapter opening, the unsimplified tree must equal the frozen expected tree recorded with the project, and the simplified tree must equal 𝑓mix, evaluating to 1/3 at 𝑥=1/2, 2/3 at 𝑥=3/2, and 0 at 𝑥=−1. For 𝑒bhat of example 179.13, the simplified tree must equal 𝑓bhat, evaluating to 1/2 at 𝑥=1/2 and at 𝑥=3/2, and 0 at 𝑥=−1. Normalization is never attributed to convention 179.10: the runner prints which comparison used the unsimplified tree and which used the simplified one. A SlicStan example may be displayed for contrast and is not part of the test.