The basis, assembled

Which classes of operators generate the plain fragment is a question with two halves. The lower bounds are the six invariants of Provenance.PlainBasis, each with a query that breaks it. The upper bound is this file: every query of the fragment is equivalent to one using only the six classes ∅, Π, σ, ×, ⊎, γ.

It is three passes, in this order, each of which is a structural recursion carrying the identities already proved:

1. the windows go (AggQueryIn.exists_winFree), each becoming an apply of a scalar aggregation over its frame (winByApply);
2. the applies go (AggQueryIn.exists_applyFree_plainEquiv), by the decorrelation of Provenance.Decorrelate, which leaves duplicate elimination and the difference behind;
3. those two go (AggQueryIn.exists_basisOps_of_dedupDiff), by the two identities that give ε from a grouping and − from counts.

The order is forced: a window becomes an apply, so the windows must go before the applies; and the decorrelation builds an ε (the distinct rows of an apply's left side) and a − (the parameter rows a scalar aggregation's slices do not reach), so those must go after. Each pass is stated with the class set as a parameter, which is what lets them be composed: it is only because the decorrelation of a window-free query is window-free that the first pass is not undone by the second.

AggQueryIn.exists_basisOps_plainEquiv is the three passes composed, and GeneratesOn reads it as a property of a set of classes (basisOps_generatesOn). Each pass also carries overSchema: the query it produces names the relations the query it is given names, which is what the other half needs.

That other half is six lemmas, one per class a generating set must contain: proj_mem_of_generatesOn, union_mem_of_generatesOn, gamma_mem_of_generatesOn, prod_or_apply_mem_of_generatesOn, empty_mem_of_generatesOn and sel_or_diff_mem_of_generatesOn. They are separate statements rather than one conjunction because each names the schema its witness lives over, and the witness for ∅ lives over the empty schema – no single schema serves them all.

The two swaps – − for σ, the apply for × – are the last two theorems here, AggQueryIn.exists_selFree and AggQueryIn.exists_prodFree. Each is a pass applying the identity everywhere, and what they ask of a query is AggQueryIn.SwapReady: a selection's input and a product's left factor must have regular columns, since the difference and an apply's left side take those. AggQueryIn.exists_allReg of Provenance.AllRegular is what puts a query in that shape, reading every column as a value – which over a plain relation changes nothing.

The three alternative bases are stated and proved: AggQueryIn.exists_basisDiffOps_plainEquiv over {∅, Π, ×, ⊎, γ, −}, AggQueryIn.exists_basisApplyOps_plainEquiv over {∅, Π, σ, apply, ⊎, γ} and exists_basisApplyDiffOps_plainEquiv over {∅, Π, apply, ⊎, γ, −}, with basisDiffOps_generatesOn, basisApplyOps_generatesOn and basisApplyDiffOps_generatesOn their GeneratesOn forms. Each is the three passes, then the re-typing, then the swap or swaps.

They ask nothing of their input beyond what the six-class statement asks. That the columns re-type is part of AggQueryIn.usesOnly: a projection column reading an aggregate column through an arbitrary function belongs to the rewritten world, not to the source language, which reads it through a term (ProjColIn.aggTermOf), and usesOnly refuses the former as it refuses GammaTok and ProvSum. What is left of AggQueryIn.Retypable is the window's own condition, and that is vacuous here: the first pass replaces every window by an apply of a scalar aggregation (AggQueryIn.retypable_of_usesOnly).

What a window has to be for its derivation from the apply

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

Every window of the query is derivable. Two things at each window: its input's columns are all regular (an apply reads its left side as a relation of values), and its frame contains its current row – EXCLUDE CURRENT ROW and EXCLUDE TIES have no reading as an aggregation, a group being determined by its rows and not by the occurrence, which is why evaluatePlain_winByApply asks ValueFrame.ContainsSelf.

Nothing is asked about the frame condition: a frame names a FrameCond, so the selection that spells it out is read off it (ValueFrame.exists_framePred), for every frame of the syntax, every FILTER clause and every domain. DISTINCT and a clause are covered too: the derived form aggregates f^distinct where the window does, and the clause enters that selection (evaluatePlain_winByApplyOf).

What stays out is a multi-frame window, and not for want of proving: its column combines the leaves' values by a function no term expresses, so the predicate reads False there, as it does for ProjColIn.aggTerm elsewhere.

Equations

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

The first pass: the windows go

theorem AggQueryIn.exists_winFree {T : Type} [ValueType T] {S : Set OpKind} {sch : Schema} (ha : OpKind.apply ∈ S) (hg : OpKind.gamma ∈ S) (hs : OpKind.sel ∈ S) (hmb : OpKind.muBag ∉ S) (hms : OpKind.muSet ∉ S) {c n : ℕ} {κ : Fin n → ColKind} {l : List (String × ℕ)} (q : AggQueryIn T c n κ l) : usesOnly (insert OpKind.win S) q → q.WinsDerivable → overSchema sch q → ∃ (q' : AggQueryIn T c n κ l), usesOnly S q' ∧ overSchema sch q' ∧ ∀ (D : Database T) (γ : Fin c → T), q.evaluatePlain D γ = q'.evaluatePlain D γ

Every window is eliminable (evaluatePlain_winByApply, applied recursively): a query whose windows are derivable is equivalent to one with no window, using the apply, the aggregation and the selection in their place.

The third pass: duplicate elimination and the difference go

theorem AggQueryIn.exists_basisOps_of_dedupDiff {T : Type} [ValueType T] {S : Set OpKind} {sch : Schema} (hp : OpKind.proj ∈ S) (hs : OpKind.sel ∈ S) (hx : OpKind.prod ∈ S) (hu : OpKind.union ∈ S) (hg : OpKind.gamma ∈ S) (hap : OpKind.apply ∉ S) (hmb : OpKind.muBag ∉ S) (hms : OpKind.muSet ∉ S) (cnt : SeqAggFunc T) (hcnt : cnt.Counts) {c n : ℕ} {κ : Fin n → ColKind} {l : List (String × ℕ)} (q : AggQueryIn T c n κ l) : c = 0 → usesOnly (insert OpKind.dedup (insert OpKind.diff S)) q → overSchema sch q → ∃ (q' : AggQueryIn T c n κ l), usesOnly S q' ∧ overSchema sch q' ∧ ∀ (D : Database T) (γ : Fin c → T), q.evaluatePlain D γ = q'.evaluatePlain D γ

Duplicate elimination and the difference are eliminable (recursively): over a closed query using the basis classes and those two, duplicate elimination becomes a grouping and the difference becomes a count over the tagged union, so the query is equivalent to one over the basis alone.

The query is asked to be closed, which is where the two identities are proved, and to use no apply – both of which the decorrelation's output is.

The three passes composed

def basisDD : Set OpKind

The classes the middle of the construction works in: the basis, with duplicate elimination and the difference, which the decorrelation leaves behind and the third pass removes.

Equations

• basisDD = insert OpKind.dedup (insert OpKind.diff basisOps)

def plainOps : Set OpKind

The plain fragment's classes: the basis, duplicate elimination, the difference, the apply and the window. The four operators usesOnly reads as False – the two recursions, the token-building grouping and the provenance sum – are outside it, as is the multi-frame window, which AggQueryIn.WinsDerivable excludes.

Equations

• plainOps = insert OpKind.win (insert OpKind.apply basisDD)

theorem AggQueryIn.exists_basisOps_plainEquiv {T : Type} [ValueType T] {sch : Schema} {n : ℕ} {κ : Fin n → ColKind} (cnt : SeqAggFunc T) (hcnt : cnt.Counts) (q : AggQuery T n κ) (hq : usesOnly plainOps q) (hd : WinsDerivable q) (hqs : overSchema sch q) : ∃ (q' : AggQuery T n κ), usesOnly basisOps q' ∧ overSchema sch q' ∧ PlainEquiv q q'

The six classes generate the plain fragment: every query of the plain fragment is equivalent to one using only the six basis classes ∅, Π, σ, ×, ⊎, γ, over the same schema.

The three hypotheses are what the identities ask for: an aggregate that counts (SQL's count(e)), that the query use only the classes in scope, and that every window be derivable.

The basis with the window kept

win is needed in every basis of the whole algebra (win_mem_of_generatesOnRec), so the statement a source query is read by keeps its windows and runs only two passes: the applies go by the decorrelation, and the duplicate elimination and the difference it builds go with them. Nothing is asked of a window here – not that its frame contain its current row, not that it be single-frame, not that its input's columns be regular – because nothing has to rewrite one: the decorrelation carries a window of every frame (ValueFrame.frameOf_slices: the row a frame takes out is the same row on both sides), and the third pass keeps it.

AggQueryIn.exists_basisOps_plainEquiv is the strictly stronger claim – the window class is not needed for the windows evaluatePlain_winByApply reaches – and that is where AggQueryIn.WinsDerivable is asked.

def basisWinOps : Set OpKind

The basis with the window: the six classes and win.

Equations

• basisWinOps = insert OpKind.win basisOps

theorem AggQueryIn.exists_basisWinOps_plainEquiv {T : Type} [ValueType T] {sch : Schema} {n : ℕ} {κ : Fin n → ColKind} (cnt : SeqAggFunc T) (hcnt : cnt.Counts) (q : AggQuery T n κ) (hq : usesOnly plainOps q) (hqs : overSchema sch q) : ∃ (q' : AggQuery T n κ), usesOnly basisWinOps q' ∧ overSchema sch q' ∧ PlainEquiv q q'

Every query of the plain fragment is equivalent to one over the basis and the window, over the same schema and with the same columns. It carries no hypothesis about windows at all.

def GeneratesOn (T : Type) [ValueType T] (sch : Schema) (S : Set OpKind) : Prop

A generating set over a schema: every query over sch whose windows are derivable, and which applies no function to an aggregate column, is equivalent to one over sch using only the classes of S. This is the form the necessity of ∅ and of σ/− needs (empty_mem_of_generatesOn, sel_or_diff_mem_of_generatesOn); the three passes give the equivalence on every instance, which is stronger than AggQueryIn.PlainEquivOn asks. The query produced has regular columns throughout, which is what the swaps need and what the plain semantics has anyway. The classes of S are recursion-free, as the fragment is: so the query produced is defined everywhere (GeneratesOn.settles), and the generation with the recursions is GeneratesOnRec's.

Equations

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

def schemaS : Schema

The schema of the binary relation the projection witness reads.

Equations

• schemaS = Schema.ofFn (fun (s : String) => if s = "S" then some 2 else none) {"S"} schemaS._proof_2

theorem basisOps_generatesOn {T : Type} [ValueType T] (cnt : SeqAggFunc T) (hcnt : cnt.Counts) (sch : Schema) : GeneratesOn T sch basisOps

The six classes generate, over a schema: GeneratesOn's form of the theorem above, which is what the necessity lemmas below are stated against.

What every generating set must contain

Each of the six invariants of Provenance.PlainBasis holds of every query that avoids one class, and each has a witness query that breaks it; a generating set that omitted the class would have to express the witness by a query that cannot.

theorem union_mem_of_generatesOn {T : Type} [ValueType T] {S : Set OpKind} {sch : Schema} (hS : GeneratesOn T sch S) : OpKind.union ∈ S

⊎ is necessary: without it a thin instance has an answer of at most one row, and two copies of one row are two.

theorem gamma_mem_of_generatesOn {T : Type} [ValueType T] {S : Set OpKind} {sch : Schema} (hS : GeneratesOn T sch S) : OpKind.gamma ∈ S

γ is necessary: without it the all-empty instance has an empty answer, and the unit has a row there.

theorem proj_mem_of_generatesOn {S : Set OpKind} (hS : GeneratesOn ℕ schemaS S) : OpKind.proj ∈ S

Π is necessary: without it a query's multiplicities are bounded by the query, and a projection of a relation with a repeated column has unbounded ones. The invariant holds with the recursions too (AggQueryIn.count_le_multBound), which is the whole algebra's row.

theorem prod_or_apply_mem_of_generatesOn {S : Set OpKind} (hS : GeneratesOn ℕ schemaR S) : OpKind.prod ∈ S ∨ OpKind.apply ∈ S

One of × and the apply is necessary: without both, an answer is linear in the instance, and a relation joined with itself is quadratic. With the recursions the row is stated in the minimal universe, prod_or_apply_mem_of_generatesOnRec of Provenance.RecursionBasis.

The two rows that are about the schema

∅ and σ/− are necessary for a reason the semantics alone does not see: a query may name a relation the schema does not declare, and such a reference reads the empty relation. So without ∅ one can still write a query with no rows – by naming nothing – and without σ and − one can still write a query that is empty on every instance. What makes them necessary is that the query be over the schema (AggQueryIn.overSchema), and the generation then has to produce a query over the same schema.

theorem empty_mem_of_generatesOn {T : Type} [ValueType T] {S : Set OpKind} (hS : GeneratesOn T Schema.empty S) : OpKind.empty ∈ S

∅ is necessary: over the empty schema a query can name no relation, so there is nothing to write it with. No witness is needed – the unit is already a query over that schema, and whatever it is equivalent to must be written without a relation name.

theorem sel_or_diff_mem_of_generatesOn {S : Set OpKind} (hS : GeneratesOn ℕ schemaR S) : OpKind.sel ∈ S ∨ OpKind.diff ∈ S

One of σ and − is necessary: without both, a query over the schema is empty on every instance or non-empty on every full one, and a selection on a value is neither – it keeps the row of one full instance and drops the row of another.

The swaps: a selection as a difference, a product as an apply

− may stand in for σ, and the apply for ×. Both identities are in Provenance.PlainBasis; what they ask of a query is that the input of a selection and the left factor of a product have regular columns – the difference and an apply's left side take those – and AggQueryIn.exists_allReg is what puts a query in that shape (AggQueryIn.SwapReady). These two passes then apply them everywhere.

theorem AggQueryIn.exists_prodFree {T : Type} [ValueType T] {S : Set OpKind} {sch : Schema} (ha : OpKind.apply ∈ S) (hmb : OpKind.muBag ∉ S) (hms : OpKind.muSet ∉ S) {c n : ℕ} {κ : Fin n → ColKind} {l : List (String × ℕ)} (q : AggQueryIn T c n κ l) : l = [] → usesOnly (insert OpKind.prod S) q → q.SwapReady → overSchema sch q → ∃ (q' : AggQueryIn T c n κ), usesOnly S q' ∧ overSchema sch q' ∧ ∀ (D : Database T) (γ : Fin c → T), q.evaluatePlain D γ = q'.evaluatePlain D γ

Every product is an apply (recursively): one whose right side reads no outer column, which is what apply_plainEquiv_prod says.

theorem AggQueryIn.exists_selFree {T : Type} [ValueType T] {S : Set OpKind} {sch : Schema} (hp : OpKind.proj ∈ S) (hd : OpKind.diff ∈ S) (hap : OpKind.apply ∉ S) (hmb : OpKind.muBag ∉ S) (hms : OpKind.muSet ∉ S) {c n : ℕ} {κ : Fin n → ColKind} {l : List (String × ℕ)} (q : AggQueryIn T c n κ l) : l = [] → c = 0 → usesOnly (insert OpKind.sel S) q → q.SwapReady → overSchema sch q → ∃ (q' : AggQueryIn T c n κ), usesOnly S q' ∧ overSchema sch q' ∧ q'.SwapReady ∧ ∀ (D : Database T) (γ : Fin c → T), q.evaluatePlain D γ = q'.evaluatePlain D γ

Every selection is a difference (recursively): the rows tagged with the predicate's value, minus those the constant tagging leaves out, which is what sel_plainEquiv_selByDiff_polTerm says. The query is asked to be closed, which is where that identity is proved, and to use no apply – both of which the three passes' output is.

The two alternative bases

With the swaps proved as passes, the generation half holds of the two sets obtained from the six by letting − stand in for σ, or the apply for ×. Each is the three passes, then the re-typing, then the pass that applies the identity everywhere – the re-typing in the middle because a selection's input and a product's left factor have to hold values, which is what the difference and an apply's left side take.

def basisDiffOps : Set OpKind

The basis with the difference in place of the selection.

Equations

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

def basisApplyOps : Set OpKind

The basis with the apply in place of the product.

Equations

• basisApplyOps = {OpKind.empty, OpKind.proj, OpKind.sel, OpKind.apply, OpKind.union, OpKind.gamma}

theorem AggQueryIn.exists_basisDiffOps_plainEquiv {T : Type} [ValueType T] {sch : Schema} {n : ℕ} {κ : Fin n → ColKind} (cnt : SeqAggFunc T) (hcnt : cnt.Counts) (q : AggQuery T n κ) (hq : usesOnly plainOps q) (hd : WinsDerivable q) (hqs : overSchema sch q) : ∃ (q' : AggQuery T n (ColKind.allReg n)), usesOnly basisDiffOps q' ∧ overSchema sch q' ∧ PlainEquiv q q'

The basis with − for σ: every query of the plain fragment whose projections post-compose no aggregate column is equivalent to one over ∅, Π, ×, ⊎, γ, −. The value domain's own non-zero value is what the selection's difference marks the rows it keeps with.

theorem AggQueryIn.exists_basisApplyOps_plainEquiv {T : Type} [ValueType T] {sch : Schema} {n : ℕ} {κ : Fin n → ColKind} (cnt : SeqAggFunc T) (hcnt : cnt.Counts) (q : AggQuery T n κ) (hq : usesOnly plainOps q) (hd : WinsDerivable q) (hqs : overSchema sch q) : ∃ (q' : AggQuery T n (ColKind.allReg n)), usesOnly basisApplyOps q' ∧ overSchema sch q' ∧ PlainEquiv q q'

The basis with the apply for ×: the same, over ∅, Π, σ, the apply, ⊎, γ.

theorem basisDiffOps_generatesOn {T : Type} [ValueType T] (cnt : SeqAggFunc T) (hcnt : cnt.Counts) (sch : Schema) : GeneratesOn T sch basisDiffOps

{∅, Π, ×, ⊎, γ, −} generates, over a schema.

theorem basisApplyOps_generatesOn {T : Type} [ValueType T] (cnt : SeqAggFunc T) (hcnt : cnt.Counts) (sch : Schema) : GeneratesOn T sch basisApplyOps

{∅, Π, σ, apply, ⊎, γ} generates, over a schema.

Three windows that are derivable

AggQueryIn.WinsDerivable asks of a window that its frame contain its current row and that its input be all regular. These are three frames that satisfy the first, each over any DISTINCT and any FILTER clause: the whole partition and the two RANGE frames. Nothing is asked of the frame condition, which ValueFrame.exists_framePred reads as a predicate of the language, nor of the domain.

theorem AggQueryIn.winsDerivable_win_whole {T : Type} [ValueType T] {lab c n m p : ℕ} {rd : Fin c → Bool} (P : Tuple (Fin n) m) (O : Tuple (Fin n) p) (o : OrderSpec p) (t : TermIn T c n) (f : SeqAggFunc T) {q : AggQueryIn T c n (ColKind.allReg n)} (dist : Bool) (keep : Option (Selection T n)) (hq : q.WinsDerivable) : (Win P O o ValueFrame.whole t f q ⋯ dist keep).WinsDerivable

A window over the whole partition is derivable.

The fourth basis: both swaps at once

The two swaps are independent, so a fourth basis is the two together: − for σ and the apply for ×. What makes the composition work is that the selection pass leaves its output ready for the product pass (AggQueryIn.swapReady_selByDiff), the difference it builds introducing neither a product nor a selection of its own.

def basisApplyDiffOps : Set OpKind

The basis with the difference for the selection and the apply for the product.

Equations

• basisApplyDiffOps = {OpKind.empty, OpKind.proj, OpKind.apply, OpKind.union, OpKind.gamma, OpKind.diff}

theorem AggQueryIn.exists_basisApplyDiffOps_plainEquiv {T : Type} [ValueType T] {sch : Schema} {n : ℕ} {κ : Fin n → ColKind} (cnt : SeqAggFunc T) (hcnt : cnt.Counts) (q : AggQuery T n κ) (hq : usesOnly plainOps q) (hd : WinsDerivable q) (hqs : overSchema sch q) : ∃ (q' : AggQuery T n (ColKind.allReg n)), usesOnly basisApplyDiffOps q' ∧ overSchema sch q' ∧ PlainEquiv q q'

The basis with − for σ and the apply for ×: every query of the plain fragment whose projections post-compose no aggregate column is equivalent to one over ∅, Π, the apply, ⊎, γ, −.

theorem basisApplyDiffOps_generatesOn {T : Type} [ValueType T] (cnt : SeqAggFunc T) (hcnt : cnt.Counts) (sch : Schema) : GeneratesOn T sch basisApplyDiffOps

{∅, Π, apply, ⊎, γ, −} generates, over a schema.

Home · Documentation · Publications · Contributors · Source · Cite