Query semantics over annotated databases

This file defines the evaluation of relational algebra queries over annotated databases. Query operators are lifted to annotated relations using the m-semiring operations of the annotation domain K: addition corresponds to union, multiplication to join, and monus to difference. This is the algebra of Section IV-B of Sen, Maniu & Senellart, ProvSQL: A General System for Keeping Track of the Provenance and Probability of Data, itself an adaptation of Green, Karvounarakis & Tannen, Provenance Semirings to multiset semantics with explicit duplicate elimination and multiset difference.

Main definitions

• Query.evaluateAnnotated – evaluates a query over an AnnotatedDatabase T K, propagating annotations through each relational operator according to the semiring structure of K

References

• Sen, Maniu & Senellart, ProvSQL (Section IV-B)
• Green, Karvounarakis & Tannen, Provenance Semirings

@[reducible]

def Filter.evalDecidableAnnotated {T : Type} [ValueType T] {K : Type} {n : ℕ} (φ : Filter T n) : DecidablePred fun (ta : AnnotatedTuple T K n) => φ.eval ta.1

Equations

• φ.evalDecidableAnnotated t = match φ.evalDecidable t.1 with | isTrue h => isTrue h | isFalse h => isFalse ⋯

def groupByKey {T : Type} [ValueType T] {K : Type} [SemiringWithMonus K] [DecidableEq K] {n : ℕ} (m : Multiset (Tuple T n × K)) : { l : List (Tuple T n × K) // KeyValueList l }

Equations

• groupByKey m = Multiset.foldr KeyValueList.addKVFold ⟨[], True.intro⟩ m

def Query.evaluateAnnotated {T : Type} [ValueType T] {K : Type} [SemiringWithMonus K] [DecidableEq K] {n : ℕ} (q : Query T n) (hq : q.noAgg) (d : AnnotatedDatabase T K) : AnnotatedRelation T K n

Annotated (m-semiring) semantics of a non-aggregation query.

The Diff case follows ProvSQL: every tuple slot (u, α) of r₁ is kept, with its annotation rewritten to α ⊖ Σ β where Σ β is the semiring sum of the annotations of all copies of u in r₂. Two consequences worth noting:

• difference never removes tuple slots (only annotations change, possibly to 0), so the data part of the result is insensitive to Diff – this is made precise in Provenance.QueryAdequacy;
• each copy of u in r₁ separately gets the full grouped sum subtracted, so the result is not invariant under regrouping extensionally equal annotated relations: over ℕ, {(t,1),(t,1)} ∖ {(t,1)} has total annotation 0 while {(t,2)} ∖ {(t,1)} has total annotation 1. As a consequence, over ℕ the annotated semantics agrees with the all-or-nothing plain difference of Query.evaluate on 0/1-annotated inputs, but not once Dedup has accumulated annotations (see Nat.counterexample_diff_adequacy).

Equations

• One or more equations did not get rendered due to their size.
• (Query.Rel n s).evaluateAnnotated hq_2 d = match h : AnnotatedDatabase.find n s d with | none => ∅ | some rn => rn
• (Π ts q').evaluateAnnotated hq_2 d = Multiset.map (fun (t : AnnotatedTuple T K n_2) => (fun (k : Fin n) => (ts k).eval t.1, t.2)) (q'.evaluateAnnotated ⋯ d)
• (σ φ q_2).evaluateAnnotated hq_2 d = Multiset.filter (fun (ta : AnnotatedTuple T K n) => φ.eval ta.1) (q_2.evaluateAnnotated ⋯ d)
• (q₁ ⊎ q₂).evaluateAnnotated hq_2 d = q₁.evaluateAnnotated ⋯ d + q₂.evaluateAnnotated ⋯ d
• (ε q_2).evaluateAnnotated hq_2 d = ↑↑(groupByKey (q_2.evaluateAnnotated ⋯ d))
• (Query.Agg a a_1 a_2 a_3).evaluateAnnotated hq_2 d = ⋯.elim

Home · Documentation · Publications · Contributors · Source · Cite