Rewriting a bare grouping: aggregate results as output values

The HAVING site rewriting of Provenance.AggQueryHavingRewriting covers the case where the aggregate tokens of a grouping are consumed by a comparison gate and never leave the site. This module covers the complementary – and, in SQL, far more common – case: a bare GROUP BY whose aggregate columns flow onward as ordinary output columns.

Rule (R5) is the classical counterpart. Carrying it over the classical syntax took a whole new value domain – data, annotation and K-tensor monomials, quotiented – together with its own evaluator. In the general framework no new value domain is needed: the rewritten world's evaluator already has aggregate tokens as ordinary column values, and AggQuery.GammaTok – ProvSQL's provsql_agg – already materializes exactly the token that the general evaluator's Gamma produces. What was missing is the correspondence at token level: the statement of AggQuery.havingRewrites_valid folds an annotated relation into composite rows through AnnotatedRelation.toComposite, which reads tokens through their deterministic collapse and therefore cannot express a token-bearing output.

GenRow.toCompositeRow supplies that embedding: data columns go through Sum.inl, token columns are transported by AggValue.toComposite (values embedded in the composite domain, occurrence annotations unchanged), and the row's finalized annotation is appended as the provenance column. On token-free rows it agrees with the old embedding (GenRow.toCompositeRow_of_reg), so the statement below genuinely extends the compositional rewriting correctness rather than sitting beside it.

AggQuery.gammaRew_valid is then the (R5) analogue: for a classical subquery, the general evaluator's grouping – tokens and pending group-existence factor included – is computed by the rewritten token-building grouping over the classically rewritten subquery, with the group guard δ(⊕ U) landing in the provenance column.

Tokens in the composite domain

def AggValue.toComposite {T : Type} [ValueType T] {K : Type} (a : AggValue T K) : AggValue (T ⊕ K) K

Transport a symbolic aggregate token to the composite value domain: the aggregated values are embedded by Sum.inl, the aggregate function is lifted, and the occurrence annotations are unchanged.

Equations

• a.toComposite = { agg := a.agg.liftComposite, occs := List.map (fun (o : T × K) => (Sum.inl o.1, o.2)) a.occs }

theorem AggValue.ofGroup_toComposite {T : Type} [ValueType T] {K : Type} [CommSemiringWithMonus K] [HasAltLinearOrder K] {m : ℕ} (f : SeqAggFunc T) (t : Term T m) (U : List (AnnotatedTuple T K m)) : (ofGroup f t U).toComposite = ofGroup f.liftComposite t.castToAnnotatedTuple (List.map (fun (p : AnnotatedTuple T K m) => (p.toComposite, p.2)) U)

The token of a group transports to the token of the composite embedding of that group – the token the rewritten world's AggQuery.GammaTok builds.

def GenValue.toComposite {T : Type} [ValueType T] {K : Type} : GenValue T K → GenValue (T ⊕ K) K

Transport a lifted column value to the composite domain.

Equations

• GenValue.toComposite (Sum.inl v) = Sum.inl (Sum.inl v)
• GenValue.toComposite (Sum.inr a) = Sum.inr a.toComposite

def GenRow.toCompositeRow {T : Type} [ValueType T] {K : Type} [CommSemiringWithMonus K] {n : ℕ} (r : GenRow T K n) : Tuple (GenValue (T ⊕ K) K) (n + 1)

The token-aware composite embedding of a general row: every column transported to the composite domain, with the row's finalized annotation appended as the provenance column.

Equations

• r.toCompositeRow = Fin.append (fun (k : Fin n) => (r.1 k).toComposite) fun (x : Fin 1) => Sum.inl (Sum.inr r.2.finalize)

theorem GenRow.toCompositeRow_of_reg {T : Type} [ValueType T] {K : Type} [CommSemiringWithMonus K] {n : ℕ} (r : GenRow T K n) (hr : ∀ (k : Fin n), (r.1 k).kindOf = ColKind.reg) : r.toCompositeRow = fun (k : Fin (n + Nat.succ 0)) => Sum.inl (r.toAnnotated.toComposite k)

On token-free rows the token-aware embedding is the embedding used by the classical and HAVING-site rewriting correctness statements: the inl-image of the composite encoding of the finalized annotated tuple.

Coordinates of the token-aware embedding

@[simp]

theorem GenRow.toCompositeRow_castAdd {T : Type} [ValueType T] {K : Type} [CommSemiringWithMonus K] {n : ℕ} (r : GenRow T K n) (k : Fin n) : r.toCompositeRow (Fin.castAdd 1 k) = (r.1 k).toComposite

@[simp]

theorem GenRow.toCompositeRow_last {T : Type} [ValueType T] {K : Type} [CommSemiringWithMonus K] {n : ℕ} (r : GenRow T K n) : r.toCompositeRow (Fin.last n) = Sum.inl (Sum.inr r.2.finalize)

@[simp]

theorem AggValue.collapseSum_toComposite {T : Type} [ValueType T] {K : Type} (x : GenValue T K) : collapseSum x.toComposite = Sum.inl (collapseSum x)

The deterministic reading commutes with the token transport.

theorem GenRow.toCompositeRow_coord {T : Type} [ValueType T] {K : Type} [CommSemiringWithMonus K] {n : ℕ} (r : GenRow T K n) (j : Fin (n + 1)) : r.toCompositeRow j = if h : ↑j < n then (r.1 ⟨↑j, h⟩).toComposite else Sum.inl (Sum.inr r.2.finalize)

Coordinates of the token-aware embedding, in dite form.

theorem GenRow.toCompositeRow_gammaRow_left {T : Type} [ValueType T] {K : Type} [CommSemiringWithMonus K] {n₁ n₂ : ℕ} (g : Tuple T n₁) (h : Fin n₂ → AggValue T K) (a : GenAnn K) (i : Fin n₁) : toCompositeRow (Fin.append (fun (k : Fin n₁) => Sum.inl (g k)) fun (i' : Fin n₂) => Sum.inr (h i'), a) (Fin.castAdd 1 (Fin.castAdd n₂ i)) = Sum.inl (Sum.inl (g i))

A key column of the embedding of a grouping row.

theorem GenRow.toCompositeRow_gammaRow_right {T : Type} [ValueType T] {K : Type} [CommSemiringWithMonus K] {n₁ n₂ : ℕ} (g : Tuple T n₁) (h : Fin n₂ → AggValue T K) (a : GenAnn K) (i : Fin n₂) : toCompositeRow (Fin.append (fun (k : Fin n₁) => Sum.inl (g k)) fun (i' : Fin n₂) => Sum.inr (h i'), a) (Fin.castAdd 1 (Fin.natAdd n₁ i)) = Sum.inr (h i).toComposite

A token column of the embedding of a grouping row.

The rewritten bare grouping

@[reducible, inline]

abbrev ColKind.gammaRewKinds (n₁ n₂ : ℕ) : Fin (n₁ + n₂ + 1) → ColKind

The kind vector of a rewritten Gamma output: the group keys, the aggregate tokens, and the provenance column carrying the group guard.

Equations

• ColKind.gammaRewKinds n₁ n₂ = Fin.append (ColKind.gammaKinds n₁ n₂) fun (x : Fin 1) => ColKind.prov

theorem ColKind.gammaTok_rew_kinds {m n₁ n₂ : ℕ} (is : Tuple (Fin m) n₁) : (Fin.append (Fin.append (fun (k : Fin n₁) => rewKinds m (Fin.castLE ⋯ (is k))) fun (x : Fin n₂) => agg) fun (x : Fin 1) => prov) = gammaRewKinds n₁ n₂

The kind vector produced by the token-building grouping over a rewritten subquery is the rewritten Gamma kind vector: the key columns of a rewritten schema are regular.

def AggQuery.gammaRew {T : Type} [ValueType T] {K : Type} [CommSemiringWithMonus K] [HasAltLinearOrder K] {m n₁ n₂ : ℕ} (is : Tuple (Fin m) n₁) (ts : Tuple (Term T m) n₂) (fs : Tuple (SeqAggFunc T) n₂) (qg : AggQuery T m (ColKind.allReg m)) (hq : qg.classical) : AggQuery (T ⊕ K) (n₁ + n₂ + 1) (ColKind.gammaRewKinds n₁ n₂)

The rewritten bare grouping: ProvSQL's provsql_agg grouping over the classically rewritten subquery, reading the occurrence annotations off the subquery's provenance column. The output carries the group keys, one aggregate token per (term, aggregate) pair, and the group-existence guard δ(⊕ U) in the provenance column.

Equations

• One or more equations did not get rendered due to their size.

Correctness

theorem AggQuery.gammaRew_valid {T : Type} [ValueType T] {K : Type} [CommSemiringWithMonus K] [DecidableEq K] [HasAltLinearOrder K] {m n₁ n₂ : ℕ} (is : Tuple (Fin m) n₁) (ts : Tuple (Term T m) n₂) (fs : Tuple (SeqAggFunc T) n₂) (qg : AggQuery T m (ColKind.allReg m)) (hq : qg.classical) (d : AnnotatedDatabase T K) : Multiset.map GenRow.toCompositeRow ((Gamma is ts fs qg).evaluate d) = (gammaRew is ts fs qg hq).evaluateRew d.toComposite

Correctness of the bare-grouping rewriting – the general framework's rule (R5): for a classical subquery, the general evaluator's grouping, embedded row-wise into the composite domain (tokens included, finalized annotation appended), is computed by the rewritten world's token-building grouping over the classically rewritten subquery.

The gate reads a transported token unchanged

theorem AggValue.predProv_toComposite {T : Type} [ValueType T] {K : Type} [CommSemiringWithMonus K] [DecidableEq K] [HasAltLinearOrder K] (a : AggValue T K) (op : CompOp) (c : T) : a.toComposite.predProv op (Sum.inl c) = a.predProv op c

The predicate provenance under the token transport: comparing a transported token against an embedded value is the original comparison. The token transport preserves lengths and annotations, lifts the aggregate faithfully on embedded values, and comparisons restrict along inl.

Home · Documentation · Publications · Contributors · Source · Cite