Data-part adequacy of the general evaluator

Forgetting the annotations of the general annotated evaluation of a query yields the plain (classical) evaluation of the stripped query on the plain database:

(q.evaluateAnnotated d).toPlain = q.stripAgg.evaluatePlain d.toPlain

This generalizes Query.evaluateAnnotated_toPlain to the kind-indexed syntax. The stripping removes differences (annotated Diff never removes tuple slots) and aggregate-atom selections (the annotated evaluator keeps classically-failing rows annotated 𝟘, as ProvSQL emits them); on the remaining operators the data parts agree tuple for tuple, the aggregate tokens contributing through their deterministic collapse reading:

• terms, projection columns and predicates evaluated on a lifted tuple agree with their plain readings on the collapsed tuple (TermG.eval_eq_evalPlain, ProjCol.collapseSum_eval, GenPred.holds_iff_holdsPlain);
• the group sequence of the fused semantics projects onto the plain group sequence (havingGroup_map_fst): both are sorted lists of the same multiset of tuples, sorted by the same order on the tuple part – the annotation tie-break of havingGroup is invisible after projection;
• one output row of Gamma per group key, whose aggregate columns collapse to the plain aggregates of the whole group.

Plain readings through collapse

theorem TermG.eval_eq_evalPlain {T : Type} [ValueType T] {K : Type} {n : ℕ} {κ : Fin n → ColKind} (t : TermG T κ) (u : Tuple (GenValue T K) n) : t.eval u = t.evalPlain (GenRow.plainTuple u)

A term over regular columns evaluates on a lifted tuple as its plain reading on the collapsed tuple.

theorem ProjCol.collapseSum_eval {T : Type} [ValueType T] {K : Type} {n : ℕ} {κ : Fin n → ColKind} (p : ProjCol T κ) (u : Tuple (GenValue T K) n) : AggValue.collapseSum (p.eval u) = p.evalPlain (GenRow.plainTuple u)

A projection column collapses on a lifted tuple to its plain reading on the collapsed tuple.

theorem GenPred.holds_iff_holdsPlain {T : Type} [ValueType T] {K : Type} {n : ℕ} {κ : Fin n → ColKind} (φ : GenPred T κ) (u : Tuple (GenValue T K) n) : φ.holds u ↔ φ.holdsPlain (GenRow.plainTuple u)

A predicate holds on a lifted tuple iff its plain reading holds on the collapsed tuple.

@[simp]

theorem GenRow.plainTuple_ofAnnotated {T K : Type} {n : ℕ} (p : AnnotatedTuple T K n) : plainTuple (ofAnnotated p).1 = p.1

The collapsed tuple of an embedded annotated tuple is its data part.

theorem GenRow.plainTuple_append {T K : Type} {n₁ n₂ : ℕ} (g : Tuple T n₁) (h : Fin n₂ → AggValue T K) : plainTuple (Fin.append (fun (k : Fin n₁) => Sum.inl (g k)) fun (j : Fin n₂) => Sum.inr (h j)) = Fin.append g fun (j : Fin n₂) => (h j).collapse

Collapsing distributes over appending a regular and a token part.

theorem AggValue.collapse_ofGroup {T : Type} [ValueType T] {K : Type} {m : ℕ} (f : SeqAggFunc T) (t : Term T m) (U : List (AnnotatedTuple T K m)) : (ofGroup f t U).collapse = f (List.map (fun (p : AnnotatedTuple T K m) => t.eval p.1) U)

The collapse of a group token is the plain aggregate of the group's value sequence.

Multiset helpers

theorem product_map_map {α₁ α₂ β₁ β₂ : Type} (f : α₁ → β₁) (g : α₂ → β₂) (s : Multiset α₁) (t : Multiset α₂) : (Multiset.map f s).product (Multiset.map g t) = Multiset.map (fun (x : α₁ × α₂) => (f x.1, g x.2)) (s.product t)

theorem map_fst_groupByKey {T : Type} [ValueType T] {K : Type} [CommSemiringWithMonus K] [DecidableEq K] {n : ℕ} (r : AnnotatedRelation T K n) : Multiset.map Prod.fst ↑↑(groupByKey r) = (Multiset.map Prod.fst r).dedup

The keys of groupByKey are the deduplicated data parts (factored out of the Dedup case of Query.evaluateAnnotated_toPlain).

The group-sequence bridge

theorem havingGroup_map_fst {T : Type} [ValueType T] {K : Type} [CommSemiringWithMonus K] [HasAltLinearOrder K] {m n₁ : ℕ} (is : Tuple (Fin m) n₁) (r : AnnotatedRelation T K m) (g : Tuple T n₁) : List.map Prod.fst (Having.havingGroup is r g) = Relation.groupSeq is r.toPlain g

The data parts of the fused group sequence form the plain group sequence: both are lists of the same multiset of tuples, sorted by the canonical order on tuples – havingGroup's annotation tie-break is invisible after projection.

The adequacy theorem

theorem AggQuery.evaluateAnnotated_toPlain {T : Type} [ValueType T] {K : Type} [CommSemiringWithMonus K] [DecidableEq K] [HasAltLinearOrder K] {n : ℕ} {κ : Fin n → ColKind} (q : AggQuery T n κ) (d : AnnotatedDatabase T K) : (q.evaluateAnnotated d).toPlain = q.stripAgg.evaluatePlain d.toPlain

Data-part adequacy of the general evaluator. Forgetting the annotations of the general annotated evaluation yields the plain evaluation of the stripped query on the plain database.

Home · Documentation · Publications · Contributors · Source · Cite