Chapter 176Optional

Probabilistic Program Logics

Prerequisites. Direct starred prerequisites: chapter 174. No later core chapter depends on this route.

Let ${bad}_{1}$ be the program $b \leftarrow coin (1 / 4); return b$ , where $tt$ means failure, and let ${bad}_{2}$ run two independent copies and report whether either failed. Exact enumeration gives $Pr [{bad}_{1}] = \frac{1}{4}, Pr [{bad}_{2}] = 1 - (\frac{3}{4})^{2} = \frac{7}{16} .$ Enumeration also gives the answer for three copies, and for four, and for a program whose two copies are drawn from a continuous distribution it gives nothing at all: the state space is uncountable, and the four cases become an integral.

What survives all these changes is an inequality and the way it was obtained: the probability of a disjunction is at most the sum of the probabilities, so $Pr [{bad}_{2}] \leq Pr [{bad}_{1}] + Pr [{bad}_{1}] = 1 / 2$ . That step used nothing about the value $1 / 4$ , nothing about the number of copies, and nothing about the type of the sampled value. A logic is what remains when such a step is separated from the program it was applied to: judgments that record a bound, rules that compose bounds, and a soundness theorem tying the rules to the measures of chapter 174.

The obstruction that organizes the chapter is that a denotational equality between whole programs, which is what the preceding chapters prove, does not compose with a bound. Knowing $[[e_{1}]] = [[e_{2}]]$ says nothing about $Pr [e_{1} fails]$ , and knowing a bound for a subprogram says nothing about the whole unless there is a rule for the construct that joins them. The chapter builds those rules for a fixed language, proves them sound against the quasi-Borel semantics, and then applies them to three programs whose side conditions are displayed at the point of use.

Convention 176.1 — Imported interface ¶

This chapter uses the quasi-Borel category and its probability monad from chapter 174 — proposition 174.8, proposition 174.10, theorem 174.16, proposition 174.17 — and, through it, the integration and kernel facts $PMK$ -map and $PMK$ -bind of convention 172.27. It does not use the inference transformations of chapter 175.

Referenced from 2 locations

Probabilistic Program Logics

From one bound to a judgment

Definition 176.2 — The programming fragment ¶

Fix the call-by-value fragment $HPProg$ with types $τ : : = 1 ∣ 2 ∣ R ∣ τ \times τ ∣ τ ⟶ τ ∣ M [τ]$ , where $M [τ]$ is the type of distributions over $τ$ ; terms include variables, abstraction, application, pairing, projections, real constants, $coin (p)$ for rational $p \in [0, 1]$ , $return e$ , and $x \leftarrow e_{1}; e_{2}$ . A term of type $M [τ]$ denotes an element of $P [[τ]]$ in the sense of definition 174.12, and a term of a first-order type denotes a point.

Referenced from 4 locations

Probabilistic Program Logics

Definition 176.3 — Assertions ¶

Assertions $φ$ are built from equalities and inequalities between enriched expressions, which extend the terms of definition 176.2 by two families: for $d$ of type $M [τ]$ and a predicate $p$ over $τ$ , $\underset{x \sim d}{Pr} [p (x)]$ of type $R$ , and for $h$ of type $τ ⟶ R$ , $E_{x \sim d} [h (x)]$ of type $R$ . Assertions are closed under $\land$ , $\neg$ , and quantification over a type. Their meaning is the evident predicate on the denotation of the context, with $\underset{x \sim d}{Pr} [p (x)] = \int 1_{p} d [[d]], E_{x \sim d} [h (x)] = \int [[h]] d [[d]],$ both integrals in the sense of definition 174.12.

Referenced from 4 locations

Probabilistic Program Logics

Definition 176.4 — The three judgments ¶

$Γ ∣ Ψ ⊢_{PL} φ$ asserts that $φ$ holds in every environment satisfying the assumptions $Ψ$ . $Γ ∣ Ψ ⊢_{UPL} e : τ ∣ φ$ asserts the same for $φ$ with a distinguished variable $r$ bound to the value of $e$ . $Γ ∣ Ψ ⊢_{RPL} e_{1} : τ_{1} \sim e_{2} : τ_{2} ∣ φ$ asserts it for $φ$ with two distinguished variables $r_{1}, r_{2}$ bound to the values of $e_{1}$ and $e_{2}$ .

Referenced from 4 locations

Probabilistic Program Logics

The unary and relational judgments are notation for the assertion judgment, not separate logics; the following equivalence is the precise form of that claim and is the reason a single soundness theorem suffices.

Proposition 176.5 — Interderivability ¶

$Γ ∣ Ψ ⊢_{UPL} e : τ ∣ φ$ is derivable if and only if $Γ ∣ Ψ ⊢_{PL} φ [e / r]$ is derivable, and $Γ ∣ Ψ ⊢_{RPL} e_{1} : τ_{1} \sim e_{2} : τ_{2} ∣ φ$ is derivable if and only if $Γ ∣ Ψ ⊢_{PL} φ [e_{1} / r_{1}] [e_{2} / r_{2}]$ is.

Referenced from 4 locations

Probabilistic Program Logics

Proof of Proposition 176.5 — Interderivability

Proof. Each unary rule is, by construction, the assertion rule obtained by substituting the subject expression for $r$ ; the derivations are in bijection, and the substitution is meaningful because definition 176.3 allows enriched expressions inside assertions. The relational case substitutes both subjects. This is Sato et al.’s Theorem 6.1 and its relational counterpart Theorem 6.2, at their signatures. ◻

Rules for the fragment, and their soundness

Definition 176.6 — Probabilistic rules ¶

The rules below are stated for the fragment of definition 176.2; every premise is a judgment of definition 176.4 and every side condition is displayed. In Choice, $e_{p}$ abbreviates the biased branch $(b \leftarrow coin (p); if b then e_{1} else e_{0})$ .

Γ ∣ Ψ ⊢_{PL} φ [δ_{e} / r]

Γ ∣ Ψ ⊢_{UPL} return e : M [τ] ∣ φ

Ret

p \in [0, 1] \cap Q

Γ ∣ Ψ ⊢_{UPL} coin (p) : M [2] ∣ \underset{x \sim r}{Pr} [x] = p

Coin

Γ ∣ Ψ ⊢_{UPL} e_{1} : M [τ_{1}] ∣ φ_{1}

Γ, x : τ_{1} ∣ Ψ, φ_{1} [x / r] ⊢_{UPL} e_{2} : M [τ_{2}] ∣ φ_{2}

Γ ∣ Ψ ⊢_{UPL} (x \leftarrow e_{1}; e_{2}) : M [τ_{2}] ∣ \underset{y \sim r}{Pr} [q (y)] \leq sup_{x} \underset{y \sim e_{2}}{Pr} [q (y)]

Bind

Γ ∣ Ψ ⊢_{UPL} e_{0} : M [τ] ∣ \underset{x \sim r}{Pr} [q (x)] \leq a_{0}

Γ ∣ Ψ ⊢_{UPL} e_{1} : M [τ] ∣ \underset{x \sim r}{Pr} [q (x)] \leq a_{1}

Γ ∣ Ψ ⊢_{UPL} e_{p} : M [τ] ∣ \underset{x \sim r}{Pr} [q (x)] \leq p a_{1} + (1 - p) a_{0}

Choice

Γ ∣ Ψ ⊢_{UPL} e : M [τ] ∣ \underset{x \sim r}{Pr} [q_{1} (x)] \leq a_{1}

Γ ∣ Ψ ⊢_{UPL} e : M [τ] ∣ \underset{x \sim r}{Pr} [q_{2} (x)] \leq a_{2}

Γ ∣ Ψ ⊢_{UPL} e : M [τ] ∣ \underset{x \sim r}{Pr} [q_{1} (x) \lor q_{2} (x)] \leq a_{1} + a_{2}

Union

Γ ∣ Ψ ⊢_{UPL} e : τ ∣ φ

Γ, r : τ ∣ Ψ ⊢_{PL} φ \Rightarrow φ^{'}

Γ ∣ Ψ ⊢_{UPL} e : τ ∣ φ^{'}

Weaken

Referenced from 7 locations

Probabilistic Program Logics

Theorem 176.7 — Soundness for the fragment ¶

Every rule of definition 176.6 is sound for the interpretation of definition 176.3: if the denotations of the premises hold in an environment satisfying $Ψ$ , so does the denotation of the conclusion.

Referenced from 6 locations

Probabilistic Program Logics

Proof of Theorem 176.7 — Soundness for the fragment

Proof. Fix an environment satisfying $Ψ$ and write $μ = [[e]]$ for the relevant subject.

Ret. $[[return e]] = δ_{[[e {]]}_{}}$ by definition 174.14, which is what the premise assumes about $r$ .

Coin. $\underset{x \sim coin (p)}{Pr} [x] = \int 1_{{tt}} d (p δ_{tt} + (1 - p) δ_{ff}) = p$ , by lemma 172.13.

Choice. The subject denotes $p [[e_{1}]] + (1 - p) [[e_{0}]]$ by the bind clause and lemma 172.15; integrating $1_{q}$ against a finite mixture is the corresponding combination of the integrals, by example 172.26. The premises bound the two integrals by $a_{1}$ and $a_{0}$ , and the combination is monotone in each, so the conclusion follows.

Union. Pointwise $1_{q_{1} \lor q_{2}} \leq 1_{q_{1}} + 1_{q_{2}}$ , so by monotonicity and additivity of the integral (lemma 172.13, convention 172.12) $Pr [q_{1} \lor q_{2}] \leq Pr [q_{1}] + Pr [q_{2}] \leq a_{1} + a_{2}$ . The two premises are about the same subject $e$ , which is what makes the sum meaningful; nothing about independence is used or needed.

Bind. By lemma 172.19, $\underset{y \sim (x \leftarrow e_{1}; e_{2})}{Pr} [q (y)] = \int \underset{y \sim e_{2}}{Pr} [q (y)] d [[e_{1}]] (x)$ , and an integral of a function bounded by $c$ against a subprobability measure is at most $c$ ; here $c$ is the displayed supremum, which is finite because probabilities are bounded by $1$ . The second premise is what makes $\underset{y \sim e_{2}}{Pr} [q (y)]$ a function of $x$ satisfying the assumption $φ_{1} [x / r]$ at $[[e_{1}]]$ -almost every $x$ .

Weaken. Immediate from the interpretation of implication as inclusion of predicates. ◻

Example 176.8 — The opening bound, derived ¶

Write ${bad}_{2} = (b_{1} \leftarrow coin (1 / 4); b_{2} \leftarrow coin (1 / 4); return (b_{1} \lor b_{2})) .$ By Coin, $Pr [b_{i}] = 1 / 4$ for each copy; by Bind and Weaken each copy contributes $\underset{x \sim r}{Pr} [q_{i} (x)] \leq 1 / 4$ , where $q_{i}$ is the predicate that the $i$ -th draw is $tt$ ; by Union, $\underset{x \sim r}{Pr} [q_{1} \lor q_{2}] \leq 1 / 2$ . The derived bound is $1 / 2$ and the exact value, by enumeration, is $7 / 16$ . The gap is the price of a rule that never mentions independence: the same derivation applies verbatim when the two draws are dependent, and there $7 / 16$ would be false.

Referenced from 5 locations

Probabilistic Program Logics

Convention 176.9 — The Sato et al. semantic core, imported ¶

The general soundness theorem is imported at exactly this signature. Formulas are interpreted as objects of $Pred (QBS)$ , the category of predicates on quasi-Borel spaces, obtained as the change of base of the predicate fibration along the forgetful functor $QBS \to Set$ ; a well-formed formula $Γ ⊢ φ$ denotes a subset of $[[Γ]]$ , with conjunction as intersection, negation as complement, and universal quantification as an intersection over the interpretation of the bound type. Sato et al.’s Theorem 7.4: if $Γ ∣ Ψ ⊢_{PL} φ$ is derivable then $⋂_{ψ \in Ψ} [[Γ ⊢ ψ]] \subseteq [[Γ ⊢ φ]]$ , equivalently the identity on $[[Γ]]$ is a morphism $[[Γ ⊢ \underset{ψ \in Ψ}{⋀} ψ]] \to [[Γ ⊢ φ]]$ in $Pred (QBS)$ . Their Corollary 7.5 and Corollary 7.6 derive the unary and relational statements from it through the interderivability of proposition 176.5. Their proof of the axioms uses the isomorphism $M 1 ≅ [0, \infty]$ , the commutativity of the monad — proved here as proposition 174.17 — the agreement of the monadic integral with Lebesgue integration, and the fact that measurable maps between standard Borel spaces are exactly the quasi-Borel morphisms between them. Theorem 176.7 is the fragment instance proved locally; the import supplies the general case, including the higher-order rules not displayed in definition 176.6.

Referenced from 3 locations

Probabilistic Program Logics

Exercise 176.1 ¶

★☆☆ Derive $Pr [{bad}_{1}] \leq 1 / 4$ with Choice from the two trivial bounds $0$ and $1$ , and compute the resulting arithmetic.

Referenced from 2 locations

Probabilistic Program Logics

Exercise 176.2 ¶

★☆☆ Exhibit a program for which the Union bound is attained exactly, and one for which it exceeds the true probability by $1 / 16$ , as in example 176.8.

Referenced from 2 locations

Probabilistic Program Logics

Exercise 176.3 ¶

★★☆ In Bind, replace the supremum over $x$ by the value at one particular $x$ and exhibit a two-point example where the resulting rule is unsound. State which step of the proof of theorem 176.7 fails.

Referenced from 2 locations

Probabilistic Program Logics

Three applications, with their side conditions

Slicing a probabilistic program

Proposition 176.10 — Removing an unused draw ¶

Let $Γ ⊢ e_{1} : M [τ_{1}]$ and $Γ ⊢ e_{2} : M [τ_{2}]$ , and let $Γ, y : τ_{2} ⊢ e : M [σ]$ with $x$ not free in $e$ . Then $[[x \leftarrow e_{1}; y \leftarrow e_{2}; e]] = [[y \leftarrow e_{2}; e]]$ whenever $[[e_{1}]]$ is a probability measure, that is, of total mass $1$ .

Referenced from 4 locations

Probabilistic Program Logics

Proof of Proposition 176.10 — Removing an unused draw

Proof. By proposition 174.17 the two binds may be exchanged, so the left-hand side equals $[[y \leftarrow e_{2}; x \leftarrow e_{1}; e]]$ . Since $x$ is not free in $e$ , the inner bind is $[[e_{1}]] ≫ = λ x . [[e]]$ with a constant integrand, whose value at a measurable set $A$ is $[[e]] (A) \cdot [[e_{1}]] (whole space) = [[e]] (A)$ by lemma 172.13 and the mass hypothesis. ◻

Remark 176.11 — The hypothesis is not decorative ¶

If $e_{1}$ contains a score, its denotation has mass different from $1$ and the conclusion is false by exactly that factor: with $e_{1} = score (2)$ , the left-hand side is twice the right-hand side. Slicing is therefore a statement about the sublanguage without scoring, or about programs whose sliced part is proved to have unit mass.

Referenced from 2 locations

Probabilistic Program Logics

A sample-size bound for importance sampling

Lemma 176.12 — Markov and Chebyshev ¶

Let $μ$ be a probability measure on $X$ and $f : X \to [0, \infty]$ measurable. Then $μ ({f \geq a}) \leq \frac{1}{a} \int f d μ$ for every $a > 0$ . Consequently, if $g : X \to R$ has mean $m = \int g d μ$ and variance $σ^{2} = \int (g - m)^{2} d μ < \infty$ , then $μ ({| g - m | \geq ε}) \leq σ^{2} / ε^{2}$ for every $ε > 0$ .

Referenced from 4 locations

Probabilistic Program Logics

Proof of Lemma 176.12 — Markov and Chebyshev

Proof. Pointwise $a \cdot 1_{{f \geq a}} \leq f$ , so integrating and using monotonicity and homogeneity (lemma 172.13, convention 172.12) gives $a μ ({f \geq a}) \leq \int f d μ$ . For the second claim apply the first to $f = (g - m)^{2}$ and $a = ε^{2}$ , noting ${| g - m | \geq ε} = {(g - m)^{2} \geq ε^{2}}$ . ◻

Proposition 176.13 — Monte Carlo sample size ¶

Let $d$ be a probability measure, let $h$ be measurable with $μ = E_{x \sim d} [h (x)]$ and $σ^{2} = {Var}_{x \sim d} [h (x)] < \infty$ , and let ${mc}_{n}$ be the program that draws $x_{1}, \dots, x_{n}$ independently from $d$ and returns $\frac{1}{n} \sum_{i} h (x_{i})$ . Then for every $ε > 0$ , $\underset{v \sim {mc}_{n}}{Pr} [| v - μ | \geq ε] \leq \frac{σ^{2}}{n ε^{2}},$ so $n \geq σ^{2} / (δ ε^{2})$ gives the bound $δ$ .

Referenced from 3 locations

Probabilistic Program Logics

Proof of Proposition 176.13 — Monte Carlo sample size

Proof. The denotation of ${mc}_{n}$ is the pushforward of the $n$ -fold product $d^{\otimes n}$ along $λ \vec{x} . \frac{1}{n} \sum_{i} h (x_{i})$ , by lemma 172.22 and proposition 174.17, which permits the $n$ draws to be performed in any order. Its mean is $μ$ , by linearity of the integral and Tonelli, and its variance is $σ^{2} / n$ : expanding $\int (\frac{1}{n} \sum_{i} (h (x_{i}) - μ))^{2} d d^{\otimes n}$ by linearity gives $n$ diagonal terms $σ^{2} / n^{2}$ and $n (n - 1)$ off-diagonal terms, each of which factors by Tonelli into $\frac{1}{n^{2}} (\int (h - μ) d d)^{2} = 0$ . Now apply lemma 176.12 with $g$ the identity on the pushed-forward measure. ◻

Example 176.14 — The bound as a judgment ¶

In the notation of definition 176.4, the proposition is the judgment $\begin{aligned} (E_{x \sim d} [1] = 1), & (σ^{2} = {Var}_{x \sim d} [h (x)]), (μ = E_{x \sim d} [h (x)]), (ε > 0) \\ ⊢_{UPL} {mc}_{n} : M [R] ∣ \underset{v \sim r}{Pr} [| v - μ | \geq ε] \leq \frac{σ^{2}}{n ε^{2}} . \end{aligned}$ The four assumptions are exactly the hypotheses used in the proof: total mass one, finite variance, the value of the mean, and positivity of $ε$ . Dropping the finiteness of $σ^{2}$ makes the right-hand side meaningless; dropping the mass condition makes the mean computation false.

Referenced from 2 locations

Probabilistic Program Logics

Convergence of a mean-learning program

Convention 176.15 — Imported application ¶

The third reconstructed application is Sato et al.’s analysis of Gaussian mean learning, imported at its signature. Let the prior on the unknown mean be normal with mean $m_{0}$ and variance $v_{0}$ , let each observation be normal about the unknown mean with known variance $v$ , and let ${learn}_{n}$ be the program returning the posterior after $n$ observations. Their development derives, in UPL, that the posterior mean after $n$ observations is the stated weighted average of $m_{0}$ and the empirical mean, that the posterior variance is $(1 / v_{0} + n / v)^{- 1}$ , and hence that the posterior variance converges to $0$ at rate $v / n$ ; the stability statement bounds the change in the posterior under a perturbation of one observation by a quantity proportional to $v_{0} / (v_{0} n + v)$ . The hypotheses are that all variances are strictly positive, that the observations are conditionally independent given the mean, and that the prior is proper. Nothing in this chapter proves these; the Lipschitz analysis of generalized value iteration that the source also presents is comparison material and owns no statement here.

Referenced from 2 locations

Probabilistic Program Logics

Remark 176.16 — The mechanization boundary ¶

Two Isabelle developments accompany this material and their coverage is not the same as the paper’s. The Quasi-Borel Spaces entry of the Archive of Formal Proofs mechanizes quasi-Borel spaces, their products, coproducts and exponentials, and the probability monad with its laws — the content of convention 174.19 — and it does not by itself formalize conditioning. The S-Finite Measure Monad entry adds s-finite kernels and a monad supporting scoring, a richer measure interface, and still does not by itself prove every rule of definition 176.6 or the general soundness statement of convention 176.9. When a rule of the logic is said to be checked, the claim is about a named lemma of one of these entries; no claim of machine-checked status is made for the applications of section 176.3. Lilac, a separate logic for independence and conditional probability, is a comparison card: none of its rules or metatheorems is attributed to the logic of this chapter.

Referenced from 2 locations

Probabilistic Program Logics

Exercise 176.4 ¶

★☆☆ Give the two-line calculation showing that proposition 176.10 fails for $e_{1} = score (2)$ , and give the exact factor by which the two sides differ.

Referenced from 2 locations

Probabilistic Program Logics

Exercise 176.5 ¶

★★☆ Exhibit a distribution and an $ε$ for which the Chebyshev bound of lemma 176.12 is attained with equality, and one for which it overestimates by a factor of $100$ .

Referenced from 2 locations

Probabilistic Program Logics

Exercise 176.6 ¶

★★☆ Carry out in full the variance computation in the proof of proposition 176.13 for $n = 2$ , displaying the diagonal and off-diagonal terms and the use of Tonelli.

Referenced from 2 locations

Probabilistic Program Logics

Suggested first pass.

None of these problems is a prerequisite for a later chapter. Begin with exercise 176.7, then exercise 176.8, then the practical project exercise 176.11.

Exercise 176.7 ¶

★☆☆ Enumerate ${bad}_{2}$ exactly, confirm $Pr [{bad}_{2}] = 7 / 16$ , and compare it with the derived bound $1 / 2$ of example 176.8.

Referenced from 3 locations

Probabilistic Program Logics

Exercise 176.8 ¶

★★☆ Write out the Bind case of theorem 176.7 for the special case where $e_{1}$ is $coin (p)$ , replacing the integral by a two-term sum, and identify the exact inequality that the supremum supplies.

Referenced from 3 locations

Probabilistic Program Logics

Exercise 176.9 ¶

★★☆ Using proposition 176.5, translate the slicing statement of proposition 176.10 into an RPL judgment, and state the assumptions $Ψ$ it requires.

Referenced from 2 locations

Probabilistic Program Logics

Exercise 176.10 ¶

★★☆ Generalize example 176.8 to $k$ independent copies: derive the bound $k / 4$ by Union, compute the exact probability $1 - (3 / 4)^{k}$ , and determine the least $k$ for which the derived bound exceeds $1$ while the exact probability does not.

Referenced from 2 locations

Probabilistic Program Logics

Exercise 176.11 ¶

★★★ Practical project.finite-bound-certificate-checker Build a certificate checker for the finite fragment. A certificate is one of $ret$ , $bind (c_{1}, c_{2})$ , $choice (p, c_{0}, c_{1})$ , $weaken (q, q^{'}, c)$ , and $union (c_{1}, c_{2})$ , where every probability is a reduced rational; the checker computes the claimed bound bottom-up according to definition 176.6 and compares it with the requested bound using integer arithmetic only. A second component enumerates the program exactly and reports its true probability.

The invariant to maintain is that no floating-point number appears anywhere and that a certificate is accepted only when every side condition of the corresponding rule is checked, including the requirement in Union that both premises concern the same subject program.

The concrete result is the pair of verdicts and the exact probability for the two programs of the chapter opening. The acceptance test is decidable and exact: the checker must accept $Pr [{bad}_{1}] \leq 1 / 4$ by $choice$ ; accept $Pr [{bad}_{2}] \leq 1 / 2$ by $union$ ; reject the same ${bad}_{2}$ certificate at the bound $1 / 4$ , reporting the derived bound $1 / 2$ and the requested bound $1 / 4$ ; and the enumerator must report $Pr [{bad}_{2}] = 7 / 16$ exactly. Successful checking is the oracle. The certificate language is a finite executable shadow of the logic of definition 176.6; its general soundness is theorem 176.7, which the checker does not prove.

Referenced from 3 locations