The cut a query's symbolic evaluation is taken relative to

The symbolic evaluation of a query is correct relative to a cut holding every value the evaluation compares, groups or makes up (Sym.Good): the values of the relations it reads, its constants, the null, the context's values, and the values its aggregations compute. The last are computed by symbolic evaluations themselves: a grouping's counts, at every parameter row, are read off the symbolic evaluation of its input relative to the cut of that input, which is smaller. So the cut is defined by recursion on the query (Sym.cutQ), each aggregation adding the values its symbolic counterpart computes, and it is proved to make the evaluation good (Sym.good_cutQ).

def Sym.unionFin {T : Type} [ValueType T] {c : ℕ} (f : ℕ → String) (n : ℕ) : (Fin n → AggQueryIn T c 1 (ColKind.allReg 1)) → AggQueryIn T c 1 (ColKind.allReg 1)

The union of finitely many unary relations.

Equations

• Sym.unionFin f 0 x_2 = AggQueryIn.emptyRel 1
• Sym.unionFin f n.succ F = AggQueryIn.sumByMuX (f 0) (f 1) (F 0) (Sym.unionFin (fun (i : ℕ) => f (i + 2)) n fun (i : Fin n) => F i.succ)

def Sym.u2 {T : Type} [ValueType T] {c : ℕ} (f : ℕ → String) (a b : AggQueryIn T c 1 (ColKind.allReg 1)) : AggQueryIn T c 1 (ColKind.allReg 1)

The union of two unary relations.

Equations

• Sym.u2 f a b = AggQueryIn.sumByMuX (f 0) (f 1) a b

def Sym.valsOf {T : Type} [ValueType T] {c : ℕ} (f : ℕ → String) {n : ℕ} (q : AggQueryIn T c n (ColKind.allReg n)) : AggQueryIn T c 1 (ColKind.allReg 1)

The values of every column of a relation.

Equations

• Sym.valsOf f q = Sym.unionFin f n fun (i : Fin n) => Sym.projQ (fun (x : Fin 1) => Sym.SA.col i) q

def Sym.ambQ {T : Type} [ValueType T] (f : ℕ → String) (c : ℕ) : AggQueryIn T c 1 (ColKind.allReg 1)

The context's values.

Equations

• Sym.ambQ f c = Sym.unionFin f c fun (j : Fin c) => Sym.projQ (fun (x : Fin 1) => Sym.SA.amb j) AggQueryIn.unitC

def Sym.nullQ {T : Type} [ValueType T] {c : ℕ} : AggQueryIn T c 1 (ColKind.allReg 1)

The null, if the domain has one.

Equations

• Sym.nullQ = match ValueType.nullVal with | some ν => Sym.constQ ν | none => AggQueryIn.emptyRel 1

noncomputable def Sym.constsQ {T : Type} [ValueType T] {c : ℕ} (f : ℕ → String) (S : Finset T) : AggQueryIn T c 1 (ColKind.allReg 1)

Finitely many constants.

Equations

• Sym.constsQ f S = Sym.unionFin f S.toList.length fun (i : Fin S.toList.length) => Sym.constQ (S.toList.get i)

The aggregations of the symbolic evaluation, before their cells

noncomputable def Sym.gammaRaw {T : Type} [ValueType T] {k c : ℕ} (env : SymEnv T k c) (f : ℕ → String) {m n₁ n₂ : ℕ} (is : Tuple (Fin m) n₁) (ts : Tuple (TermIn T (k + c) m) n₂) (fs : Tuple (SeqAggFunc T) n₂) (q : AggQueryIn T (k + c) m (ColKind.allReg m)) (keep : Fin n₂ → Option (Selection T m)) : AggQueryIn T c (k * (7 + k) + n₁ * (7 + k) + n₂) (ColKind.allReg (k * (7 + k) + n₁ * (7 + k) + n₂))

A symbolic grouping's rows: the keys' cells, then the aggregate values themselves.

Equations

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

noncomputable def Sym.nestRaw {T : Type} [ValueType T] {k c : ℕ} (env : SymEnv T k c) (f : ℕ → String) {m n₁ : ℕ} {κ : Fin m → ColKind} (is : Tuple (Fin m) n₁) (p : ProjColIn T (k + c) κ) (g : Multiset T → T) (q : AggQueryIn T (k + c) m κ) : AggQueryIn T c (k * (7 + k) + n₁ * (7 + k) + 1) (ColKind.allReg (k * (7 + k) + n₁ * (7 + k) + 1))

A symbolic second-level grouping's rows.

Equations

• Sym.nestRaw env f is p g q = (AggQueryIn.GammaNest (Sym.gKeyIdx is) ⋯ (Sym.projV p) g (Sym.sym env f q)).allRegOf

noncomputable def Sym.scalarRaw {T : Type} [ValueType T] {k c : ℕ} (env : SymEnv T k c) (f : ℕ → String) {m n₂ : ℕ} (ts : Tuple (TermIn T (k + c) m) n₂) (fs : Tuple (SeqAggFunc T) n₂) {κ : Fin m → ColKind} (q : AggQueryIn T (k + c) m κ) : AggQueryIn T c (k * (7 + k) + n₂) (ColKind.allReg (k * (7 + k) + n₂))

A symbolic scalar aggregation's rows, over the padded union.

Equations

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

noncomputable def Sym.winRaw {T : Type} [ValueType T] {k c : ℕ} (env : SymEnv T k c) (f : ℕ → String) {n m p : ℕ} (P : Tuple (Fin n) m) (O : Tuple (Fin n) p) (o : OrderSpec p) (w : ValueFrame T p) {hsql : ValueFrame.IsSQL o w} (t : TermIn T (k + c) n) (g : SeqAggFunc T) {κ : Fin n → ColKind} (q : AggQueryIn T (k + c) n κ) (dist : Bool) (keep : Option (Selection T n)) : AggQueryIn T c ((k + n) * (7 + k) + 1) (ColKind.allReg ((k + n) * (7 + k) + 1))

A symbolic window's rows: the input's cells, then the window's value itself.

Equations

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

The cut

def Sym.part (f : ℕ → String) (j : ℕ) : ℕ → String

An eighth of a supply of names.

Equations

• Sym.part f j i = f (8 * i + j)

def Sym.colsQ {T : Type} [ValueType T] {c N p : ℕ} (f : ℕ → String) (q : AggQueryIn T c N (ColKind.allReg N)) (idx : Fin p → Fin N) : AggQueryIn T c 1 (ColKind.allReg 1)

The values of some columns of a relation.

Equations

• Sym.colsQ f q idx = Sym.unionFin f p fun (j : Fin p) => Sym.projQ (fun (x : Fin 1) => Sym.SA.col (idx j)) q

noncomputable def Sym.cutOf {T : Type} [ValueType T] {c : ℕ} (f : ℕ → String) (S : Finset T) (core : AggQueryIn T c 1 (ColKind.allReg 1)) : AggQueryIn T c 1 (ColKind.allReg 1)

A cut: the null, the context's values, finitely many constants and the values a query computes.

Equations

• Sym.cutOf f S core = Sym.u2 (Sym.part f 0) (Sym.u2 (Sym.part f 1) Sym.nullQ (Sym.ambQ (Sym.part f 2) c)) (Sym.u2 (Sym.part f 3) (Sym.constsQ (Sym.part f 4) S) core)

@[irreducible]

noncomputable def Sym.cutCore {T : Type} [ValueType T] {k c : ℕ} (cnt : SeqAggFunc T) (f : ℕ → String) {n : ℕ} {κ : Fin n → ColKind} {l : List (String × ℕ)} : AggQueryIn T (k + c) n κ l → AggQueryIn T c 1 (ColKind.allReg 1)

The values a query reads and computes: those of the relations it reads and those its aggregations compute, read off their symbolic counterparts relative to the cut of their input.

Equations

• One or more equations did not get rendered due to their size.
• Sym.cutCore cnt f (AggQueryIn.Rel x✝ s) = Sym.valsOf f (AggQueryIn.Rel x✝ s)
• Sym.cutCore cnt f (AggQueryIn.Hole x✝¹ s x✝) = AggQueryIn.emptyRel 1
• Sym.cutCore cnt f (AggQueryIn.Param pv x✝) = AggQueryIn.emptyRel 1
• Sym.cutCore cnt f AggQueryIn.Empty = AggQueryIn.emptyRel 1
• Sym.cutCore cnt f (AggQueryIn.Proj ps q) = Sym.cutCore cnt f q
• Sym.cutCore cnt f (AggQueryIn.Sel φ q hφ) = Sym.cutCore cnt f q
• Sym.cutCore cnt f (q₁.Prod q₂) = Sym.u2 (Sym.part f 0) (Sym.cutCore cnt (Sym.part f 1) q₁) (Sym.cutCore cnt (Sym.part f 2) q₂)
• Sym.cutCore cnt f (AggQueryIn.Explode k_1 a q) = Sym.cutCore cnt f q
• Sym.cutCore cnt f (AggQueryIn.Retag h q) = Sym.cutCore cnt f q
• Sym.cutCore cnt f (AggQueryIn.Mu s q₀ q₁) = Sym.u2 (Sym.part f 0) (Sym.cutCore cnt (Sym.part f 1) q₀) (Sym.cutCore cnt (Sym.part f 2) q₁)
• Sym.cutCore cnt f (a.Apply a_1) = AggQueryIn.emptyRel 1
• Sym.cutCore cnt f (a.Sum a_1) = AggQueryIn.emptyRel 1
• Sym.cutCore cnt f a.Dedup = AggQueryIn.emptyRel 1
• Sym.cutCore cnt f (a.Diff a_1) = AggQueryIn.emptyRel 1
• Sym.cutCore cnt f (AggQueryIn.MuSet s a a_1) = AggQueryIn.emptyRel 1
• Sym.cutCore cnt f (AggQueryIn.GammaTok is his ts fs a a_1 keep) = AggQueryIn.emptyRel 1
• Sym.cutCore cnt f (AggQueryIn.ProvSum is his t a) = AggQueryIn.emptyRel 1
• Sym.cutCore cnt f (AggQueryIn.WinExpr P O o ws ts fs g a keeps) = AggQueryIn.emptyRel 1

noncomputable def Sym.cutQ {T : Type} [ValueType T] {k c : ℕ} (cnt : SeqAggFunc T) (f : ℕ → String) {n : ℕ} {κ : Fin n → ColKind} {l : List (String × ℕ)} (q : AggQueryIn T (k + c) n κ l) : AggQueryIn T c 1 (ColKind.allReg 1)

The cut of a query.

Equations

• Sym.cutQ cnt f q = Sym.cutOf (Sym.part f 0) q.allConsts (Sym.cutCore cnt (Sym.part f 1) q)

What the cut names

What the cut holds

The cut makes the evaluation good

def Sym.basisProdOps : Set OpKind

The classes of the basis with products in place of the apply: ∅, Π, σ, ×, γ, win, μ^⊎.

Equations

• Sym.basisProdOps = {OpKind.empty, OpKind.proj, OpKind.sel, OpKind.prod, OpKind.gamma, OpKind.win, OpKind.muBag}

def Sym.CutOK {T : Type} [ValueType T] {k c' n : ℕ} {κ : Fin n → ColKind} {l : List (String × ℕ)} (cnt : SeqAggFunc T) (f : ℕ → String) (q : AggQueryIn T (k + c') n κ l) (C : Finset T) (D : Database T) (γ : Fin c' → T) : Prop

What a cut is asked of a query: the null, the context's values, the query's constants and the values of its core.

Equations

• Sym.CutOK cnt f q C D γ = ((∀ (a : T), ValueType.isNull a = true → a ∈ C) ∧ (∀ (j : Fin c'), γ j ∈ C) ∧ q.allConsts ⊆ C ∧ Sym.valsU ((Sym.cutCore cnt f q).evaluatePlain D γ) ⊆ C)

The table of a query

noncomputable def Sym.tabEnv {T : Type} [ValueType T] {k c : ℕ} (cnt : SeqAggFunc T) (f : ℕ → String) {n : ℕ} {κ : Fin n → ColKind} (q : AggQueryIn T (k + c) n κ) : SymEnv T k c

The environment of a query's table: built from the query's cut.

Equations

• Sym.tabEnv cnt f q = Sym.envOf (Sym.part f 0) cnt k (Sym.cutQ cnt (Sym.part f 1) q)

noncomputable def Sym.tabQ {T : Type} [ValueType T] {k c : ℕ} (cnt : SeqAggFunc T) (f : ℕ → String) {n : ℕ} {κ : Fin n → ColKind} (q : AggQueryIn T (k + c) n κ) : AggQueryIn T c ((k + n) * (7 + k)) (ColKind.allReg ((k + n) * (7 + k)))

The table of a query: its symbolic evaluation relative to its cut, the encodings of its rows at every type of parameter row.

Equations

• Sym.tabQ cnt f q = Sym.sym (Sym.tabEnv cnt f q) (Sym.part f 2) q

theorem Sym.tabQ_correct {T : Type} [ValueType T] {k c : ℕ} (Θ : Set (SeqAggFunc T)) {cnt : SeqAggFunc T} (hc : cnt.Counts) (f : ℕ → String) {n : ℕ} {κ : Fin n → ColKind} (q : AggQueryIn T (k + c) n κ) (hU : AggQueryIn.usesOnly basisProdOps q) (hsrc : SymSrc Θ q) (hf : ∀ (i : ℕ), AggQueryIn.noMention (f i) q) (D : Database T) (γ : Fin c → T) (par : Fin k → T) (hset : q.SettlesAt D (Fin.append par γ)) : SliceIs (cutAt (tabEnv cnt f q) D γ) par ((tabQ cnt f q).evaluatePlain D γ) (Multiset.map (fun (v : Tuple T n) => (v, Fin.elim0)) (q.evaluatePlain D (Fin.append par γ))) ∧ ∀ (v : Tuple T n), Multiset.Mem (q.evaluatePlain D (Fin.append par γ)) v → ∀ (i : Fin n), GoodVal par (v i)

The table holds, under each parameter row's descriptor, the encodings of the rows the query computes at that row, wherever the query settles.

Home · Documentation · Publications · Contributors · Source · Cite