Documentation

Provenance.QueryAggregationHom

Hom commutation for Query.evaluateAggSum #

For a SemiringWithMonusHom h : K → K', evaluating the aggregation operator under the pushforward of the annotated database h ⋆ d equals pushing the K-tensor coefficients of evaluateAggSum's output forward along h:

evaluateAggSum is ts q hq (h ⋆ d) =
  (evaluateAggSum is ts q hq d).map (push K-tensor along h)

This is the aggregation analogue of Query.evaluateAnnotated_hom (Green, Karvounarakis & Tannen, Provenance Semirings, Prop. 3.5, Geerts & Poggi, On database query languages for K-relations, Prop. 1) and continues the “compile once, evaluate many” theme of Sen, Maniu & Senellart, ProvSQL: a single K-annotated computation can be specialised to any concrete m-semiring K' through an m-semiring homomorphism, including for the aggregation operator and its K-tensor row annotations.

The proof reduces to (i) the existing Query.evaluateAnnotated_hom on the inner non-aggregating query and (ii) the observation that the pushforward of an annotated relation leaves the data side untouched and applies h.toRingHom to each annotation – which means group keys, matching predicates and aggregated data values are unaffected, while each K-tensor coefficient is mapped through h.

References #

source
def Query.mapAggSumRow {T K K' : Type} [CommSemiringWithMonus K] [CommSemiringWithMonus K'] (h : SemiringWithMonusHom K K') {n₁ n₂ : ℕ} (row : Tuple T n₁ × Tuple (T × KTensor K T) n₂) :
Tuple T n₁ × Tuple (T × KTensor K' T) n₂

The push-forward applied row-by-row to an evaluateAggSum output: the group-key stays untouched; for each aggregated column, the data value (Prod.fst) is preserved and the K-tensor (Prod.snd) is mapped through h.toRingHom on each monomial's K-coefficient.

Equations
Instances For
    source
    theorem Query.evaluateAggSum_hom {T : Type} [ValueType T] [AddCommSemigroup T] {K K' : Type} [CommSemiringWithMonus K] [CommSemiringWithMonus K'] [DecidableEq K] [DecidableEq K'] (h : SemiringWithMonusHom K K') {m n₁ n₂ : ℕ} (is : Tuple (Fin m) n₁) (ts : Tuple (Term T m) n₂) (q : Query T m) (hq : q.noAgg) (d : AnnotatedDatabase T K) :
    evaluateAggSum is ts q hq (h.mapAnnotatedDatabase d) = Multiset.map (mapAggSumRow h) (evaluateAggSum is ts q hq d)

    Aggregation hom commutation. For any SemiringWithMonusHom h : K → K' and any non-aggregating inner query q, evaluating the aggregation on h ⋆ d is the same as evaluating on d and then mapping each K-tensor coefficient through h.toRingHom. The aggregation operator therefore inherits the “compile once, evaluate many” property already established by Query.evaluateAnnotated_hom on the non-aggregating fragment.