Categorical-block probability and deterministic-OR soundness

This file is the categorical-block counterpart of Provenance.Circuit's decomposable + deterministic weighted-model-counting correctness theorem (Circuit.dD_funcProb_eq_probDD): the same result re-proved over categorical block variables instead of free Boolean variables. It is an independent development (it shares no code with Provenance.Circuit; the Boolean case is the κ ≡ fun _ => Bool instance of this one).

It is the formal counterpart of the verified mulinput-OR certificate correctness-hardening item for ProvSQL's bounded-treewidth route (the repair_key / BID block consumed by evaluateCertifiedIsland): that evaluator marks a block's plus(mulinputs) deterministic and trusts the mark: it plain-sums the alternatives, registers the block key once, and reads the none-branch as monus(one, plus(mulinputs)) = 1 - Σ pᵢ. The determinism of those state ORs is a global property the C++ does not check locally. This development is the spec backing that trust, in the probability / weighted-model-counting semantics.

Modeling choice (the crux)

A block is modeled as one categorical random variable, not as independent Booleans with an at-most-one constraint. Concretely we work over a finite index ι of blocks, each block b : ι carrying a finite outcome type κ b; a CatAssignment gives, per block, a probability distribution P.prob b : κ b → ℚ summing to 1. A valuation v : (b : ι) → κ b draws one outcome per block, with the blocks independent: valProb v = ∏ b, P.prob b (v b).

A mulinput mᵢ of a block b is the event {v | v b = i}; the none-branch is {v | v b = o} for a designated outcome o : κ b. With this model the three block facts the C++ relies on are near-immediate (mulin_disjoint, mulin_or_prob, mulin_none), and the deterministic-OR sum is exact (singleBlock_detOR_sound).

Main definitions

• CatAssignment κ – a per-block categorical probability distribution.
• CatAssignment.valProb – Pr(v) for a categorical valuation, blocks independent.
• CatAssignment.eventProb – Pr(E) for an event E : ((b : ι) → κ b) → Bool.
• EventDependsOn – support of an event (a Finset of blocks).
• CatCircuit ι κ – Boolean circuits whose leaves are block-outcome literals lit b i (the event {v b = i}).
• CatCircuit.Decomposable / Deterministic / probDD – the d-D structural predicates and the direct-summation evaluator, exactly as in Provenance.Circuit but over categorical blocks.

Main results

• CatAssignment.eventProb_and_disjoint – independence: Pr(E ∧ F) = Pr(E)·Pr(F) when E, F depend on disjoint block sets.
• CatAssignment.eventProb_or, eventProb_not – inclusion-exclusion and complement.
• CatAssignment.eventProb_lit, eventProb_block_mem – leaf / marginal: Pr(v b = i) = pᵢ and Pr(v b ∈ S) = Σ_{i∈S} pᵢ.
• CatCircuit.dD_eventProb_eq_probDD – the lifted d-D soundness theorem: Pr(⟦c⟧) = probDD c for decomposable + deterministic categorical circuits.
• CatAssignment.mulin_disjoint, mulin_or_prob, mulin_none – the three block lemmas backing the deterministic-OR mark and the 1 - Σ pᵢ none-branch.
• CatAssignment.singleBlock_detOR_sound – single-block soundness: the plain sum of a block's mulinput marginals equals the probability the block fires.

References

• Sen, Maniu & Senellart (Section V-D)
• Amarilli, Bourhis & Senellart, Provenance Circuits for Trees and Treelike Instances (ICALP 2015)

structure CatAssignment {ι : Type} (κ : ι → Type) [(b : ι) → Fintype (κ b)] : Type

A categorical assignment: for each block b : ι, a probability distribution prob b : κ b → ℚ over that block's finite outcome type. This is the categorical analogue of ProbAssignment (where every block would be a single Bool).

• prob (b : ι) : κ b → ℚ

  The probability assigned to each outcome of each block.

• prob_nonneg (b : ι) (i : κ b) : 0 ≤ self.prob b i

  Probabilities are non-negative.

• sum_prob (b : ι) : ∑ i : κ b, self.prob b i = 1

  Each block's outcome probabilities sum to 1.

theorem CatAssignment.prob_le_one {ι : Type} [Fintype ι] [DecidableEq ι] {κ : ι → Type} [(b : ι) → Fintype (κ b)] [(b : ι) → DecidableEq (κ b)] (P : CatAssignment κ) (b : ι) (i : κ b) : P.prob b i ≤ 1

Each individual outcome probability is at most 1 (it is one summand of a sum of non-negatives equal to 1).

def CatAssignment.valProb {ι : Type} [Fintype ι] {κ : ι → Type} [(b : ι) → Fintype (κ b)] (P : CatAssignment κ) (v : (b : ι) → κ b) : ℚ

Probability of a categorical valuation v, the blocks independent: Pr(v) = ∏ b, P.prob b (v b).

Equations

• P.valProb v = ∏ b : ι, P.prob b (v b)

def CatAssignment.eventProb {ι : Type} [Fintype ι] [DecidableEq ι] {κ : ι → Type} [(b : ι) → Fintype (κ b)] (P : CatAssignment κ) (E : ((b : ι) → κ b) → Bool) : ℚ

Probability of an event E over categorical valuations: Pr(E) = ∑_{v ⊨ E} Pr(v).

Equations

• P.eventProb E = ∑ v : (b : ι) → κ b, if E v = true then P.valProb v else 0

theorem CatAssignment.valProb_nonneg {ι : Type} [Fintype ι] [DecidableEq ι] {κ : ι → Type} [(b : ι) → Fintype (κ b)] [(b : ι) → DecidableEq (κ b)] (P : CatAssignment κ) (v : (b : ι) → κ b) : 0 ≤ P.valProb v

theorem CatAssignment.sum_valProb_eq_one {ι : Type} [Fintype ι] [DecidableEq ι] {κ : ι → Type} [(b : ι) → Fintype (κ b)] [(b : ι) → DecidableEq (κ b)] (P : CatAssignment κ) : ∑ v : (b : ι) → κ b, P.valProb v = 1

The categorical valuations form a probability distribution: ∑ v, Pr(v) = 1.

theorem CatAssignment.eventProb_nonneg {ι : Type} [Fintype ι] [DecidableEq ι] {κ : ι → Type} [(b : ι) → Fintype (κ b)] [(b : ι) → DecidableEq (κ b)] (P : CatAssignment κ) (E : ((b : ι) → κ b) → Bool) : 0 ≤ P.eventProb E

theorem CatAssignment.eventProb_le_one {ι : Type} [Fintype ι] [DecidableEq ι] {κ : ι → Type} [(b : ι) → Fintype (κ b)] [(b : ι) → DecidableEq (κ b)] (P : CatAssignment κ) (E : ((b : ι) → κ b) → Bool) : P.eventProb E ≤ 1

theorem CatAssignment.eventProb_false {ι : Type} [Fintype ι] [DecidableEq ι] {κ : ι → Type} [(b : ι) → Fintype (κ b)] [(b : ι) → DecidableEq (κ b)] (P : CatAssignment κ) : (P.eventProb fun (x : (b : ι) → κ b) => false) = 0

Pr(false) = 0.

theorem CatAssignment.eventProb_true {ι : Type} [Fintype ι] [DecidableEq ι] {κ : ι → Type} [(b : ι) → Fintype (κ b)] [(b : ι) → DecidableEq (κ b)] (P : CatAssignment κ) : (P.eventProb fun (x : (b : ι) → κ b) => true) = 1

Pr(true) = 1.

theorem CatAssignment.eventProb_congr {ι : Type} [Fintype ι] [DecidableEq ι] {κ : ι → Type} [(b : ι) → Fintype (κ b)] [(b : ι) → DecidableEq (κ b)] (P : CatAssignment κ) {E F : ((b : ι) → κ b) → Bool} (h : ∀ (v : (b : ι) → κ b), E v = F v) : P.eventProb E = P.eventProb F

Pointwise-equal events have equal probabilities.

Support of an event

def EventDependsOn {ι : Type} {κ : ι → Type} (E : ((b : ι) → κ b) → Bool) (S : Finset ι) : Prop

E depends only on the blocks in S: any two valuations agreeing on S give E the same value. The categorical analogue of BoolFunc.DependsOn.

Equations

• EventDependsOn E S = ∀ (v₁ v₂ : (b : ι) → κ b), (∀ b ∈ S, v₁ b = v₂ b) → E v₁ = E v₂

Leaf / marginal probabilities

theorem CatAssignment.eventProb_block_mem {ι : Type} [Fintype ι] [DecidableEq ι] {κ : ι → Type} [(b : ι) → Fintype (κ b)] [(b : ι) → DecidableEq (κ b)] (P : CatAssignment κ) (b : ι) (S : Finset (κ b)) : (P.eventProb fun (v : (b : ι) → κ b) => decide (v b ∈ S)) = ∑ i ∈ S, P.prob b i

Marginal. The probability that block b's outcome lies in a finset S of outcomes is the sum of the corresponding marginals. The categorical analogue of funcProb_var, proved by the same Fintype.prod_sum column-swap.

theorem CatAssignment.eventProb_lit {ι : Type} [Fintype ι] [DecidableEq ι] {κ : ι → Type} [(b : ι) → Fintype (κ b)] [(b : ι) → DecidableEq (κ b)] (P : CatAssignment κ) (b : ι) (i : κ b) : (P.eventProb fun (v : (b : ι) → κ b) => decide (v b = i)) = P.prob b i

Leaf. Pr(v b = i) = pᵢ.

Independence, inclusion-exclusion, complement

theorem CatAssignment.eventProb_and_disjoint {ι : Type} [Fintype ι] [DecidableEq ι] {κ : ι → Type} [(b : ι) → Fintype (κ b)] [(b : ι) → DecidableEq (κ b)] (P : CatAssignment κ) {E F : ((b : ι) → κ b) → Bool} {S T : Finset ι} (hE : EventDependsOn E S) (hF : EventDependsOn F T) (hST : Disjoint S T) : (P.eventProb fun (v : (b : ι) → κ b) => E v && F v) = P.eventProb E * P.eventProb F

Independence lemma. If E depends on block set S and F on block set T with S, T disjoint, then Pr(E ∧ F) = Pr(E) · Pr(F). The categorical analogue of funcProb_mul_disjoint; the deterministic-AND / decomposability soundness.

theorem CatAssignment.eventProb_or {ι : Type} [Fintype ι] [DecidableEq ι] {κ : ι → Type} [(b : ι) → Fintype (κ b)] [(b : ι) → DecidableEq (κ b)] (P : CatAssignment κ) (E F : ((b : ι) → κ b) → Bool) : (P.eventProb fun (v : (b : ι) → κ b) => E v || F v) = P.eventProb E + P.eventProb F - P.eventProb fun (v : (b : ι) → κ b) => E v && F v

Inclusion-exclusion. Pr(E ∨ F) = Pr(E) + Pr(F) - Pr(E ∧ F), with no disjointness hypothesis. The categorical analogue of funcProb_add_eq.

theorem CatAssignment.eventProb_not {ι : Type} [Fintype ι] [DecidableEq ι] {κ : ι → Type} [(b : ι) → Fintype (κ b)] [(b : ι) → DecidableEq (κ b)] (P : CatAssignment κ) (E : ((b : ι) → κ b) → Bool) : (P.eventProb fun (v : (b : ι) → κ b) => !E v) = 1 - P.eventProb E

Complement. Pr(¬E) = 1 - Pr(E).

Categorical circuits and d-D soundness

inductive CatCircuit (ι : Type) (κ : ι → Type) : Type

A Boolean circuit whose variable leaves are block-outcome literals: lit b i denotes the event {v | v b = i}. Otherwise identical to Circuit.

• const {ι : Type} {κ : ι → Type} : Bool → CatCircuit ι κ

  A Boolean constant.

• lit {ι : Type} {κ : ι → Type} (b : ι) : κ b → CatCircuit ι κ

  The leaf event {v | v b = i}.

• not {ι : Type} {κ : ι → Type} : CatCircuit ι κ → CatCircuit ι κ

  Logical negation.

• and {ι : Type} {κ : ι → Type} : CatCircuit ι κ → CatCircuit ι κ → CatCircuit ι κ

  Logical conjunction.

• or {ι : Type} {κ : ι → Type} : CatCircuit ι κ → CatCircuit ι κ → CatCircuit ι κ

  Logical disjunction.

def CatCircuit.eval {ι : Type} {κ : ι → Type} [(b : ι) → DecidableEq (κ b)] : CatCircuit ι κ → ((b : ι) → κ b) → Bool

Evaluate a categorical circuit under a categorical valuation.

Equations

• (CatCircuit.const x_2).eval x✝ = x_2
• (CatCircuit.lit b i).eval x✝ = decide (x✝ b = i)
• c.not.eval x✝ = !c.eval x✝
• (c.and d).eval x✝ = (c.eval x✝ && d.eval x✝)
• (c.or d).eval x✝ = (c.eval x✝ || d.eval x✝)

def CatCircuit.toEvent {ι : Type} {κ : ι → Type} [(b : ι) → DecidableEq (κ b)] (c : CatCircuit ι κ) : ((b : ι) → κ b) → Bool

The event a circuit denotes.

Equations

• c.toEvent = c.eval

def CatCircuit.blocks {ι : Type} [DecidableEq ι] {κ : ι → Type} : CatCircuit ι κ → Finset ι

The set of blocks a circuit reads (the categorical "variable support").

Equations

• (CatCircuit.const a).blocks = ∅
• (CatCircuit.lit b a).blocks = {b}
• c.not.blocks = c.blocks
• (c.and d).blocks = c.blocks ∪ d.blocks
• (c.or d).blocks = c.blocks ∪ d.blocks

inductive CatCircuit.Decomposable {ι : Type} [DecidableEq ι] {κ : ι → Type} : CatCircuit ι κ → Prop

Decomposable: every AND gate has children reading disjoint block sets.

• const {ι : Type} [DecidableEq ι] {κ : ι → Type} (x : Bool) : (CatCircuit.const x).Decomposable
• lit {ι : Type} [DecidableEq ι] {κ : ι → Type} (b : ι) (i : κ b) : (CatCircuit.lit b i).Decomposable
• not {ι : Type} [DecidableEq ι] {κ : ι → Type} {c : CatCircuit ι κ} : c.Decomposable → c.not.Decomposable
• and {ι : Type} [DecidableEq ι] {κ : ι → Type} {c d : CatCircuit ι κ} : c.Decomposable → d.Decomposable → Disjoint c.blocks d.blocks → (c.and d).Decomposable
• or {ι : Type} [DecidableEq ι] {κ : ι → Type} {c d : CatCircuit ι κ} : c.Decomposable → d.Decomposable → (c.or d).Decomposable

inductive CatCircuit.Deterministic {ι : Type} {κ : ι → Type} [(b : ι) → DecidableEq (κ b)] : CatCircuit ι κ → Prop

Deterministic: every OR gate has children that are mutually exclusive as events (their conjunction is unsatisfiable). This is the categorical deterministic-OR mark: for the mulinput-OR of one block it is supplied by mulin_disjoint.

• const {ι : Type} {κ : ι → Type} [(b : ι) → DecidableEq (κ b)] (x : Bool) : (CatCircuit.const x).Deterministic
• lit {ι : Type} {κ : ι → Type} [(b : ι) → DecidableEq (κ b)] (b : ι) (i : κ b) : (CatCircuit.lit b i).Deterministic
• not {ι : Type} {κ : ι → Type} [(b : ι) → DecidableEq (κ b)] {c : CatCircuit ι κ} : c.Deterministic → c.not.Deterministic
• and {ι : Type} {κ : ι → Type} [(b : ι) → DecidableEq (κ b)] {c d : CatCircuit ι κ} : c.Deterministic → d.Deterministic → (c.and d).Deterministic
• or {ι : Type} {κ : ι → Type} [(b : ι) → DecidableEq (κ b)] {c d : CatCircuit ι κ} : c.Deterministic → d.Deterministic → (∀ (v : (b : ι) → κ b), (c.eval v && d.eval v) = false) → (c.or d).Deterministic

def CatCircuit.probDD {ι : Type} {κ : ι → Type} [(b : ι) → Fintype (κ b)] (P : CatAssignment κ) : CatCircuit ι κ → ℚ

The d-D direct-summation evaluator (categorical). Differs from a read-once evaluator only at OR gates, which sum directly.

Equations

• CatCircuit.probDD P (CatCircuit.const true) = 1
• CatCircuit.probDD P (CatCircuit.const false) = 0
• CatCircuit.probDD P (CatCircuit.lit b i) = P.prob b i
• CatCircuit.probDD P c.not = 1 - CatCircuit.probDD P c
• CatCircuit.probDD P (c.and d) = CatCircuit.probDD P c * CatCircuit.probDD P d
• CatCircuit.probDD P (c.or d) = CatCircuit.probDD P c + CatCircuit.probDD P d

theorem CatCircuit.toEvent_dependsOn_blocks {ι : Type} [Fintype ι] [DecidableEq ι] {κ : ι → Type} [(b : ι) → Fintype (κ b)] [(b : ι) → DecidableEq (κ b)] (c : CatCircuit ι κ) : EventDependsOn c.toEvent c.blocks

A circuit's event depends only on the blocks it reads.

theorem CatCircuit.dD_eventProb_eq_probDD {ι : Type} [Fintype ι] [DecidableEq ι] {κ : ι → Type} [(b : ι) → Fintype (κ b)] [(b : ι) → DecidableEq (κ b)] (P : CatAssignment κ) (c : CatCircuit ι κ) (hd : c.Decomposable) (hdet : c.Deterministic) : P.eventProb c.toEvent = probDD P c

Lifted d-D soundness theorem. For any decomposable + deterministic categorical circuit c, the direct-summation evaluator c.probDD P agrees with the weighted-model-counting semantics Pr(⟦c⟧). This is Circuit.dD_funcProb_eq_probDD lifted from free Boolean variables to categorical block variables: AND uses eventProb_and_disjoint (decomposability), OR uses eventProb_or with the determinism hypothesis collapsing the inclusion-exclusion term, NOT uses eventProb_not.

The three block lemmas and single-block soundness

The payload backing evaluateCertifiedIsland's trust in the deterministic-OR mark of a repair_key block. A block is b : ι; its outcomes are κ b, with a designated none-outcome o : κ b and the mulinputs being all other outcomes i ∈ univ.erase o, with marginals pᵢ = P.prob b i.

theorem CatAssignment.mulin_disjoint {ι : Type} [Fintype ι] [DecidableEq ι] {κ : ι → Type} [(b : ι) → Fintype (κ b)] [(b : ι) → DecidableEq (κ b)] (b : ι) {i j : κ b} (h : i ≠ j) (v : (b : ι) → κ b) : ((CatCircuit.lit b i).eval v && (CatCircuit.lit b j).eval v) = false

mulin_disjoint. Distinct mulinputs of one block are mutually exclusive events: this is what licenses marking the block's mulinput-OR deterministic (CatCircuit.Deterministic.or).

theorem CatAssignment.mulin_or_prob {ι : Type} [Fintype ι] [DecidableEq ι] {κ : ι → Type} [(b : ι) → Fintype (κ b)] [(b : ι) → DecidableEq (κ b)] (P : CatAssignment κ) (b : ι) (o : κ b) : (P.eventProb fun (v : (b : ι) → κ b) => decide (v b ≠ o)) = ∑ i ∈ Finset.univ.erase o, P.prob b i

mulin_or_prob. The probability that block b fires some mulinput (its outcome is not the none-outcome o) is the exact sum of the mulinput marginals: the plain sum evaluateCertifiedIsland computes is exact.

theorem CatAssignment.mulin_none {ι : Type} [Fintype ι] [DecidableEq ι] {κ : ι → Type} [(b : ι) → Fintype (κ b)] [(b : ι) → DecidableEq (κ b)] (P : CatAssignment κ) (b : ι) (o : κ b) : (P.eventProb fun (v : (b : ι) → κ b) => decide (v b = o)) = 1 - ∑ i ∈ Finset.univ.erase o, P.prob b i

mulin_none. The none-branch probability is 1 - Σ pᵢ, the monus(one, plus(mulinputs)) the evaluator reads.

theorem CatAssignment.singleBlock_detOR_sound {ι : Type} [Fintype ι] [DecidableEq ι] {κ : ι → Type} [(b : ι) → Fintype (κ b)] [(b : ι) → DecidableEq (κ b)] (P : CatAssignment κ) (b : ι) (o : κ b) : (∑ i ∈ Finset.univ.erase o, P.eventProb fun (v : (b : ι) → κ b) => decide (v b = i)) = P.eventProb fun (v : (b : ι) → κ b) => decide (v b ≠ o)

Single-block soundness. Plain-summing the marginals of a block's mulinputs (exactly what evaluateCertifiedIsland does for the marked deterministic OR) equals the probability that the block fires. Combines eventProb_lit and mulin_or_prob; it is the single-block instance of CatCircuit.dD_eventProb_eq_probDD.

Home · Documentation · Publications · Contributors · Source · Cite