Why-provenance m-semiring Why[X]

This file defines the Why provenance semiring Why α = Set (Set α). Elements are sets of subsets of α (representing sets of witnesses). Addition is union of families, and multiplication is pairwise union of witnesses.

Why α is idempotent but not absorptive when α is nonempty. It also does not satisfy left-distributivity of multiplication over monus, contradicting a claim in Amsterdamer, Deutch & Tannen, On the limitations of provenance for queries with differences, Table on p. 4.

References

• Amsterdamer, Deutch & Tannen, On the limitations of provenance for queries with differences

structure Why (α : Type) : Type

• carrier : Set (Set α)

theorem Why.ext {α : Type} {x y : Why α} (carrier : x.carrier = y.carrier) : x = y

theorem Why.ext_iff {α : Type} {x y : Why α} : x = y ↔ x.carrier = y.carrier

@[instance_reducible]

instance instCoeWhySet {α : Type} : Coe (Why α) (Set (Set α))

Equations

• instCoeWhySet = { coe := Why.carrier }

@[instance_reducible]

instance instZeroWhy {α : Type} : Zero (Why α)

Equations

• instZeroWhy = { zero := { carrier := ∅ } }

@[instance_reducible]

instance instAddWhy {α : Type} : Add (Why α)

Equations

• instAddWhy = { add := fun (a b : Why α) => { carrier := a.carrier ∪ b.carrier } }

def why_mul {α : Type} (a b : Why α) : Why α

Equations

• why_mul a b = { carrier := {z : Set α | ∃ (x : Set α), ∃ (y : Set α), x ∈ a.carrier ∧ y ∈ b.carrier ∧ z = x ∪ y} }

@[instance_reducible]

instance instCommSemiringWhy {α : Type} : CommSemiring (Why α)

Equations

• One or more equations did not get rendered due to their size.

@[instance_reducible]

instance instSemiringWithMonusWhy {α : Type} : SemiringWithMonus (Why α)

Why-provenance is a semiring with monus: ∖ is set difference on the outer level, 2^(2^X) ordered by inclusion.

Named explicitly, and not to be renamed: this name is published as a link target in Sen, Maniu & Senellart, ProvSQL: A General System for Keeping Track of the Provenance and Probability of Data, ICDE 2026.

Equations

• One or more equations did not get rendered due to their size.

@[instance_reducible]

instance instCommSemiringWithMonusWhy {α : Type} : CommSemiringWithMonus (Why α)

Equations

• instCommSemiringWithMonusWhy = { toSemiringWithMonus := instSemiringWithMonusWhy, mul_comm := ⋯ }

theorem Why.idempotent {α : Type} : _root_.idempotent (Why α)

instance instNontrivialWhy {α : Type} : Nontrivial (Why α)

instance Why.instCharPZero {α : Type} : CharP (Why α) 0

Why α has characteristic 0 in the CharP sense: it is idempotent and nontrivial (⟨∅⟩ ≠ ⟨{∅}⟩), so every positive natural-number cast equals 1.

theorem Why.not_absorptive {α : Type} (hNotEmpty : ∃ (x : α), ⊤) : ¬absorptive (Why α)

theorem Why.not_isDelta_id {α : Type} (hNotEmpty : ∃ (x : α), ⊤) : ¬IsDelta id

On Why[X] with a non-empty variable set, the identity is not an admissible δ: delta_absorb at a = 𝟙 is absorptivity, which Why[X] lacks. This is why the instance takes the support indicator rather than ProvSQL's historical witness-preserving Why::delta.

theorem Why.not_mul_sub_left_distributive {α : Type} [Inhabited α] : ¬mul_sub_left_distributive (Why α)

In Why[X], as long as X is non-empty, times is not distributive over monus. Note that this contradicts Amsterdamer, Deutch & Tannen, On the limitations of provenance for queries with differences, table page 4, which claims this semiring satisfies axiom A13.

theorem Why.no_hom_from_BoolFunc {α Y : Type} [Inhabited Y] [Inhabited α] : ∃ (ν : Y → Why α), ¬∃ (φ : BoolFunc Y →+* Why α), ∀ (i : Y), φ (BoolFunc.var i) = ν i

There is no semiring homomorphism from BoolFunc Y to Why α (with α inhabited) sending the variables to arbitrary values: Why α is not absorptive (Why.not_absorptive), which contradicts var i + 1 = 1 in BoolFunc Y.

theorem Why.counterexample_having {α : Type} [Inhabited α] : ∃ (t₁ : Why α), ∃ (t₂ : Why α), ∃ (t₃ : Why α), t₁ * t₂ * (1 - t₃) + t₁ * t₃ * (1 - t₂) + t₂ * t₃ * (1 - t₁) ≠ t₁ * t₂ + t₁ * t₃ + t₂ * t₃ - t₁ * t₂ * t₃

The =-comparison correspondence fails in Why[X]. For a three-tuple group with occurrence annotations t₁, t₂, t₃, the fused HAVING (COUNT(*) = 2) predicate provenance is (t₁ ⊗ t₂) ⊗ (𝟙 ⊖ t₃) ⊕ (t₁ ⊗ t₃) ⊗ (𝟙 ⊖ t₂) ⊕ (t₂ ⊗ t₃) ⊗ (𝟙 ⊖ t₁), while the join-based rewriting Q₂^{≥2} − Q₂^{≥3} annotates the key with ((t₁ ⊗ t₂) ⊕ (t₁ ⊗ t₃) ⊕ (t₂ ⊗ t₃)) ⊖ (t₁ ⊗ t₂ ⊗ t₃). In Why[X] – idempotent, but without distributivity of ⊗ over ⊖ (Why.not_mul_sub_left_distributive) – the two disagree: with t₁ = t₂ = t₃ = ⟨{{a}}⟩ for any witness a, every product equals ⟨{{a}}⟩ and every factor 𝟙 ⊖ tᵢ equals 𝟙 (as ∅ ∉ {{a}}), so the fused side keeps the witness, ⟨{{a}}⟩, while on the join side the difference of the two ≥-chains cancels it: ⟨{{a}}⟩ ⊖ ⟨{{a}}⟩ = 𝟘.

Home · Documentation · Publications · Contributors · Source · Cite