Support adequacy over 𝔹 and transfer along monus homomorphisms

Provenance.QueryAdequacy shows that on the data parts, adequacy of the annotated semantics with the plain semantics stops at the positive fragment. This file gives the equality that does extend to the full non-aggregation fragment (difference and duplicate elimination included): over the Boolean m-semiring 𝔹, the support of the annotated evaluation – the multiset of true-annotated tuple slots – is exactly the plain evaluation of the support of the database (Query.evaluateAnnotated_support).

The result is derived, rather than re-proved, from the possible-worlds commutation theorem randomWorld_evaluateAnnotated of Provenance.Probability, instantiated at the variable-free Boolean-function semiring BoolFunc Empty ≃ 𝔹 via the constant embedding Bool.constHom.

It then transfers along any m-semiring homomorphism h : K → 𝔹 (Query.evaluateAnnotated_support_hom), by the hom-commutation theorem Query.evaluateAnnotated_hom: every annotation domain that admits a monus-preserving support map into 𝔹 inherits the adequacy equality. BoolFunc X admits one per valuation (Bool.homomorphism_to_BoolFunc), which recovers the possible-worlds reading; ℕ admits none (Nat.no_monusHom_to_Bool in Provenance.Semirings.Nat) – its support map n ↦ (n ≠ 0) is a ring homomorphism but does not preserve monus, which is the algebraic reason why ℕ-adequacy is restricted to the positive fragment (the theorem of Benzaken, Cohen-Boulakia, Contejean, Keller & Zucchini, A Coq formalization of data provenance).

Main definitions

• AnnotatedRelation.support, AnnotatedDatabase.support – the true-annotated tuple slots of a 𝔹-annotated relation / database
• Bool.constHom – the constant embedding 𝔹 → 𝔹[X] as an m-semiring homomorphism

Main results

• Query.evaluateAnnotated_support – support adequacy over 𝔹, for the full non-aggregation fragment
• Query.evaluateAnnotated_support_hom – transfer along any m-semiring homomorphism K → 𝔹

References

• Benzaken, Cohen-Boulakia, Contejean, Keller & Zucchini, A Coq formalization of data provenance
• Sen, Maniu & Senellart, ProvSQL

def AnnotatedRelation.support {T : Type} {n : ℕ} (r : AnnotatedRelation T Bool n) : Multiset (Tuple T n)

Boolean support of a 𝔹-annotated relation: the multiset of data parts of the true-annotated tuple slots. The return type is a bare Multiset (Tuple T n) so that Multiset lemmas apply without an extra unfolding step.

Equations

• r.support = Multiset.map Prod.fst (Multiset.filter (fun (p : AnnotatedTuple T Bool n) => p.2 = true) r)

def AnnotatedDatabase.support {T : Type} (d : AnnotatedDatabase T Bool) : Database T

Boolean support of a 𝔹-annotated database, relation by relation.

Equations

• d.support = List.map (fun (e : String × (n : ℕ) × AnnotatedRelation T Bool n) => (e.1, ⟨e.2.fst, e.2.snd.support⟩)) d

@[reducible]

def Bool.constHom (X : Type) : SemiringWithMonusHom Bool (BoolFunc X)

The constant embedding 𝔹 → 𝔹[X] as an m-semiring homomorphism (the same homomorphism exhibited by Bool.homomorphism_from_BoolFunc, as a usable definition).

Equations

• Bool.constHom X = { toFun := fun (b : Bool) (x : X → Bool) => b, map_one' := ⋯, map_mul' := ⋯, map_zero' := ⋯, map_add' := ⋯, map_sub := ⋯, map_delta := ⋯ }

theorem randomWorld_constHom {T : Type} {n : ℕ} {X : Type} (v : X → Bool) (r : AnnotatedRelation T Bool n) : randomWorld v ((Bool.constHom X).mapAnnotatedRelation r) = r.support

The random world of the constant embedding of a 𝔹-annotated relation is its support, under any valuation.

theorem AnnotatedDatabase.randomWorld_constHom {T X : Type} (v : X → Bool) (d : AnnotatedDatabase T Bool) : randomWorld v ((Bool.constHom X).mapAnnotatedDatabase d) = d.support

Database-level version of randomWorld_constHom.

theorem Query.evaluateAnnotated_support {T : Type} [ValueType T] {n : ℕ} (q : Query T n) (hq : q.noAgg) (d : AnnotatedDatabase T Bool) : (q.evaluateAnnotated hq d).support = q.evaluate d.support

Support adequacy over 𝔹. For any non-aggregation query q – the full fragment, difference and duplicate elimination included – the support of the 𝔹-annotated evaluation equals the plain evaluation of the support of the database. This is the equality that replaces the (positive-fragment only) ℕ-adequacy of Benzaken, Cohen-Boulakia, Contejean, Keller & Zucchini once difference enters the language.

theorem Query.evaluateAnnotated_support_hom {T : Type} [ValueType T] {K : Type} [SemiringWithMonus K] [DecidableEq K] {n : ℕ} (h : SemiringWithMonusHom K Bool) (q : Query T n) (hq : q.noAgg) (d : AnnotatedDatabase T K) : (h.mapAnnotatedRelation (q.evaluateAnnotated hq d)).support = q.evaluate (h.mapAnnotatedDatabase d).support

Transfer of support adequacy along monus homomorphisms. Any m-semiring homomorphism h : K → 𝔹 turns the annotated evaluation over K into a plain evaluation on the h-support of the database. BoolFunc X admits one such homomorphism per valuation (Bool.homomorphism_to_BoolFunc), recovering the possible-worlds semantics; ℕ admits none (Nat.no_monusHom_to_Bool), which is why ℕ-adequacy stops at the positive fragment.

Home · Documentation · Publications · Contributors · Source · Cite