Decorrelation: an apply read as a product

An apply evaluates its right side once per row of its left side, with that row's values filled in for the parameters. Nothing is lost by forbidding it: every query is equivalent to one whose applies are products. The construction is that of Galindo-Legaria & Joshi, Orthogonal Optimization of Subqueries and Aggregation, in the form AggQueryIn.hasDecorrelation_of_usesOnly states: given a parameter relation P whose rows are pairwise distinct, a query q reading P's columns as parameters is turned into a closed query D_P(q) over the parameters and q's own columns together, so that

D_P(q) = ⊎_{v ∈ P} {v} × q[v],

which is the apply of P and q. Every operator inside carries the parameter columns along: a selection on a parameter becomes one on a column, a grouping or a window gains the parameters in its key or partition, and an apply recurses with the distinct rows of its own left side as the parameter relation.

This file carries the first half: lifting the parameters of a term, a predicate or a projection column into columns of the decorrelated query. A term's outer column j becomes the column j of the result, a column i of its own becomes the column c + i, and the reading is unchanged (TermGIn.evalPlain_lift).

@[reducible, inline]

abbrev ColKind.liftKinds (c : ℕ) {k : ℕ} (κ : Fin k → ColKind) : Fin (c + k) → ColKind

The kinds of a decorrelated query: the parameters first, which are regular columns, then the query's own.

Equations

• ColKind.liftKinds c κ = Fin.append (ColKind.allReg c) κ

theorem ColKind.liftKinds_param (c : ℕ) {k : ℕ} (κ : Fin k → ColKind) (j : Fin c) : liftKinds c κ (Fin.castAdd k j) = reg

A parameter column of the decorrelated query is regular.

theorem ColKind.liftKinds_col (c : ℕ) {k : ℕ} (κ : Fin k → ColKind) (i : Fin k) : liftKinds c κ (Fin.natAdd c i) = κ i

And a column of the query's own keeps its kind.

Lifting a term

def TermIn.lift {T : Type} {c k : ℕ} : TermIn T c k → TermIn T 0 (c + k)

A term with its parameters read as columns: the outer column j becomes the column j, and the term's own column i becomes the column c + i.

Equations

• (TermIn.const a).lift = TermIn.const a
• (TermIn.outer j).lift = #(Fin.castAdd k j)
• (#i).lift = #(Fin.natAdd c i)
• (t₁.add t₂).lift = t₁.lift.add t₂.lift
• (t₁.sub t₂).lift = t₁.lift.sub t₂.lift
• (t₁.mul t₂).lift = t₁.lift.mul t₂.lift
• (TermIn.caseWhen op t₁ t₂ t₃ t₄).lift = TermIn.caseWhen op t₁.lift t₂.lift t₃.lift t₄.lift
• (t₁.coalesce t₂).lift = t₁.lift.coalesce t₂.lift

Lifting a general term

def TermGIn.lift {T : Type} {c k : ℕ} {κ : Fin k → ColKind} : TermGIn T c κ → TermGIn T 0 (ColKind.liftKinds c κ)

A general term with its parameters read as columns.

Equations

• (TermGIn.const a).lift = TermGIn.const a
• (TermGIn.outer j).lift = TermGIn.index (Fin.castAdd k j) ⋯
• (TermGIn.index i h).lift = TermGIn.index (Fin.natAdd c i) ⋯
• (TermGIn.provIndex i h).lift = TermGIn.provIndex (Fin.natAdd c i) ⋯
• (TermGIn.cmpAgg i h op t).lift = TermGIn.cmpAgg (Fin.natAdd c i) ⋯ op t.lift
• (TermGIn.chiGate op t₁ t₂).lift = TermGIn.chiGate op t₁.lift t₂.lift
• (t₁.add t₂).lift = t₁.lift.add t₂.lift
• (t₁.sub t₂).lift = t₁.lift.sub t₂.lift
• (t₁.mul t₂).lift = t₁.lift.mul t₂.lift
• (TermGIn.caseWhen op t₁ t₂ t₃ t₄).lift = TermGIn.caseWhen op t₁.lift t₂.lift t₃.lift t₄.lift
• (t₁.coalesce t₂).lift = t₁.lift.coalesce t₂.lift

theorem TermGIn.evalPlain_lift {T : Type} [ValueType T] {c k : ℕ} {κ : Fin k → ColKind} (t : TermGIn T c κ) (v : Tuple T c) (w : Tuple T k) : t.lift.evalPlain (Fin.append v w) = t.evalPlain w v

Lifting does not change what a general term reads.

Lifting a predicate and a projection column

def GenPredIn.lift {T : Type} {c k : ℕ} {κ : Fin k → ColKind} : GenPredIn T c κ → GenPred T (ColKind.liftKinds c κ)

A predicate with its parameters read as columns.

Equations

• (GenPredIn.cmp op t₁ t₂).lift = GenPredIn.cmp op t₁.lift t₂.lift
• (GenPredIn.aggCmp i h op t).lift = GenPredIn.aggCmp (Fin.natAdd c i) ⋯ op t.lift
• (GenPredIn.aggRange i h op₁ t₁ op₂ t₂).lift = GenPredIn.aggRange (Fin.natAdd c i) ⋯ op₁ t₁.lift op₂ t₂.lift
• (φ.and ψ).lift = GenPredIn.and φ.lift ψ.lift
• (φ.or ψ).lift = GenPredIn.or φ.lift ψ.lift
• φ.not.lift = GenPredIn.not φ.lift

def ProjColIn.lift {T : Type} {c k : ℕ} {κ : Fin k → ColKind} : ProjColIn T c κ → ProjCol T (ColKind.liftKinds c κ)

A projection column with its parameters read as columns.

Equations

• (ProjColIn.term t).lift = ProjColIn.term t.lift
• (ProjColIn.token i h).lift = ProjColIn.token (Fin.natAdd c i) ⋯
• (ProjColIn.aggTerm i h gf).lift = ProjColIn.aggTerm (Fin.natAdd c i) ⋯ gf
• (ProjColIn.aggTermOf i h gf).lift = ProjColIn.aggTermOf (Fin.natAdd c i) ⋯ gf
• (ProjColIn.provTerm t).lift = ProjColIn.provTerm t.lift

Slices: what a decorrelated query computes

A decorrelated query holds, for each row v of the parameter relation, a slice: the rows of q[v] with v in front. Everything below is read off that shape, and the operators of the algebra act slice by slice – which is why the construction can push them through. The parameter rows being pairwise distinct is what makes the slices disjoint, and so is needed exactly where an operator compares whole rows: ε and −.

def Relation.slices {T : Type} {c k : ℕ} (P : Multiset (Tuple T c)) (f : Tuple T c → Multiset (Tuple T k)) : Multiset (Tuple T (c + k))

The slices of a parameter relation: for each v ∈ P, the rows f v with v in front.

Equations

• Relation.slices P f = P.bind fun (v : Tuple T c) => Multiset.map (fun (w : Fin k → T) => Fin.append v w) (f v)

The parameter join

Two decorrelated queries over the same parameters are put side by side by a product, a selection matching their parameter blocks, and a projection keeping one copy of the parameters. This is the step that turns an apply into a product, and the one that needs the parameter rows to be pairwise distinct: a repeated row would pair the copies of its own slice with each other.

def Relation.paramsOf {T : Type} {c k : ℕ} (x : Tuple T (c + k)) : Tuple T c

The parameters a row of a decorrelated query carries.

Equations

• Relation.paramsOf x j = x (Fin.castAdd k j)

def Relation.joinParams {T : Type} {c k₁ k₂ : ℕ} (x : Tuple T (c + k₁ + (c + k₂))) : Prop

The condition the parameter join selects on: the two parameter blocks agree.

Equations

• Relation.joinParams x = ∀ (j : Fin c), x (Fin.castAdd (c + k₂) (Fin.castAdd k₁ j)) = x (Fin.natAdd (c + k₁) (Fin.castAdd k₂ j))

@[instance_reducible]

instance instDecidableJoinParams {T : Type} [ValueType T] {c k₁ k₂ : ℕ} (x : Tuple T (c + k₁ + (c + k₂))) : Decidable (Relation.joinParams x)

Equations

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

def Relation.joinCols {T : Type} {c k₁ k₂ : ℕ} (x : Tuple T (c + k₁ + (c + k₂))) : Tuple T (c + (k₁ + k₂))

The columns the parameter join keeps: the parameters once, then each side's own columns.

Equations

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

theorem Relation.filter_paramsOf_slices {T : Type} [ValueType T] {c k : ℕ} (P : Multiset (Tuple T c)) (hP : P.Nodup) (g : Tuple T c → Multiset (Tuple T k)) {v : Tuple T c} (hv : v ∈ P) : Multiset.filter (fun (b : Tuple T (c + k)) => paramsOf b = v) (slices P g) = Multiset.map (fun (w : Fin k → T) => Fin.append v w) (g v)

The rows of one slice, read off the slices by their parameters: with the parameter rows distinct, the rows carrying v are exactly that slice's.

What a decorrelated query is, and the cases of the construction

The claim is one statement per operator: given decorrelations of the subqueries over the same parameter relation, build one for the whole. Each case is a lemma below, and the induction that assembles them is at the end. Nothing here needs a castKind: the kind vector of the decorrelated query is whatever the construction produces, and what is claimed of it is an equality of plain semantics.

def basisOps : Set OpKind

The six classes of the basis: the empty relation, the generalized projection, the selection, the product, the union and the aggregation. The other four classes the plain semantics grades – duplicate elimination, the difference, the apply and the window – are each expressible in these, which is what Provenance.BasisAssembly proves.

Equations

• basisOps = {OpKind.empty, OpKind.proj, OpKind.sel, OpKind.prod, OpKind.union, OpKind.gamma}

def decorrOps : Set OpKind

The classes the construction needs beyond the ones the query already uses: it pairs the parameters with a leaf (×) and may have to spell the empty relation (∅), it projects the columns into place (Π), it matches the parameter blocks of a product (σ), it reads the distinct rows of an apply's left side (ε), and it recovers the parameter rows a scalar aggregation's slices do not reach (⊎, −).

The classification needs this to be precise: the target set is a parameter so that a query with no window decorrelates to one with no window, which is what lets the passes be composed.

Equations

• decorrOps = {OpKind.empty, OpKind.proj, OpKind.sel, OpKind.prod, OpKind.union, OpKind.dedup, OpKind.diff}

def decorrCore : Set OpKind

The classes every decorrelation needs: the selection and the duplicate elimination are needed only for a product or an apply, whose decorrelations match parameter blocks and read the distinct rows of a left side.

Equations

• decorrCore = {OpKind.empty, OpKind.proj, OpKind.prod, OpKind.union, OpKind.diff}

def AggQueryIn.paramsReg {T : Type} {c n : ℕ} {κ : Fin n → ColKind} {l : List (String × ℕ)} : AggQueryIn T c n κ l → Prop

Every parameter leaf is regular: what keeps a decorrelation in the signature, a leaf with an aggregate column being rebuilt by an aggregate that reads the one value of its group.

Equations

• (AggQueryIn.Rel x✝ a).paramsReg = True
• (AggQueryIn.Hole x✝¹ s x✝).paramsReg = True
• (AggQueryIn.Param pv x✝).paramsReg = ∀ (k : Fin x✝¹), x✝ k = ColKind.reg
• AggQueryIn.Empty.paramsReg = True
• (AggQueryIn.Proj ps q).paramsReg = q.paramsReg
• (AggQueryIn.Sel φ q hφ).paramsReg = q.paramsReg
• (q₁.Prod q₂).paramsReg = (q₁.paramsReg ∧ q₂.paramsReg)
• (q₁.Apply q₂).paramsReg = (q₁.paramsReg ∧ q₂.paramsReg)
• (q₁.Sum q₂).paramsReg = (q₁.paramsReg ∧ q₂.paramsReg)
• q.Dedup.paramsReg = q.paramsReg
• (q₁.Diff q₂).paramsReg = (q₁.paramsReg ∧ q₂.paramsReg)
• (AggQueryIn.Explode k a q).paramsReg = q.paramsReg
• (AggQueryIn.Retag h q).paramsReg = q.paramsReg
• (AggQueryIn.Mu s q₀ q₁).paramsReg = (q₀.paramsReg ∧ q₁.paramsReg)
• (AggQueryIn.MuSet s q₀ q₁).paramsReg = (q₀.paramsReg ∧ q₁.paramsReg)
• (AggQueryIn.Gamma is ts fs q keep ord).paramsReg = q.paramsReg
• (AggQueryIn.GammaScalar ts fs q ord).paramsReg = q.paramsReg
• (AggQueryIn.GammaNest is his p f q).paramsReg = q.paramsReg
• (AggQueryIn.ProvSum is his t q).paramsReg = q.paramsReg
• (AggQueryIn.GammaTok is his ts fs a q keep).paramsReg = q.paramsReg
• (AggQueryIn.Win P O o w t f q a dist keep).paramsReg = q.paramsReg
• (AggQueryIn.WinExpr P O o ws ts fs g q_1 keeps).paramsReg = q_1.paramsReg

def AggQueryIn.DecorrelatesTo {T : Type} [ValueType T] {c k : ℕ} {κ : Fin k → ColKind} {l : List (String × ℕ)} {κ' : Fin (c + k) → ColKind} (P : AggQuery T c (ColKind.allReg c)) (q : AggQueryIn T c k κ l) (q' : AggQueryIn T 0 (c + k) κ' l) : Prop

A decorrelation of q over the parameter relation P: a closed query whose rows are the slices, one per row of P, holding what q gives under that row.

Equations

• AggQueryIn.DecorrelatesTo P q q' = ∀ (D : Database T), q'.evaluatePlain D = Relation.slices (AggQueryIn.evaluatePlain P D) fun (v : Tuple T c) => q.evaluatePlain D v

def AggQueryIn.HasDecorrelation {T : Type} [ValueType T] {c k : ℕ} {κ : Fin k → ColKind} {l : List (String × ℕ)} (S : Set OpKind) (sch : Schema) (P : AggQuery T c (ColKind.allReg c)) (q : AggQueryIn T c k κ l) : Prop

q has a decorrelation over P using no apply. Its columns are the parameters and q's own, with the kinds they have: that the kind vector is exactly the lifted one is what lets a selection's predicate, a union's two sides and a difference's be put over it.

Equations

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

The leaves

def headAgg {T : Type} [ValueType T] : SeqAggFunc T

The first value of a sequence: what an aggregate over a group of one row reads of it.

Equations

• headAgg L = L.headD 0

def pvTerm {T : Type} {c : ℕ} : T ⊕ Fin c → TermIn T 0 c

A parameter or a constant, as a term over the parameter relation.

Equations

• pvTerm = Sum.elim TermIn.const TermIn.index

@[reducible, inline]

abbrev paramGammaKinds (c m : ℕ) : Fin (c + m) → ColKind

The kinds of the grouping that rebuilds a parameter leaf.

Equations

• paramGammaKinds c m = Fin.append (fun (x : Fin c) => ColKind.reg) fun (x : Fin m) => ColKind.agg

def pvTermG {T : Type} {c m : ℕ} : T ⊕ Fin c → TermGIn T 0 (paramGammaKinds c m)

A parameter or a constant, as a regular term over that grouping.

Equations

• pvTermG = Sum.elim TermGIn.const fun (j : Fin c) => TermGIn.index (Fin.castAdd m j) ⋯

def paramCol {T : Type} {c m : ℕ} (pv : Fin m → T ⊕ Fin c) (ρ : Fin m → ColKind) (k : Fin m) : ProjColIn T 0 (paramGammaKinds c m)

The column k of the rebuilt leaf: the aggregate column the grouping built for it where the leaf says aggregate, the parameter itself otherwise.

Equations

• paramCol pv ρ k = match ρ k with | ColKind.reg => ProjColIn.term (pvTermG (pv k)) | ColKind.agg => ProjColIn.token (Fin.natAdd c k) ⋯ | ColKind.prov => ProjColIn.provTerm (pvTermG (pv k))

def paramCols {T : Type} {c m : ℕ} (pv : Fin m → T ⊕ Fin c) (ρ : Fin m → ColKind) : Fin (c + m) → ProjColIn T 0 (paramGammaKinds c m)

The columns of the rebuilt leaf: the parameter row, then its own.

Equations

• paramCols pv ρ i = Fin.addCases (fun (j : Fin c) => ProjColIn.term (TermGIn.index (Fin.castAdd m j) ⋯)) (paramCol pv ρ) i

def paramColsReg {T : Type} {c m : ℕ} (pv : Fin m → T ⊕ Fin c) : Fin (c + m) → ProjColIn T 0 (ColKind.allReg c)

The columns of a regular parameter leaf, read off a parameter row.

Equations

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

The operators that act slice by slice

The product: a join on the parameters

Two decorrelations over the same parameters are put side by side by a product, a selection matching their parameter blocks and a projection keeping one copy of them. The projection copies each column as its kind asks (AggQueryIn.carryCol), so aggregate and provenance columns are carried through as well.

def joinSrc (c k₁ k₂ : ℕ) : Fin (c + (k₁ + k₂)) → Fin (c + k₁ + (c + k₂))

Where each column of the parameter join reads from.

Equations

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

The operators the plain semantics does not see

Shifting a closed term over the parameter block

A window's FILTER clause is a selection on its input's columns, and the decorrelated window's input has the parameters before them. The clause therefore has to read the column c + i where it read the column i; it reads no parameter, having none to read.

def TermIn.shift {T : Type} (c : ℕ) {c' k : ℕ} : TermIn T c' k → TermIn T c' (c + k)

A term reading the columns of the decorrelated query's own half: the column i becomes the column c + i. Unlike TermIn.lift this leaves the outer columns alone – it shifts a term's reading, where lift closes it.

Equations

• TermIn.shift c (TermIn.const a) = TermIn.const a
• TermIn.shift c (TermIn.outer j) = TermIn.outer j
• TermIn.shift c #i = #(Fin.natAdd c i)
• TermIn.shift c (t₁.add t₂) = (TermIn.shift c t₁).add (TermIn.shift c t₂)
• TermIn.shift c (t₁.sub t₂) = (TermIn.shift c t₁).sub (TermIn.shift c t₂)
• TermIn.shift c (t₁.mul t₂) = (TermIn.shift c t₁).mul (TermIn.shift c t₂)
• TermIn.shift c (TermIn.caseWhen op t₁ t₂ t₃ t₄) = TermIn.caseWhen op (TermIn.shift c t₁) (TermIn.shift c t₂) (TermIn.shift c t₃) (TermIn.shift c t₄)
• TermIn.shift c (t₁.coalesce t₂) = (TermIn.shift c t₁).coalesce (TermIn.shift c t₂)

def BoolTerm.shift {T : Type} (c : ℕ) {k : ℕ} : BoolTerm T k → BoolTerm T (c + k)

A comparison on the shifted columns.

Equations

• BoolTerm.shift c (BoolTerm.EQ a b) = BoolTerm.EQ (TermIn.shift c a) (TermIn.shift c b)
• BoolTerm.shift c (BoolTerm.NE a b) = BoolTerm.NE (TermIn.shift c a) (TermIn.shift c b)
• BoolTerm.shift c (BoolTerm.LE a b) = BoolTerm.LE (TermIn.shift c a) (TermIn.shift c b)
• BoolTerm.shift c (BoolTerm.LT a b) = BoolTerm.LT (TermIn.shift c a) (TermIn.shift c b)
• BoolTerm.shift c (BoolTerm.GE a b) = BoolTerm.GE (TermIn.shift c a) (TermIn.shift c b)
• BoolTerm.shift c (BoolTerm.GT a b) = BoolTerm.GT (TermIn.shift c a) (TermIn.shift c b)
• BoolTerm.shift c (BoolTerm.SYNEQ a b) = BoolTerm.SYNEQ (TermIn.shift c a) (TermIn.shift c b)
• BoolTerm.shift c (BoolTerm.SYNNE a b) = BoolTerm.SYNNE (TermIn.shift c a) (TermIn.shift c b)

def Selection.shift {T : Type} (c : ℕ) {k : ℕ} : Selection T k → Selection T (c + k)

A selection on the shifted columns.

Equations

• Selection.shift c (Selection.BT b) = Selection.BT (BoolTerm.shift c b)
• Selection.shift c φ.Not = (Selection.shift c φ).Not
• Selection.shift c (φ₁.And φ₂) = (Selection.shift c φ₁).And (Selection.shift c φ₂)
• Selection.shift c (φ₁.Or φ₂) = (Selection.shift c φ₁).Or (Selection.shift c φ₂)
• Selection.shift c Selection.True = Selection.True

theorem Selection.keeps_shift {T : Type} [ValueType T] (c : ℕ) {k : ℕ} (φ : Selection T k) (v : Tuple T c) (u : Tuple T k) : (shift c φ).keeps (Fin.append v u) = φ.keeps u

It keeps the same rows.

Groups: the parameters join the key

An aggregation of the decorrelated query groups by the parameters as well as by its own key columns, so each group is one slice's group. The rows of that group are the slice's with the parameters in front, which is what the aggregates then read.

def winOrd (c : ℕ) {k p : ℕ} (O : Tuple (Fin k) p) : Tuple (Fin (c + k)) p

The order columns, shifted.

Equations

• winOrd c O i = Fin.natAdd c (O i)

theorem OrderSpec.readLe_append {T : Type} [ValueType T] {c k p : ℕ} (O : Tuple (Fin k) p) (o : OrderSpec p) (v : Tuple T c) (x y : Tuple T k) : readLe (winOrd c O).key id o (Fin.append v x) (Fin.append v y) = readLe O.key id o x y

The clause reads a prefixed pair as it reads the pair: the order values are the same, and the ties it leaves are broken by the rows, which a common prefix does not reorder.

def groupKey (c : ℕ) {m n₁ : ℕ} (is : Tuple (Fin m) n₁) : Tuple (Fin (c + m)) (c + n₁)

The key columns of a decorrelated aggregation: the parameters, then the key columns of the original.

Equations

• groupKey c is = Fin.append (fun (j : Fin c) => Fin.castAdd m j) fun (i : Fin n₁) => Fin.natAdd c (is i)

A grouping's own clauses

An aggregation carries an ORDER BY of its own and a FILTER clause per aggregate. Both read the input's columns, so both are shifted over the parameter block: the order reads the column c + i where it read i, which leaves the reading order unchanged (OrderSpec.readLe_append), and the clause keeps the same rows (Selection.keeps_shift).

def GroupOrder.lift {T : Type} (c : ℕ) {m : ℕ} : GroupOrder T m → GroupOrder T (c + m)

A grouping's ORDER BY, shifted over the parameters.

Equations

• GroupOrder.lift c GroupOrder.unord = GroupOrder.unord
• GroupOrder.lift c (GroupOrder.byCols cols spec) = GroupOrder.byCols (winOrd c cols) spec

def gammaSrc (c n₁ n₂ : ℕ) : Fin (c + (n₁ + n₂)) → Fin (c + n₁ + n₂)

Where each column of a decorrelated aggregation reads from: the parameters and the key come from its key block, the aggregates from its aggregate block.

Equations

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

The scalar aggregation

A scalar aggregation has one row whatever its input, so the decorrelation has one row per parameter row – including those whose slice is empty, which a grouping by the parameters does not produce. Those are recovered from the parameter rows the slices do not reach, each carrying the aggregates' value on no input. That value is written as a constant aggregate rather than as a constant term: a projection column carrying a constant is a regular column, and the column a scalar aggregation produces is an aggregate one, so only an aggregating operator can build it.

Windows: the parameters join the partition

A window of the decorrelated query partitions by the parameters as well, so each partition lies inside one slice; the frames are then the frames of that slice, read in the same order, because the clause reads the shifted order columns and the parameter block it shares is read first.

def winPart (c : ℕ) {k mp : ℕ} (P' : Tuple (Fin k) mp) : Tuple (Fin (c + k)) (c + mp)

The partition columns of a decorrelated window: the parameters, then the partition columns of the original.

Equations

• winPart c P' = Fin.append (fun (j : Fin c) => Fin.castAdd k j) fun (i : Fin mp) => Fin.natAdd c (P' i)

theorem ValueFrame.frameOf_slices {T : Type} [ValueType T] {c k mp p : ℕ} (P : Multiset (Tuple T c)) (hP : P.Nodup) (f : Tuple T c → Multiset (Tuple T k)) (P' : Tuple (Fin k) mp) (O : Tuple (Fin k) p) (w : ValueFrame T p) {v : Tuple T c} (hv : v ∈ P) (u : Tuple T k) : frameOf id (winPart c P') (winOrd c O) w (Relation.slices P f) (Fin.append v u) = Multiset.map (fun (x : Fin k → T) => Fin.append v x) (frameOf id P' O w (f v) u)

A frame of the decorrelated query is a frame of one slice: the parameters are part of the partition key, so a row of another slice is in no frame, and within a slice the frame condition reads the same values. EXCLUDE CURRENT ROW and EXCLUDE TIES are covered too: the row the frame takes out is the same row on both sides.

def winSrc (c n : ℕ) : Fin (c + (n + 1)) → Fin (c + n + 1)

The column a decorrelated window's row takes each of its own from: the parameters, the input's columns and the window's column last.

Equations

• winSrc c n i = Fin.addCases (fun (jp : Fin c) => (Fin.castAdd n jp).castSucc) (fun (i : Fin (n + 1)) => Fin.lastCases (Fin.last (c + n)) (fun (i : Fin n) => (Fin.natAdd c i).castSucc) i) i

Second-level aggregation

A second-level aggregation reads its group as a bag – its aggregate is a function of one – so the decorrelation needs the group itself rather than the sequence it is read as.

The apply: the construction's own recursion

An apply reads its right side once per row of its left, with that row's columns as the context. Decorrelating it is the recursion the whole construction is for: the left side is decorrelated over P, and the right side over the distinct rows of that decorrelation, which are the pairs its context ranges over. Pairing the two back by those columns restores the multiplicities duplicate elimination dropped.

An apply's right side reads its left row first and the ambient parameters after it, where a decorrelation puts the parameters in front: the two orders are swapped, which is what Relation.swapBlocks does.

def swapSrc (c n₁ : ℕ) : Fin (n₁ + c) → Fin (c + n₁)

The columns of the swapped block order: the left row, then the parameters.

Equations

• swapSrc c n₁ i = Fin.addCases (fun (i : Fin n₁) => Fin.natAdd c i) (fun (j : Fin c) => Fin.castAdd n₁ j) i

def Relation.swapBlocks {T : Type} (c n₁ : ℕ) (x : Tuple T (c + n₁)) : Tuple T (n₁ + c)

A row with its two blocks swapped: what an apply's right side reads as its context, read off a row of the left side's decorrelation.

Equations

• Relation.swapBlocks c n₁ x j = x (swapSrc c n₁ j)

def applySrc (c n₁ n₂ : ℕ) : Fin (c + (n₁ + n₂)) → Fin (c + n₁ + (n₁ + c + n₂))

The columns of the apply's join: the parameters and the left side's columns off the left decorrelation, the right side's own off the right.

Equations

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

theorem Relation.applyJoin_slices {T : Type} [ValueType T] {c n₁ n₂ : ℕ} (P : Multiset (Tuple T c)) (f : Tuple T c → Multiset (Tuple T n₁)) (g : Tuple T (n₁ + c) → Multiset (Tuple T n₂)) : Multiset.map (fun (z : Tuple T (c + n₁ + (n₁ + c + n₂))) (j : Fin (c + (n₁ + n₂))) => z (applySrc c n₁ n₂ j)) (Multiset.filter (fun (z : Tuple T (c + n₁ + (n₁ + c + n₂))) => ∀ (l : Fin (n₁ + c)), z (Fin.castAdd (n₁ + c + n₂) (swapSrc c n₁ l)) = z (Fin.natAdd (c + n₁) (Fin.castAdd n₂ l))) ((slices P f).bind fun (x : Tuple T (c + n₁)) => Multiset.map (fun (y : Fin (n₁ + c + n₂) → T) => Fin.append x y) (slices (Multiset.map (swapBlocks c n₁) (slices P f).dedup) g))) = slices P fun (v : Tuple T c) => (f v).bind fun (u : Tuple T n₁) => Multiset.map (fun (w : Fin n₂ → T) => Fin.append u w) (g (Fin.append u v))

The apply, at the level of relations. The left side's decorrelation holds each pair (parameters, left row) with its multiplicity; the right side's, over the distinct such pairs swapped into the order its context expects, holds one row per answer. Joining them on those columns and keeping the parameters, the left row and the right row gives the apply, slice by slice: duplicate elimination made the right side's parameter rows distinct, and the join puts the multiplicities back.

A block read twice

An apply's left side may carry aggregate columns, which its right side reads through their values; the join that puts the two decorrelations back together compares them, so it compares a copy of them read as values (AggQueryIn.Explode) and keeps the originals for the output.

def dupL (m X : ℕ) : Fin (m + X) → Fin (m + m + X)

The first copy of a doubled block, the rest of the row unmoved.

Equations

• dupL m X i = Fin.addCases (fun (i : Fin m) => Fin.castAdd X (Fin.castAdd m i)) (fun (x : Fin X) => Fin.natAdd (m + m) x) i

def dupR (m X : ℕ) : Fin (m + X) → Fin (m + m + X)

The second copy of a doubled block, the rest of the row unmoved.

Equations

• dupR m X i = Fin.addCases (fun (i : Fin m) => Fin.castAdd X (Fin.natAdd m i)) (fun (x : Fin X) => Fin.natAdd (m + m) x) i

def Tuple.dupBlock {T : Type} {m X : ℕ} (z : Tuple T (m + X)) : Tuple T (m + m + X)

A row with its first block doubled.

Equations

• z.dupBlock = Fin.append (Fin.append (fun (i : Fin m) => z (Fin.castAdd X i)) fun (i : Fin m) => z (Fin.castAdd X i)) fun (x : Fin X) => z (Fin.natAdd m x)

theorem dup_kind {T : Type} {m : ℕ} (κ : Fin m → ColKind) : (fun (j : Fin (m + m)) => ProjColIn.kind (AggQueryIn.carryCol κ (Fin.addCases id id j))) = Fin.append κ κ

def AggQueryIn.withRegCopy {T : Type} {m : ℕ} {κ : Fin m → ColKind} {l : List (String × ℕ)} (A : AggQueryIn T 0 m κ l) : AggQueryIn T 0 (m + m) (regBelow (Fin.append κ κ) m) l

A query with its columns doubled, the first copy read as values.

Equations

• A.withRegCopy = AggQueryIn.explodeBelow m (AggQueryIn.castKind ⋯ (AggQueryIn.Proj (fun (j : Fin (m + m)) => AggQueryIn.carryCol κ (Fin.addCases id id j)) A))

The construction

Putting the cases together: every query of the plain fragment – the basis classes and the apply – has a decorrelation using the basis classes only. The induction is on the query, and its statement quantifies over the parameter relation, because the apply's right side is decorrelated over a parameter relation built from its left side.

What the parameter relation is asked is that it use the basis classes (it ends up inside the decorrelation) and that its rows be pairwise distinct (Multiset.Nodup): a repeated parameter row would pair the copies of its own slice with each other, which is what Relation.filter_paramsOf_slices rules out.

theorem AggQueryIn.hasDecorrelation_of_usesOnly_gen {T : Type} [ValueType T] {S U : Set OpKind} (hmb : OpKind.muBag ∉ U) (hms : OpKind.muSet ∉ U) {sch : Schema} (hS : decorrCore ⊆ S) (hU : ∀ k ∈ U, k ≠ OpKind.apply → k ∈ S) (hσ : OpKind.prod ∈ U ∨ OpKind.apply ∈ U → OpKind.sel ∈ S ∧ OpKind.dedup ∈ S) {c n : ℕ} {κ : Fin n → ColKind} {l : List (String × ℕ)} (q : AggQueryIn T c n κ l) : l = [] → usesOnly U q → overSchema sch q → ∀ (P : AggQuery T c (ColKind.allReg c)), usesOnly S P → overSchema sch P → (∀ (D : Database T), Multiset.Nodup (evaluatePlain P D)) → HasDecorrelation S sch P q

Every query has an apply-free decorrelation over every parameter relation whose rows are distinct. The construction is that of Galindo-Legaria & Joshi, each operator carrying the parameters along, and the apply itself recursing with the distinct rows of its own left side as the new parameter relation.

The target set is the query's own, which is what makes the result composable: a query with no window decorrelates to one with no window.

theorem AggQueryIn.hasDecorrelation_of_usesOnly {T : Type} [ValueType T] {S : Set OpKind} (hmb : OpKind.muBag ∉ S) (hms : OpKind.muSet ∉ S) {sch : Schema} (hS : decorrOps ⊆ S) {c n : ℕ} {κ : Fin n → ColKind} {l : List (String × ℕ)} (q : AggQueryIn T c n κ l) : l = [] → usesOnly (insert OpKind.apply S) q → overSchema sch q → ∀ (P : AggQuery T c (ColKind.allReg c)), usesOnly S P → overSchema sch P → (∀ (D : Database T), Multiset.Nodup (evaluatePlain P D)) → HasDecorrelation S sch P q

The decorrelation over the classes S, the apply aside.

theorem AggQueryIn.exists_applyFree_plainEquiv_sig {T : Type} [ValueType T] {S : Set OpKind} {sch : Schema} (hS : decorrOps ⊆ S) (hg : OpKind.gamma ∈ S) (hmb : OpKind.muBag ∉ S) (hms : OpKind.muSet ∉ S) {n : ℕ} {κ : Fin n → ColKind} (q : AggQuery T n κ) (hq : usesOnly (insert OpKind.apply S) q) (hqs : overSchema sch q) : ∃ (q' : AggQuery T n κ), usesOnly S q' ∧ overSchema sch q' ∧ (∀ (Θ : Set (SeqAggFunc T)), inSig Θ q → paramsReg q → inSig Θ q') ∧ PlainEquiv q q'

A closed query's applies are eliminable. Over the unit – one empty row, which is the parameter relation a closed query reads – the decorrelation is the query itself, its parameter block empty, so projecting that block away gives an apply-free query with the same plain semantics. This is why the apply is left out of the basis classes.

theorem AggQueryIn.exists_applyFree_plainEquiv {T : Type} [ValueType T] {S : Set OpKind} {sch : Schema} (hS : decorrOps ⊆ S) (hg : OpKind.gamma ∈ S) (hmb : OpKind.muBag ∉ S) (hms : OpKind.muSet ∉ S) {n : ℕ} {κ : Fin n → ColKind} (q : AggQuery T n κ) (hq : usesOnly (insert OpKind.apply S) q) (hqs : overSchema sch q) : ∃ (q' : AggQuery T n κ), usesOnly S q' ∧ overSchema sch q' ∧ PlainEquiv q q'

A closed query's applies are eliminable (exists_applyFree_plainEquiv_sig without the signature).

Home · Documentation · Publications · Contributors · Source · Cite