Symbolic aggregate tokens

AggValue T K is the symbolic aggregate token of the general HAVING semantics: an aggregate function together with the ≼-sorted occurrence payload of the originating group, projected to pairs (value of the aggregated term, occurrence annotation) – exactly the data of Having.havingGroup that the possible-world semantics of an aggregate comparison consumes. It is the one-level analogue of KTensor (deliberately un-quotiented, so the possible worlds of the group can be read off the token); there is no recursion: ProvSQL rejects aggregation, grouping and ordering over aggregate values, and likewise rejects deduplication and difference on token-carrying relations, so no linear order or decidable equality on tokens is required by any permitted downstream operator (SeqAggFunc being a function type, structural decidable equality would not be available anyway).

Readings of a token

• valOn – the aggregate value in one possible world of the group, matching Having.aggValOn on the originating group (valOn_ofGroup);
• specialize – the world-faithful reading: restrict to the occurrences whose annotation is realized by a valuation and aggregate those;
• collapse – the deterministic reading: aggregate the whole sequence. This is the value ProvSQL displays for an uncompared aggregate (the actual-world value, rendered v (*)), and the reading through which the data-part adequacy of the general evaluator is stated;
• predProv – the predicate provenance of a comparison against the token: the ⊕-sum, over the non-empty possible worlds of the group, of the world annotation times the characteristic value of the comparison. On a token built from a group it coincides with the fused semantics' Having.havingProv (predProv_ofGroup) – the seed of the regression bridge between the general and the fused evaluators.

mapAnn pushes a function K → K' through the annotations of a token: value-only readings are unchanged (collapse_mapAnn) and specialize composes with the pushforward (specialize_mapAnn). This is the token layer of the hom-commutation metatheorem for the general evaluator.

Lifted column values

A column of a token-carrying relation holds either a regular value or a token: T ⊕ AggValue T K. AggValue.mapAnnSum and AggValue.collapseSum extend the pushforward and the deterministic reading to such lifted values; the kind-indexed syntax of the general evaluator governs statically which columns hold which arm.

structure AggValue (T K : Type) : Type

A symbolic aggregate token: an aggregate function together with the (≼-sorted) occurrence payload of the originating group – for each occurrence, the value of the aggregated term paired with the occurrence annotation.

• agg : SeqAggFunc T

  The sequence aggregate applied by every reading of the token.

• occs : List (T × K)

  The occurrence payload: values of the aggregated term paired with the occurrence annotations, in the group's ≼-order.

def AggValue.ofGroup {T K : Type} {m : ℕ} [ValueType T] (f : SeqAggFunc T) (t : Term T m) (U : List (AnnotatedTuple T K m)) : AggValue T K

The token of a group with occurrence sequence U, aggregating the term t with f: the projection of the group payload.

Equations

• AggValue.ofGroup f t U = { agg := f, occs := List.map (fun (p : AnnotatedTuple T K m) => (t.eval p.1, p.2)) U }

def AggValue.anns {T K : Type} (a : AggValue T K) : Fin a.occs.length → K

The occurrence annotations of a token, as a function on positions.

Equations

• a.anns i = (a.occs.get i).2

def AggValue.valOn {T K : Type} (a : AggValue T K) (W : Finset (Fin a.occs.length)) : T

The aggregate value of the token in the possible world W of its group: the aggregate of the values of the kept occurrences, in order.

Equations

• a.valOn W = a.agg (List.map Prod.fst (Having.seqOf a.occs W))

def AggValue.collapse {T K : Type} (a : AggValue T K) : T

The deterministic reading: the aggregate of the whole occurrence sequence.

Equations

• a.collapse = a.agg (List.map Prod.fst a.occs)

def AggValue.specialize {T K : Type} (a : AggValue T K) (ν : K → Bool) : T

The world-faithful reading under a valuation ν of the annotations: restrict to the occurrences whose annotation ν realizes, and aggregate those in order.

Equations

• a.specialize ν = a.agg (List.map Prod.fst (List.filter (fun (o : T × K) => ν o.2) a.occs))

def AggValue.mapAnn {T K K' : Type} (h : K → K') (a : AggValue T K) : AggValue T K'

Pushforward of h : K → K' through the annotations of a token; the values are untouched.

Equations

• AggValue.mapAnn h a = { agg := a.agg, occs := List.map (fun (o : T × K) => (o.1, h o.2)) a.occs }

def AggValue.predProv {T K : Type} [ValueType T] [CommSemiringWithMonus K] [DecidableEq K] (a : AggValue T K) (op : CompOp) (c : T) : K

Predicate provenance of an atomic comparison against a token: the ⊕-sum, over the non-empty possible worlds of the token's group, of the world annotation times the characteristic value of the comparison between the world's aggregate value and the regular value c. Non-empty worlds only: the predicate provenance already enforces group existence, exactly as in the fused semantics Having.havingProv.

Equations

• a.predProv op c = ∑ W : Finset (Fin a.occs.length) with W.Nonempty, Having.worldAnn a.anns W * Having.chi op (a.valOn W) c

Reindexing bridges

The occurrence payload of ofGroup is a List.map image of the group sequence, so worlds over the token and worlds over the group live over propositionally – not definitionally – equal position types. The bridges below transport seqOf, worldAnn and the two readings along the length-preserving equivalence finCongr.

theorem AggValue.seqOf_map {β γ : Type} (g : β → γ) (U : List β) (h : U.length = (List.map g U).length) (W : Finset (Fin U.length)) : Having.seqOf (List.map g U) (Finset.map (finCongr h).toEmbedding W) = List.map g (Having.seqOf U W)

seqOf commutes with mapping the underlying list, up to reindexing the world along the length equality.

theorem AggValue.seqOf_univ {β : Type} (U : List β) : Having.seqOf U Finset.univ = U

The whole-sequence world: seqOf over univ is the identity.

theorem AggValue.filter_eq_seqOf {β : Type} (p : β → Bool) (U : List β) : List.filter p U = Having.seqOf U {i : Fin U.length | p (U.get i) = true}

Filtering a list is taking the subsequence of the positions whose element satisfies the predicate.

The readings, related

theorem AggValue.collapse_eq_valOn_univ {T K : Type} (a : AggValue T K) : a.collapse = a.valOn Finset.univ

collapse is the aggregate value of the whole-group world.

theorem AggValue.specialize_eq_valOn {T K : Type} (a : AggValue T K) (ν : K → Bool) : a.specialize ν = a.valOn {i : Fin a.occs.length | ν (a.anns i) = true}

specialize is the aggregate value of the world of realized occurrences.

ofGroup bridges to the fused semantics

theorem AggValue.length_ofGroup_occs {T K : Type} {m : ℕ} [ValueType T] (f : SeqAggFunc T) (t : Term T m) (U : List (AnnotatedTuple T K m)) : U.length = (ofGroup f t U).occs.length

The occurrence payload of ofGroup has the length of the group sequence.

theorem AggValue.valOn_ofGroup {T K : Type} {m : ℕ} [ValueType T] (f : SeqAggFunc T) (t : Term T m) (U : List (AnnotatedTuple T K m)) (W : Finset (Fin U.length)) : (ofGroup f t U).valOn (Finset.map (finCongr ⋯).toEmbedding W) = Having.aggValOn U t f W

The world value of the token of a group is the aggregate value of the fused semantics on that world.

theorem AggValue.anns_ofGroup {T K : Type} {m : ℕ} [ValueType T] (f : SeqAggFunc T) (t : Term T m) (U : List (AnnotatedTuple T K m)) (i : Fin U.length) : (ofGroup f t U).anns ((finCongr ⋯) i) = (U.get i).2

The annotations of the token of a group are the occurrence annotations.

theorem AggValue.worldAnn_map_finCongr {K : Type} [CommSemiringWithMonus K] {N M : ℕ} (h : N = M) (α : Fin M → K) (W : Finset (Fin N)) : Having.worldAnn α (Finset.map (finCongr h).toEmbedding W) = Having.worldAnn (fun (i : Fin N) => α ((finCongr h) i)) W

The world annotation transports along the reindexing.

theorem AggValue.predProv_ofGroup {T K : Type} {m : ℕ} [ValueType T] [CommSemiringWithMonus K] [DecidableEq K] (f : SeqAggFunc T) (t : Term T m) (U : List (AnnotatedTuple T K m)) (op : CompOp) (c : T) : (ofGroup f t U).predProv op c = Having.havingProv U t f op c

Regression bridge, token side. The predicate provenance of a comparison against the token of a group is the fused semantics' predicate provenance of the same comparison on that group.

Pushforward lemmas

@[simp]

theorem AggValue.collapse_mapAnn {T K K' : Type} (h : K → K') (a : AggValue T K) : (mapAnn h a).collapse = a.collapse

The deterministic reading is unchanged by the pushforward.

@[simp]

theorem AggValue.specialize_mapAnn {T K K' : Type} (h : K → K') (a : AggValue T K) (ν : K' → Bool) : (mapAnn h a).specialize ν = a.specialize fun (k : K) => ν (h k)

The world-faithful reading composes with the pushforward.

Lifted column values

def AggValue.mapAnnSum {T K K' : Type} (h : K → K') : T ⊕ AggValue T K → T ⊕ AggValue T K'

Pushforward of h : K → K' on a lifted column value: data is untouched, a token maps its annotations.

Equations

• AggValue.mapAnnSum h = Sum.map id (AggValue.mapAnn h)

def AggValue.collapseSum {T K : Type} : T ⊕ AggValue T K → T

Deterministic reading of a lifted column value: data is itself, a token collapses.

Equations

• AggValue.collapseSum = Sum.elim id AggValue.collapse

@[simp]

theorem AggValue.collapseSum_mapAnnSum {T K K' : Type} (h : K → K') (x : T ⊕ AggValue T K) : collapseSum (mapAnnSum h x) = collapseSum x

The deterministic reading of a lifted value is unchanged by the pushforward.

Home · Documentation · Publications · Contributors · Source · Cite