The bases of the whole algebra, all of them

A recursive term reads its recursive relation under a projection, a selection, either side of a product, the left side of an apply, either side of a union, Explode and Retag, and nowhere else. Of these only a selection and an apply can drop a row: without them a round has k · |X| rows for a k that does not depend on the round X, so a bag recursion that settles is its base (AggQueryIn.evaluatePlain_mu_degenerate), and the algebra is left with polynomial answers, which the chain of diamonds refutes. So σ or the apply is in every basis (sel_or_apply_mem_of_generatesOnRec), and {∅, Π, −, ×, γ, win, μ^⊎} is not one. With the other rows this classifies the generating sets completely (generatesOnRec_iff): they are the supersets of the three bases basisRecOps, Sym.basisProdOps and basisRecDiffOps.

A recursive term that drops no row

theorem AggQueryIn.evaluatePlain_mu_degenerate {T : Type} [ValueType T] {S : Set OpKind} (hsel : OpKind.sel ∉ S) (hap : OpKind.apply ∉ S) {c n : ℕ} {κ : Fin n → ColKind} (s : String) (q₀ : AggQueryIn T c n κ) (q₁ : AggQueryIn T c n κ [(s, n)]) (hu : usesOnly S q₁) (hm : noMention s q₁) (D : Database T) (γ : Fin c → T) (h : (Mu s q₀ q₁).SettlesAt D γ) : (Mu s q₀ q₁).evaluatePlain D γ = q₀.evaluatePlain D γ

A bag recursion whose term drops no row is its base, wherever it settles: its rounds have k^j · |M| rows, so one of them is empty only if k or the base is.

Dropping such recursions

theorem AggQueryIn.exists_dropMu {T : Type} [ValueType T] {S : Set OpKind} (hsel : OpKind.sel ∉ S) (hap : OpKind.apply ∉ S) {c n : ℕ} {κ : Fin n → ColKind} {l : List (String × ℕ)} (q : AggQueryIn T c n κ l) : usesOnly S q → q.hygienic → ∃ (q' : AggQueryIn T c n κ l), usesOnly (S \ {OpKind.muBag}) q' ∧ q'.hygienic ∧ (∀ (Θ : Set (SeqAggFunc T)), inSig Θ q → inSig Θ q') ∧ (∀ (x : String), noMention x q → noMention x q') ∧ ∀ (D : Database T) (γ : Fin c → T), q.SettlesAt D γ → q'.SettlesAt D γ ∧ q.evaluatePlain D γ = q'.evaluatePlain D γ

Over classes with no selection and no apply, every bag recursion can be replaced by its base: the result has no bag recursion, keeps the hygiene, the signature and the names not mentioned, and is defined and equal wherever the source is.

The row, and the classification

theorem sel_or_apply_mem_of_generatesOnRec {cnt : SeqAggFunc ℕ} (hcnt : cnt.ReadsCount) {S : Set OpKind} (hS : GeneratesOnRec ℕ schemaSE cnt S) : OpKind.sel ∈ S ∨ OpKind.apply ∈ S

σ or the apply is in every basis of the whole algebra.

theorem not_generatesOnRec_prodDiff : ¬GeneratesOnRec ℕ schemaSE SeqAggFunc.count {OpKind.empty, OpKind.proj, OpKind.diff, OpKind.prod, OpKind.gamma, OpKind.win, OpKind.muBag}

The difference and the product together are not a basis: {∅, Π, −, ×, γ, win, μ^⊎} does not generate the whole algebra in the minimal universe.

theorem generatesOnRec_iff {S : Set OpKind} : (∀ (sch : Schema), GeneratesOnRec ℕ sch SeqAggFunc.count S) ↔ basisRecOps ⊆ S ∨ Sym.basisProdOps ⊆ S ∨ basisRecDiffOps ⊆ S

The generating sets of the whole algebra in the minimal universe, over ℕ with the counting aggregate: exactly the supersets of one of the three bases, {∅, Π, σ, apply, γ, win, μ^⊎}, {∅, Π, σ, ×, γ, win, μ^⊎} and {∅, Π, −, apply, γ, win, μ^⊎}.

Home · Documentation · Publications · Contributors · Source · Cite