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 anAnnotatedDatabase T K, propagating annotations through each relational operator according to the semiring structure ofK
References #
@[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 ⋯
Instances For
def
groupByKey
{T : Type}
[ValueType T]
{K : Type}
[SemiringWithMonus K]
[DecidableEq K]
{n : ℕ}
(m : Multiset (Tuple T n × K))
:
Equations
Instances For
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
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