Documentation

Provenance.AggQueryEmbedding

The compositional JOIN rewriting, on the general syntax #

The HAVING COUNT(*) site of the compositional rewriting theorem is, in the general syntax, the key projection of σ_ψ ∘ Gamma – all-regular, since the projection drops the token columns – so it composes under every operator of the general syntax, and the ProvSQL-legal contexts around a site are exactly the expressible ones. GenCountHavingRewrite replaces such sites by the embedded padded join query (Query.toAgg, from Provenance.QueryToAgg), and GenCountHavingRewrite.evaluateGen_eq proves the replacement preserves the general evaluator's rows verbatim, in absorptive m-semirings whose ⊗ distributes over ⊖. The expressible contexts around a site are exactly the ProvSQL-legal ones: the kind discipline forbids deduplicating, differencing or re-grouping aggregate values, matching the system.

source
theorem tokenLists_eq_zero {T K : Type} {n : ℕ} {u : Tuple (GenValue T K) n} (h : ∀ (k : Fin n), ∃ (v : T), u k = Sum.inl v) :
tokenLists u = 0

A tuple with no token column has no token annotation lists.

Dependency graph
source
def genCountHavingSite (ts' : Tuple (Term ℕ 3) 1) (op : CompOp) (C : ℕ) (g : AggQuery ℕ 3 (ColKind.allReg 3)) :
AggQuery ℕ 1 (ColKind.allReg 1)

A HAVING COUNT(*) op (C + 1) site on the general syntax: the fused comparison over the grouping, projected to its group key – all-regular output.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    Dependency graph
    source
    theorem projTerm_row_eq {T : Type} [ValueType T] {K : Type} [CommSemiringWithMonus K] [DecidableEq K] {n m : ℕ} {κ : Fin n → ColKind} (ps : Tuple (ProjCol T κ) m) (hps : ∀ (j : Fin m), ∃ (t : TermG T κ), ps j = ProjCol.term t) (r : GenRow T K n) :
    (fun (j : Fin m) => (ps j).eval r.1, { base := r.2.base * (Multiset.map (fun (l : List K) => SemiringWithMonus.delta l.sum) (r.2.pending - r.2.pending ∩ tokenLists fun (j : Fin m) => (ps j).eval r.1)).prod, pending := r.2.pending ∩ tokenLists fun (j : Fin m) => (ps j).eval r.1 }) = GenRow.ofAnnotated (fun (j : Fin m) => AggValue.collapseSum ((ps j).eval r.1), r.2.finalize)

    A projection whose columns are all regular terms embeds each row: the token lists of the output are empty, so the pending guards are all cashed and the output annotation is the finalized input annotation.

    Dependency graph
    source
    theorem genCountHavingSite_eval {K : Type} [CommSemiringWithMonus K] [DecidableEq K] [HasAltLinearOrder K] (h_abs : absorptive K) (h_distrib : mul_sub_left_distributive K) (ts' : Tuple (Term ℕ 3) 1) (op : CompOp) (C : ℕ) (g : AggQuery ℕ 3 (ColKind.allReg 3)) (q' : Query ℕ 3) (hq' : q'.source) (d : AnnotatedDatabase ℕ K) (hbridge : g.evaluateAnnotated d = q'.evaluateAnnotated hq' d) (hnodup : (Multiset.map Prod.fst (q'.evaluateAnnotated hq' d)).Nodup) :
    (genCountHavingSite ts' op C g).evaluate d = ((joinCountQueryPadded q' op C).toAgg ⋯).evaluate d

    Site correctness on the general syntax: the general evaluator on a HAVING COUNT(*) site produces exactly the rows of the embedded padded join query – as raw evaluator rows, not just after finalization, since the key projection empties the pending guards on one side and the embedding image carries none on the other.

    Dependency graph
    source
    inductive GenCountHavingRewrite {K : Type} [CommSemiringWithMonus K] [DecidableEq K] [HasAltLinearOrder K] (d : AnnotatedDatabase ℕ K) {n : ℕ} {κ : Fin n → ColKind} :
    AggQuery ℕ n κ → AggQuery ℕ n κ → Prop

    The JOIN rewriting on the general syntax: congruence rules per operator, and the site rule replacing a HAVING COUNT(*) site by the embedded padded join query built over any classical query with the same annotated semantics as the site's grouped subquery.

    Instances For
      Dependency graph
      source
      theorem GenCountHavingRewrite.evaluateGen_eq {K : Type} [CommSemiringWithMonus K] [DecidableEq K] [HasAltLinearOrder K] (h_abs : absorptive K) (h_distrib : mul_sub_left_distributive K) {d : AnnotatedDatabase ℕ K} {n : ℕ} {κ : Fin n → ColKind} {q q' : AggQuery ℕ n κ} :
      GenCountHavingRewrite d q q' → q.evaluate d = q'.evaluate d

      Compositional correctness of the JOIN rewriting, general syntax: in an absorptive commutative m-semiring whose ⊗ distributes over ⊖, rewriting any number of HAVING COUNT(*) sites – wherever they occur – preserves the general evaluator's rows verbatim.

      Dependency graph
      source
      theorem GenCountHavingRewrite.evaluateAnnotatedGen_eq {K : Type} [CommSemiringWithMonus K] [DecidableEq K] [HasAltLinearOrder K] (h_abs : absorptive K) (h_distrib : mul_sub_left_distributive K) {d : AnnotatedDatabase ℕ K} {n : ℕ} {κ : Fin n → ColKind} {q q' : AggQuery ℕ n κ} (hrw : GenCountHavingRewrite d q q') :
      q.evaluateAnnotated d = q'.evaluateAnnotated d

      The finalized form of the compositional correctness.

      Dependency graph