Worked examples: HAVING provenance and probability on a three-occurrence group

Two fully computed examples on a group with three occurrences.

• SUM(a) ≥ 5 collapse in 𝔹[X]. With attribute values a = (3, 2, 2) and annotations the distinct variables x₁, x₂, x₃, the valid non-empty worlds are {1,2}, {1,3} and {1,2,3}, and the possible-world provenance sums their world annotations. Since 𝔹[X] is absorptive, this collapses to the ⊕-sum over the two minimal valid worlds {1,2} and {1,3} alone (the general statement is Having.sum_ge_collapse); both sides compute – by kernel evaluation on all 2³ valuations – to x₁ ∧ (x₂ ∨ x₃).

• Poisson-binomial COUNT(*) ≥ 2. With independent contributors of marginals p₁ = 1/2, p₂ = 1/4, p₃ = 1/3, the point masses computed by the recurrence (HavingProbability.countMass_insert_zero / countMass_insert_succ) are ρ₃(2) = 1/4 and ρ₃(3) = 1/24, and the CDF assembly (HavingProbability.funcProb_count_filter) gives Pr[COUNT(*) ≥ 2] = 1/4 + 1/24 = 7/24.

The SUM(a) ≥ 5 collapse in 𝔹[X]

def HavingExample.t : Fin 3 → ℕ

Attribute values of the three occurrences: a(u₁) = 3, a(u₂) = a(u₃) = 2.

Equations

• HavingExample.t i = if ↑i = 0 then 3 else 2

def HavingExample.α : Fin 3 → BoolFunc (Fin 3)

Annotations: the distinct Boolean variables x₁, x₂, x₃ of 𝔹[X].

Equations

• HavingExample.α = BoolFunc.var

theorem HavingExample.sum_ge_five_prov : ∑ W ∈ Finset.univ.powerset with 5 ≤ ∑ i ∈ W, t i, Having.T α Finset.univ W = BoolFunc.var 0 * (BoolFunc.var 1 + BoolFunc.var 2)

Possible-world provenance of SUM(a) ≥ 5: the ⊕-sum of the world annotations T_U(W) over the valid worlds {1,2}, {1,3}, {1,2,3} computes to x₁ ∧ (x₂ ∨ x₃).

theorem HavingExample.sum_ge_five_minimal : ∑ V ∈ {W ∈ Finset.univ.powerset | 5 ≤ ∑ i ∈ W, t i} with ∀ V' ⊂ V, ¬5 ≤ ∑ i ∈ V', t i, Having.A α V = BoolFunc.var 0 * (BoolFunc.var 1 + BoolFunc.var 2)

Collapse to minimal worlds: the ⊕-sum of the monomials A_V over the two minimal valid worlds {1,2} and {1,3} computes to the same x₁ ∧ (x₂ ∨ x₃), as predicted by Having.sum_ge_collapse since 𝔹[X] is absorptive.

The Poisson-binomial COUNT(*) ≥ 2 example

def HavingExample.P : ProbAssignment (Fin 3)

Independent contributor marginals p₁ = 1/2, p₂ = 1/4, p₃ = 1/3.

Equations

• HavingExample.P = { prob := fun (i : Fin 3) => if ↑i = 0 then 1 / 2 else if ↑i = 1 then 1 / 4 else 1 / 3, prob_nonneg := HavingExample.P._proof_1, prob_le_one := HavingExample.P._proof_2 }

def HavingExample.S : Fin 3 → Finset (Fin 3)

Per-contributor variable supports: contributor i depends on xᵢ only.

Equations

• HavingExample.S i = {i}

theorem HavingExample.hdep (i : Fin 3) : (α i).DependsOn (S i)

theorem HavingExample.hdisj : Set.univ.Pairwise fun (i j : Fin 3) => Disjoint (S i) (S j)

theorem HavingExample.funcProb_α (i : Fin 3) : P.funcProb (α i) = P.prob i

theorem HavingExample.prob_0 : P.prob 0 = 1 / 2

theorem HavingExample.prob_1 : P.prob 1 = 1 / 4

theorem HavingExample.prob_2 : P.prob 2 = 1 / 3

theorem HavingExample.mass_empty_zero : P.funcProb (HavingProbability.countEqIndicator α ∅ 0) = 1

Base of the recurrence: over no contributors, the count is 0 with probability 1.

theorem HavingExample.mass_empty_succ (j : ℕ) : P.funcProb (HavingProbability.countEqIndicator α ∅ (j + 1)) = 0

Base of the recurrence: over no contributors, a positive count has probability 0.

theorem HavingExample.mass_1_0 : P.funcProb (HavingProbability.countEqIndicator α (insert 2 ∅) 0) = 2 / 3

theorem HavingExample.mass_1_1 : P.funcProb (HavingProbability.countEqIndicator α (insert 2 ∅) 1) = 1 / 3

theorem HavingExample.mass_1_2 : P.funcProb (HavingProbability.countEqIndicator α (insert 2 ∅) 2) = 0

theorem HavingExample.mass_1_3 : P.funcProb (HavingProbability.countEqIndicator α (insert 2 ∅) 3) = 0

theorem HavingExample.mass_2_1 : P.funcProb (HavingProbability.countEqIndicator α (insert 1 (insert 2 ∅)) 1) = 5 / 12

theorem HavingExample.mass_2_2 : P.funcProb (HavingProbability.countEqIndicator α (insert 1 (insert 2 ∅)) 2) = 1 / 12

theorem HavingExample.mass_2_3 : P.funcProb (HavingProbability.countEqIndicator α (insert 1 (insert 2 ∅)) 3) = 0

theorem HavingExample.mass_3_2 : P.funcProb (HavingProbability.countEqIndicator α Finset.univ 2) = 1 / 4

Point mass ρ₃(2) = 1/4: probability that exactly two of the three contributors are present.

theorem HavingExample.mass_3_3 : P.funcProb (HavingProbability.countEqIndicator α Finset.univ 3) = 1 / 24

Point mass ρ₃(3) = 1/24: probability that all three contributors are present.

theorem HavingExample.count_ge_two_prob : (P.funcProb fun (v : Fin 3 → Bool) => decide (2 ≤ {i : Fin 3 | α i v = true}.card)) = 7 / 24

Pr[COUNT(*) ≥ 2] = 7/24: the tail of the Poisson-binomial CDF, assembled from the point masses ρ₃(2) + ρ₃(3) = 1/4 + 1/24.

Home · Documentation · Publications · Contributors · Source · Cite