A window over a whole partition is a join with its grouping

A window whose frame is the whole partition asks of each row exactly what a grouping asks of its group. It should therefore be expressible without a window at all: join every row with the group row of its own partition, and keep the group's aggregate column.

That is what this module proves, over plain relations and over annotated ones. The plain statement is a rearrangement. The annotated statement is not: the join carries the group's existence factor δ(⊕ U) into the row's annotation, which the window never produces, and the two agree only because the group of a row contains that row – so the factor reads α ⊗ δ(α ⊕ β'), which is α by δ-absorption. A frame that excluded the current row would have no such identity, and no such rewriting.

The join picks one group per row

theorem filter_product_key {α β γ : Type} [DecidableEq γ] (R : Multiset α) (key : α → γ) (Keys : Multiset γ) (hK : Keys.Nodup) (hmem : ∀ a ∈ R, key a ∈ Keys) (row : γ → β) (P' : α × β → Prop) (inst : DecidablePred P') (hP : ∀ (a : α) (g : γ), P' (a, row g) ↔ key a = g) : Multiset.filter P' (R.product (Multiset.map row Keys)) = Multiset.map (fun (a : α) => (a, row (key a))) R

Joining on a key picks out one entry per row. A table with distinct keys, joined with a relation on the key, gives each row exactly the entry of its own key – so the join has as many rows as the relation, one per row.

The window written as a join

The composite is the one of the semantics: join the query with its own grouping on the partition key, keep the original columns and the group's aggregate column.

@[reducible, inline]

abbrev AggQueryIn.winJoinKinds (n m : ℕ) : Fin (n + (m + 1)) → ColKind

The kind vector of a query joined with its grouping: the query's own columns, then the group key, then the aggregate token.

Equations

• AggQueryIn.winJoinKinds n m = Fin.append (ColKind.allReg n) (ColKind.gammaKinds m 1)

@[reducible, inline]

abbrev AggQueryIn.winLeftPos {n : ℕ} (m : ℕ) (k : Fin n) : Fin (n + (m + 1))

The position of an original column in the join.

Equations

• AggQueryIn.winLeftPos m k = Fin.castAdd (m + 1) k

@[reducible, inline]

abbrev AggQueryIn.winKeyPos {m : ℕ} (n : ℕ) (j : Fin m) : Fin (n + (m + 1))

The position of a group-key column in the join.

Equations

• AggQueryIn.winKeyPos n j = Fin.natAdd n (Fin.castAdd 1 j)

@[reducible, inline]

abbrev AggQueryIn.winAggPos (n m : ℕ) : Fin (n + (m + 1))

The position of the aggregate column in the join.

Equations

• AggQueryIn.winAggPos n m = Fin.natAdd n (Fin.natAdd m 0)

theorem AggQueryIn.winLeftPos_kind {n m : ℕ} (k : Fin n) : winJoinKinds n m (winLeftPos m k) = ColKind.reg

theorem AggQueryIn.winKeyPos_kind {n m : ℕ} (j : Fin m) : winJoinKinds n m (winKeyPos n j) = ColKind.reg

theorem AggQueryIn.winAggPos_kind {n m : ℕ} : winJoinKinds n m (winAggPos n m) = ColKind.agg

def AggQueryIn.winProj {T : Type} (n m : ℕ) : Tuple (ProjCol T (winJoinKinds n m)) (n + 1)

The projection keeping the original columns and the aggregate.

Equations

• AggQueryIn.winProj n m = Fin.snoc (fun (k : Fin n) => ProjColIn.term (TermGIn.index (AggQueryIn.winLeftPos m k) ⋯)) (ProjColIn.token (AggQueryIn.winAggPos n m) ⋯)

theorem AggQueryIn.winProj_kinds {T : Type} (n m : ℕ) : (fun (j : Fin (n + 1)) => ProjColIn.kind (winProj n m j)) = Fin.snoc (ColKind.allReg n) ColKind.agg

def AggQueryIn.winByJoin {T : Type} {n m : ℕ} [ValueType T] (P : Tuple (Fin n) m) (t : Term T n) (f : SeqAggFunc T) (q : AggQuery T n (ColKind.allReg n)) : AggQuery T (n + 1) (Fin.snoc (ColKind.allReg n) ColKind.agg)

A window over a whole partition, written without a window: join the query with its grouping on the partition key, and keep the group's aggregate column.

Equations

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

Over plain relations

Over annotated relations

Home · Documentation · Publications · Contributors · Source · Cite