Unified hom commutation for Query.evaluateAnnotatedFull

The single hom commutation theorem Query.evaluateAnnotatedFull_hom asserts that for any well-formed query q and any SemiringWithMonusHom h : K → K',

evaluateAnnotatedFull q hq (h ⋆ d) =
  (evaluateAnnotatedFull q hq d).map (mapAnnotatedFullRow h)

where mapAnnotatedFullRow h is the pointwise pushforward on a LiftedTK-tuple (data cells unchanged, ann α mapped through h, ktensor t mapped through KTensor.mapHom h.toRingHom).

This is the aggregation analogue of Query.evaluateAnnotated_hom (Green, Karvounarakis & Tannen, Provenance Semirings, Prop. 3.5) extended to the (R5) aggregation case, 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 h, including for aggregate queries with K-tensor row annotations.

The proof reduces:

• non-Agg cases to the existing Query.evaluateAnnotated_hom plus the bridge between AnnotatedRelation.toLifted and mapAnnotatedRelation (proven here);
• the Agg case is a direct argument mirroring Query.evaluateAggSum_hom but on the LiftedTK-valued output. The δ-applied row-annotation column is handled by the new map_delta field of SemiringWithMonusHom.

References

• Green, Karvounarakis & Tannen
• Geerts & Poggi
• Sen, Maniu & Senellart

Bridge: mapAnnotatedRelation and toLifted commute

theorem Query.AnnotatedRelation.toLifted_mapAnnotatedRelation {T K K' : Type} [CommSemiringWithMonus K] [CommSemiringWithMonus K'] {n : ℕ} (h : SemiringWithMonusHom K K') (ar : AnnotatedRelation T K n) : (h.mapAnnotatedRelation ar).toLifted = Multiset.map (fun (t : Tuple (LiftedTK T K) (n + 1)) (k : Fin (n + 1)) => LiftedTK.mapHomFn (⇑h.toRingHom) (t k)) ar.toLifted

The bridge between annotated-relation pushforward and toLifted: pushing h through and then lifting agrees with lifting and then applying mapHomFn h.toRingHom pointwise on each tuple cell.

Row-wise pushforward on evaluateAnnotatedFull output

def Query.mapAnnotatedFullRow {T K K' : Type} [CommSemiringWithMonus K] [CommSemiringWithMonus K'] (h : SemiringWithMonusHom K K') {n : ℕ} (row : Tuple (LiftedTK T K) n) : Tuple (LiftedTK T K') n

The row-wise pushforward applied to an evaluateAnnotatedFull output: each LiftedTK T K cell is mapped through LiftedTK.mapHomFn h.toRingHom.

Equations

• Query.mapAnnotatedFullRow h row k = LiftedTK.mapHomFn (⇑h.toRingHom) (row k)

Unified hom commutation theorem

theorem Query.evaluateAnnotatedFull_hom {T : Type} [ValueType T] [AddCommSemigroup T] [Zero T] {K K' : Type} [CommSemiringWithMonus K] [CommSemiringWithMonus K'] [DecidableEq K] [DecidableEq K'] (h : SemiringWithMonusHom K K') {n : ℕ} (q : Query T n) (hq : q.wellFormed) (d : AnnotatedDatabase T K) : q.evaluateAnnotatedFull hq (h.mapAnnotatedDatabase d) = Multiset.map (mapAnnotatedFullRow h) (q.evaluateAnnotatedFull hq d)

Unified hom commutation for Query.evaluateAnnotatedFull.

For any SemiringWithMonusHom h : K → K' and any well-formed query q (non-aggregating, or top-level aggregation with non-aggregating inner query), evaluating the unified annotated semantics on the pushforward h ⋆ d is the same as evaluating on d and then mapping each output row pointwise through LiftedTK.mapHomFn h.toRingHom.

This is the aggregation extension of the Green-Karvounarakis-Tannen hom commutation property (Prop. 3.5), and the unified counterpart of both Query.evaluateAnnotated_hom (non-Agg) and Query.evaluateAggSum_hom (Agg, separate output format).

Home · Documentation · Publications · Contributors · Source · Cite