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_iff {α : Type} {x y : Why α} : x = y ↔ x.carrier = y.carrier

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

@[implicit_reducible]

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

Equations

• instCoeWhySet = { coe := Why.carrier }

@[implicit_reducible]

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

Equations

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

@[implicit_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} }

@[implicit_reducible]

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

Equations

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

@[implicit_reducible]

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

Equations

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

@[implicit_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_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 : ∃ (t₁ : Why (Fin 2)), ∃ (t₂ : Why (Fin 2)), ∃ (t₃ : Why (Fin 2)), t₁ * t₂ * (1 - t₃) + t₁ * t₃ * (1 - t₂) + t₂ * t₃ * (1 - t₁) ≠ t₁ * t₂ + t₁ * t₃ + t₂ * t₃

The two natural expansions of HAVING (count = 2) for a three-tuple group, (t₁ ⊗ t₂) ⊗ (𝟙 ⊖ t₃) ⊕ (t₁ ⊗ t₃) ⊗ (𝟙 ⊖ t₂) ⊕ (t₂ ⊗ t₃) ⊗ (𝟙 ⊖ t₁) and (t₁ ⊗ t₂) ⊕ (t₁ ⊗ t₃) ⊕ (t₂ ⊗ t₃), are inequivalent in Why[X]. With t₁ = ⟨{{0}}⟩, t₂ = ⟨{{1}}⟩, t₃ = ⟨{∅}⟩ = 𝟙 over X = Fin 2, the first expression has carrier {{0}, {1}} while the second has the strictly larger carrier {{0, 1}, {0}, {1}}. The witness set {0, 1} separates them.

Home · Documentation · Publications · Contributors · Source · Cite