The apply replaced by products, through a whole query

Provenance.SymApply writes one apply with products (Sym.applyX), given its right side in the fragment without the apply and a closed pool: a unary query holding every value of the left side's rows. This module runs that replacement through a query over {∅, Π, σ, apply, γ, win, μ^⊎}, from the leaves up, so that every query of that fragment is matched by one over {∅, Π, σ, ×, γ, win, μ^⊎} (Sym.basisProdOps).

The pool of an apply outside a recursion is the values of its left side. Inside a recursive term the left side reads the round, so its values are those of the round and those the term creates; the latter are bounded by a closed query (Cr), built from the leaves up alongside the term: the constants and context values a projection may emit, and the cut of each apply's right side. A recursion's rounds then hold only values of its base and of its body's Cr, and that closed union is the pool W its body's applies read. Each recursion is renamed to a name of the supply, as the copies of its base the pool holds would otherwise nest a recursion inside one of the same name.

Reading an instance away from a name

A bag recursion under another name

The names a term's pass binds around its pool

inductive Sym.Enc : (ℕ → String) → String → Prop

The names the pass of a recursive term binds around the pool it is given: at each apply on the way to the hole, the union building the apply's pool (slice 4) and the union inside the apply over it (slice 1 of the apply's own supply); the child on the way to the hole has slice 1.

• vq (f : ℕ → String) (i : ℕ) : Enc f (part f 4 i)
• vs (f : ℕ → String) (i : ℕ) : Enc f (part (part f 0) 1 i)
• down (f : ℕ → String) (x : String) : Enc (part f 1) x → Enc f x

A window kept is of the fragment

The values an apply's right side creates

The pass

def Sym.CrN (A : String → Prop) (f : ℕ → String) : String → Prop

The names a pass with supply f gives the values it creates: its input's, and its supply's away from those binding around a pool.

Equations

• Sym.CrN A f x = (A x ∨ ∃ (i : ℕ), x = f i ∧ ¬Sym.Enc f x)

def Sym.InVals {T : Type} {m : ℕ} (X : Multiset (Tuple T m)) (a : T) : Prop

A value of a row of X.

Equations

• Sym.InVals X a = ∃ (u : Tuple T m), X.Mem u ∧ ∃ (j : Fin m), u j = a

The queries bounding created values

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

The constants and the context values a projection may emit.

Equations

• Sym.emitQ f S = Sym.u2 (Sym.part f 5) (Sym.constsQ (Sym.part f 6) S) (Sym.ambQ (Sym.part f 7) c)

A projection re-typed

def Sym.projReg {T : Type} [ValueType T] {c N M : ℕ} {κ : Fin N → ColKind} {l : List (String × ℕ)} (ps : Fin M → ProjColIn T c κ) (p : AggQueryIn T c N (ColKind.allReg N) l) : AggQueryIn T c M (ColKind.allReg M) l

A projection with its columns read as regular ones.

Equations

• Sym.projReg ps p = AggQueryIn.castKind ⋯ (AggQueryIn.Proj (fun (j : Fin M) => (ps j).toReg) p)

Names of slices

theorem Sym.exists_prodPass_aux {T : Type} [ValueType T] {Θ : Set (SeqAggFunc T)} {cnt : SeqAggFunc T} (hcnt : cnt ∈ Θ) (hc : cnt.Counts) (hRC : ∀ g ∈ Θ, g.ReadsCount) {c n : ℕ} {κ : Fin n → ColKind} {l : List (String × ℕ)} (q : AggQueryIn T c n κ l) : AggQueryIn.usesOnly basisRecOps q → AggQueryIn.inSig Θ q → q.hygienic → ∀ (sch : Schema) (A : String → Prop) (f : ℕ → String), SupOK sch A f → RelsIn sch A q → (l = [] → ∃ (q' : AggQueryIn T c n (ColKind.allReg n)), Fine Θ q' ∧ Over sch (Sup A f) q' ∧ ∀ (D : Database T) (γ : Fin c → T), q.SettlesAt D γ → q'.SettlesAt D γ ∧ q.evaluatePlain D γ = q'.evaluatePlain D γ) ∧ ∀ (s : String) (m : ℕ), l = [(s, m)] → AggQueryIn.noMention s q → ∃ (Cr : AggQueryIn T c 1 (ColKind.allReg 1)), Fine Θ Cr ∧ Over sch (CrN A f) Cr ∧ (∀ (D : Database T) (γ : Fin c → T), Cr.SettlesAt D γ) ∧ (∀ (D : Database T) (γ : Fin c → T) (X : Relation T m), q.SettlesAt (Database.assign s X D) γ → ∀ (v : Tuple T n), Multiset.Mem (q.evaluatePlain (Database.assign s X D) γ) v → ∀ (i : Fin n), InVals X (v i) ∨ v i ∈ valsU (Cr.evaluatePlain D γ)) ∧ ∀ (t : String) (B : String → Prop) (W : AggQueryIn T c 1 (ColKind.allReg 1)), sch.decl t = some m → ¬A t → (∀ (x : String), B x → ¬Enc f x ∧ x ≠ t) → Over sch B W → Fine Θ W → ∃ (q' : AggQueryIn T c n (ColKind.allReg n) [(t, m)]), Fine Θ q' ∧ Over sch (fun (x : String) => Sup A f x ∨ B x ∨ x = t) q' ∧ AggQueryIn.noMention t q' ∧ ∀ (D : Database T) (γ : Fin c → T) (X : Relation T m), q.SettlesAt (Database.assign s X D) γ → W.SettlesAt D γ → (∀ (u : Tuple T m), Multiset.Mem X u → ∀ (i : Fin m), u i ∈ valsU (W.evaluatePlain D γ)) → q'.SettlesAt (Database.assign t X D) γ ∧ q.evaluatePlain (Database.assign s X D) γ = q'.evaluatePlain (Database.assign t X D) γ

The pass, both halves at once. A closed query of {∅, Π, σ, apply, γ, win, μ^⊎} is matched by a query of the fragment with products and without the apply, defined and equal wherever it is. A recursive term reading the name s is matched, given a closed pool W holding the values of the round, by a term reading a name t in its place; and the values it creates are bounded by a closed query Cr, built before the pool is known.

The basis with products

theorem Sym.basisProdOps_generatesOnRec {T : Type} [ValueType T] (sch : Schema) (cnt : SeqAggFunc T) (hcnt : cnt.IsCount) : GeneratesOnRec T sch cnt basisProdOps

{∅, Π, σ, ×, γ, win, μ^⊎} generates the whole algebra in the minimal universe: every query of the algebra over a schema, in the signature with a count as its only aggregate, is matched by one over those seven classes, defined and equal wherever the query is. The product stands in for the apply: first the query is matched over {∅, Π, σ, apply, γ, win, μ^⊎} (basisRecOps_generatesOnRec), then each apply of the match is written with products (Sym.exists_prodPass_aux).

theorem Sym.basisProdOps_minimal {S : Set OpKind} (hS : S ⊂ basisProdOps) : ¬∀ (sch : Schema), GeneratesOnRec ℕ sch SeqAggFunc.count S

No proper subset of basisProdOps generates the whole algebra in the minimal universe over ℕ. The rows of required_mem_of_generatesOnRec force each class: σ because − is not in the set, and × because the apply is not.

theorem Sym.basisProdOps_isBasis : (∀ (sch : Schema), GeneratesOnRec ℕ sch SeqAggFunc.count basisProdOps) ∧ ∀ S ⊂ basisProdOps, ¬∀ (sch : Schema), GeneratesOnRec ℕ sch SeqAggFunc.count S

basisProdOps is a basis of the whole algebra in the minimal universe over ℕ: it generates over every schema, and no proper subset does.

Home · Documentation · Publications · Contributors · Source · Cite