μ^∪ from μ^⊎

A set recursion μ^∪R.(q₀, q₁) whose recursive term is L(R) ⊎ C, with L reading R once under a projection, a selection, a product, the left side of an apply (and nothing else), is simulated by a bag recursion over pairs of a tuple and a counter: the base is (q₀ ⊎ C) × E^K for a relation E of counters, and a round applies L to the tuple part of every row and moves its counter to every strictly larger one (in the lexicographic order of E^K). A row's counters then form a strictly increasing chain, so the bag recursion ends after |E|^K rounds – it always settles – and its rounds carry, as sets, the rounds of the set recursion, which reach the fixpoint within |F| rounds, F the fixpoint. So ε(Π_tuple(S)) = F as soon as |E|^K ≥ |F| (AggQueryIn.evaluatePlain_simResult).

This module has the construction and its correctness for any counter relation E of non-null values that is large enough. What E can be read off the query is the other half: the values of the instance at the recursion's leaves, its constants and the context, with two constants of the domain (counterRel), and a width K fixed by the query. A count inside the term takes values that no such set enumerates, which is where the order-type lemma enters: the fixpoint is duplicate-free over those values and the counts the recursion computes, of which there are polynomially many (AggQueryIn.exists_card_bound_muSet in Provenance.Genericity), so |F| ≤ |E|^K for a K read off that polynomial.

Linear recursive terms

The typing of a recursive term admits the recursive relation under a ⊎, with the other side closed; the simulation needs the term without that side – which is the q₁' half of the split the generation pass produces – and reading the relation at a fixed arity.

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

A term reading the recursive relation s once, at arity n, and linearly: under a projection, a selection on regular columns, either side of a product or the left side of an apply, with the other side closed. No ⊎: its closed side is the C of q₁ = L ⊎ C.

Equations

• AggQueryIn.recLinear s n (AggQueryIn.Rel x✝ a) = False
• AggQueryIn.recLinear s n (AggQueryIn.Hole x✝¹ s' x✝) = (s' = s ∧ x✝¹ = n)
• AggQueryIn.recLinear s n (AggQueryIn.Param pv x✝) = False
• AggQueryIn.recLinear s n AggQueryIn.Empty = False
• AggQueryIn.recLinear s n (AggQueryIn.Proj ps q) = AggQueryIn.recLinear s n q
• AggQueryIn.recLinear s n (AggQueryIn.Sel φ q hφ) = (φ.hasAggAtom = false ∧ AggQueryIn.recLinear s n q)
• AggQueryIn.recLinear s n (q₁.Prod q₂) = (AggQueryIn.recLinear s n q₁ ∧ l₂ = [] ∧ AggQueryIn.noMention s q₂ ∨ l₁ = [] ∧ AggQueryIn.noMention s q₁ ∧ AggQueryIn.recLinear s n q₂)
• AggQueryIn.recLinear s n (q₁.Apply q₂) = (AggQueryIn.recLinear s n q₁ ∧ AggQueryIn.noMention s q₂)
• AggQueryIn.recLinear s n (a.Sum a_1) = False
• AggQueryIn.recLinear s n (AggQueryIn.Explode k a q) = AggQueryIn.recLinear s n q
• AggQueryIn.recLinear s n (AggQueryIn.Retag h q) = AggQueryIn.recLinear s n q
• AggQueryIn.recLinear s n a.Dedup = False
• AggQueryIn.recLinear s n (a.Diff a_1) = False
• AggQueryIn.recLinear s n (AggQueryIn.Mu s_1 a a_1) = False
• AggQueryIn.recLinear s n (AggQueryIn.MuSet s_1 a a_1) = False
• AggQueryIn.recLinear s n (AggQueryIn.Gamma is ts fs a keep ord) = False
• AggQueryIn.recLinear s n (AggQueryIn.GammaScalar ts fs a ord) = False
• AggQueryIn.recLinear s n (AggQueryIn.GammaNest is his p f a) = False
• AggQueryIn.recLinear s n (AggQueryIn.ProvSum is his t a) = False
• AggQueryIn.recLinear s n (AggQueryIn.GammaTok is his ts fs a a_1 keep) = False
• AggQueryIn.recLinear s n (AggQueryIn.Win P O o w t f a a_1 dist keep) = False
• AggQueryIn.recLinear s n (AggQueryIn.WinExpr P O o ws ts fs g a keeps) = False

The rounds of a set recursion reach its fixpoint within its size

Counters: strictly increasing chains in a finite order

def chainBag {β : Type} (r : β → β → Prop) [DecidableRel r] (Cb : Multiset β) : ℕ → Multiset β

The bag of counters a row can hold after j moves: the whole set at first, then the counters strictly above a counter of the previous round.

Equations

• chainBag r Cb 0 = Cb
• chainBag r Cb j.succ = (chainBag r Cb j).bind fun (c : β) => Multiset.filter (fun (c' : β) => r c c') Cb

Replacing the recursive relation by a query

def subIdx (s : String) (n : ℕ) (l : List (String × ℕ)) : List (String × ℕ)

The holes of a term, the recursive relation's taken out.

Equations

• subIdx s n l = List.filter (fun (p : String × ℕ) => decide (p ≠ (s, n))) l

theorem subIdx_append (s : String) (n : ℕ) (l₁ l₂ : List (String × ℕ)) : subIdx s n (l₁ ++ l₂) = subIdx s n l₁ ++ subIdx s n l₂

theorem subIdx_self (s : String) (n : ℕ) : subIdx s n [(s, n)] = []

theorem subIdx_single_ne {s s' : String} {n n' : ℕ} (h : ¬(s' = s ∧ n' = n)) : subIdx s n [(s', n')] = [(s', n')]

def AggQueryIn.castIdx {T : Type} {c m : ℕ} {κ : Fin m → ColKind} {l l' : List (String × ℕ)} (h : l = l') (q : AggQueryIn T c m κ l) : AggQueryIn T c m κ l'

A term, its hole index rewritten.

Equations

• AggQueryIn.castIdx h q = h ▸ q

theorem SelOK.sub {T : Type} {s : String} {n : ℕ} {l : List (String × ℕ)} {c m : ℕ} {κ : Fin m → ColKind} {φ : GenPredIn T c κ} (hφ : SelOK l φ) : SelOK (subIdx s n l) φ

Admissibility of a selection's predicate survives taking a hole out.

def AggQueryIn.substRel {T : Type} (s : String) {c n : ℕ} (pv : Fin n → T ⊕ Fin c) {m : ℕ} {κ : Fin m → ColKind} {l : List (String × ℕ)} : AggQueryIn T c m κ l → AggQueryIn T c m κ (subIdx s n l)

The recursive relation replaced by one row read off the context: every hole of its name and arity becomes the parameter leaf reading pv, at the hole's own kinds, so the holes of the result are the term's with that one taken out; nothing else is touched.

Equations

• One or more equations did not get rendered due to their size.
• AggQueryIn.substRel s pv (AggQueryIn.Param pv' x✝) = AggQueryIn.Param pv' x✝
• AggQueryIn.substRel s pv (AggQueryIn.Proj ps q) = AggQueryIn.Proj ps (AggQueryIn.substRel s pv q)
• AggQueryIn.substRel s pv (AggQueryIn.Sel φ q hφ) = AggQueryIn.Sel φ (AggQueryIn.substRel s pv q) ⋯
• AggQueryIn.substRel s pv (q₁.Prod q₂) = AggQueryIn.castIdx ⋯ ((AggQueryIn.substRel s pv q₁).Prod (AggQueryIn.substRel s pv q₂))
• AggQueryIn.substRel s pv (q₁.Apply q₂) = (AggQueryIn.substRel s pv q₁).Apply q₂
• AggQueryIn.substRel s pv (q₁.Sum q₂) = AggQueryIn.castIdx ⋯ ((AggQueryIn.substRel s pv q₁).Sum (AggQueryIn.substRel s pv q₂))
• AggQueryIn.substRel s pv (AggQueryIn.Explode k hk q) = AggQueryIn.Explode k hk (AggQueryIn.substRel s pv q)
• AggQueryIn.substRel s pv (AggQueryIn.Retag hk q) = AggQueryIn.Retag hk (AggQueryIn.substRel s pv q)
• AggQueryIn.substRel s pv (AggQueryIn.Rel x✝ s') = AggQueryIn.Rel x✝ s'
• AggQueryIn.substRel s pv AggQueryIn.Empty = AggQueryIn.Empty
• AggQueryIn.substRel s pv q.Dedup = q.Dedup
• AggQueryIn.substRel s pv (q₁.Diff q₂) = q₁.Diff q₂
• AggQueryIn.substRel s pv (AggQueryIn.Mu s' q₀ q₁) = AggQueryIn.Mu s' q₀ q₁
• AggQueryIn.substRel s pv (AggQueryIn.MuSet s' q₀ q₁) = AggQueryIn.MuSet s' q₀ q₁
• AggQueryIn.substRel s pv (AggQueryIn.Gamma is ts fs q keep ord) = AggQueryIn.Gamma is ts fs q keep ord
• AggQueryIn.substRel s pv (AggQueryIn.GammaScalar ts fs q ord) = AggQueryIn.GammaScalar ts fs q ord
• AggQueryIn.substRel s pv (AggQueryIn.GammaNest is his p f q) = AggQueryIn.GammaNest is his p f q
• AggQueryIn.substRel s pv (AggQueryIn.ProvSum is his t q) = AggQueryIn.ProvSum is his t q
• AggQueryIn.substRel s pv (AggQueryIn.GammaTok is his ts fs a q keep) = AggQueryIn.GammaTok is his ts fs a q keep
• AggQueryIn.substRel s pv (AggQueryIn.Win P O o w t f q hrr dist keep) = AggQueryIn.Win P O o w t f q hrr dist keep
• AggQueryIn.substRel s pv (AggQueryIn.WinExpr P O o ws ts fs g q_1 keeps) = AggQueryIn.WinExpr P O o ws ts fs g q_1 keeps

The counters: a power of a unary relation, read lexicographically

def AggQueryIn.pow {T : Type} {c : ℕ} (EQ : AggQueryIn T c 1 (ColKind.allReg 1)) (K : ℕ) : AggQueryIn T c K (ColKind.allReg K)

E^K, the K-fold product of a unary relation.

Equations

• EQ.pow 0 = AggQueryIn.unitC
• EQ.pow j.succ = (EQ.pow j).prodA EQ

def AggQueryIn.unaryVals {T : Type} (E : Multiset (Tuple T 1)) : Multiset T

The values of a unary relation.

Equations

• AggQueryIn.unaryVals E = Multiset.map (fun (y : Tuple T 1) => y 0) E

The lexicographic order on the counters is a total order

def ascLe {T : Type} [ValueType T] (p : ℕ) (x y : Tuple T p) : Prop

The relation the counters are sorted by.

Equations

• ascLe p x y = ((OrderSpec.asc p).le x y = true)

def ascLt {T : Type} [ValueType T] (p : ℕ) (x y : Tuple T p) : Prop

And the strict one the rounds move along.

Equations

• ascLt p x y = ((OrderSpec.asc p).lt x y = true)

@[instance_reducible]

instance instDecidableRelTupleAscLe {T : Type} [ValueType T] (p : ℕ) : DecidableRel (ascLe p)

Equations

• instDecidableRelTupleAscLe p x y = id inferInstance

@[instance_reducible]

instance instDecidableRelTupleAscLt {T : Type} [ValueType T] (p : ℕ) : DecidableRel (ascLt p)

Equations

• instDecidableRelTupleAscLt p x y = id inferInstance

instance instIsTransTupleAscLe {T : Type} [ValueType T] (p : ℕ) : IsTrans (Tuple T p) (ascLe p)

instance instAntisymmTupleAscLe {T : Type} [ValueType T] (p : ℕ) : Std.Antisymm (ascLe p)

instance instTotalTupleAscLe {T : Type} [ValueType T] (p : ℕ) : Std.Total (ascLe p)

instance instIrreflTupleAscLt {T : Type} [ValueType T] (p : ℕ) : Std.Irrefl (ascLt p)

The construction

def AggQueryIn.dropLeft {T : Type} (n K : ℕ) : Tuple T (n + K + (n + K)) → Tuple T (n + K)

The columns of the right side of the apply the round is built on.

Equations

• AggQueryIn.dropLeft n K w j = w (Fin.natAdd (n + K) j)

def AggQueryIn.leftPart {T : Type} (n K : ℕ) (u : Tuple T (n + K)) : Tuple T n

The tuple part of a row of the simulation.

Equations

• AggQueryIn.leftPart n K u i = u (Fin.castAdd K i)

def AggQueryIn.rightPart {T : Type} (n K : ℕ) (u : Tuple T (n + K)) : Tuple T K

And its counter.

Equations

• AggQueryIn.rightPart n K u k = u (Fin.natAdd n k)

def AggQueryIn.rowPv {T : Type} {c : ℕ} (n K : ℕ) : Fin n → T ⊕ Fin (n + K + c)

The current row's tuple part, read off the outer columns of the apply: the parameters a hole of the recursive term is replaced by.

Equations

• AggQueryIn.rowPv n K i = Sum.inr (Fin.castAdd c (Fin.castAdd K i))

def AggQueryIn.ltSel {T : Type} [ValueType T] {c : ℕ} (n K : ℕ) : GenPredIn T (n + K + c) (ColKind.allReg K)

The counter moves up: the row's counter is strictly above the current row's, lexicographically.

Equations

• AggQueryIn.ltSel n K = (OrderSpec.asc K).ltPredOn (fun (k : Fin K) => TermGIn.outer (Fin.castAdd c (Fin.natAdd n k))) (fun (k : Fin K) => TermGIn.index k ⋯) (List.finRange K)

def AggQueryIn.simBody {T : Type} [ValueType T] {c : ℕ} (s s' : String) (n K : ℕ) (EQ : AggQueryIn T c 1 (ColKind.allReg 1)) (L : AggQueryIn T c n (ColKind.allReg n) [(s, n)]) : AggQueryIn T c (n + K) (ColKind.allReg (n + K)) [(s', n + K)]

One round of the simulation: for each row of the recursive relation, the term at the row's tuple part, paired with every counter above the row's.

Equations

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

The simulation, and what it computes

def AggQueryIn.pairRel {T : Type} {n K : ℕ} (A : Multiset (Tuple T n)) (M : Multiset (Tuple T K)) : Multiset (Tuple T (n + K))

The product of two relations, as the bag of appended rows.

Equations

• AggQueryIn.pairRel A M = A.bind fun (a : Tuple T n) => Multiset.map (fun (m : Fin K → T) => Fin.append a m) M

def AggQueryIn.sim {T : Type} [ValueType T] {c : ℕ} (s s' : String) (n K : ℕ) (EQ : AggQueryIn T c 1 (ColKind.allReg 1)) (BQ : AggQueryIn T c n (ColKind.allReg n)) (L : AggQueryIn T c n (ColKind.allReg n) [(s, n)]) : AggQueryIn T c (n + K) (ColKind.allReg (n + K))

The simulation: a bag recursion over rows pairing a tuple with a counter, from (q₀ ⊎ C) × E^K, each round applying the term to the tuple part and moving the counter up.

Equations

• AggQueryIn.sim s s' n K EQ BQ L = AggQueryIn.Mu s' (BQ.prodA (EQ.pow K)) (AggQueryIn.simBody s s' n K EQ L)

theorem AggQueryIn.dedupG_kinds (n : ℕ) : (fun (j : Fin (n + 0)) => Fin.append (ColKind.allReg n) (fun (x : Fin 0) => ColKind.agg) j) = ColKind.allReg (n + 0)

def AggQueryIn.dedupG {T : Type} {c n : ℕ} (q : AggQueryIn T c n (ColKind.allReg n)) : AggQueryIn T c n (ColKind.allReg n)

Duplicate elimination as a grouping by every column with no aggregate: the shape the bases without ε use.

Equations

• q.dedupG = AggQueryIn.castKind ⋯ (AggQueryIn.Gamma (fun (k : Fin n) => k) (fun (j : Fin 0) => j.elim0) (fun (j : Fin 0) => j.elim0) q)

def AggQueryIn.simResult {T : Type} [ValueType T] {c : ℕ} (s s' : String) (n K : ℕ) (EQ : AggQueryIn T c 1 (ColKind.allReg 1)) (BQ : AggQueryIn T c n (ColKind.allReg n)) (L : AggQueryIn T c n (ColKind.allReg n) [(s, n)]) : AggQueryIn T c n (ColKind.allReg n)

Its tuple parts, without duplicates: the set recursion's value.

Equations

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

noncomputable def AggQueryIn.rowTerm {T : Type} [ValueType T] {c : ℕ} (s : String) (n : ℕ) (L : AggQueryIn T c n (ColKind.allReg n) [(s, n)]) (D : Database T) (γ : Fin c → T) : Tuple T n → Multiset (Tuple T n)

The term applied to one row of the recursive relation.

Equations

• AggQueryIn.rowTerm s n L D γ t = L.evaluatePlain (Database.assign s {t} D) γ

noncomputable def AggQueryIn.simStep {T : Type} [ValueType T] {c : ℕ} (s s' : String) (n K : ℕ) (EQ : AggQueryIn T c 1 (ColKind.allReg 1)) (L : AggQueryIn T c n (ColKind.allReg n) [(s, n)]) (D : Database T) (γ : Fin c → T) : Multiset (Tuple T (n + K)) → Multiset (Tuple T (n + K))

One round of the simulation, as a function of the recursive relation.

Equations

• AggQueryIn.simStep s s' n K EQ L D γ Y = (AggQueryIn.simBody s s' n K EQ L).evaluatePlain (Database.assign s' Y D) γ

noncomputable def AggQueryIn.counters {T : Type} [ValueType T] {c : ℕ} (EQ : AggQueryIn T c 1 (ColKind.allReg 1)) (K : ℕ) (D : Database T) (γ : Fin c → T) : Multiset (Tuple T K)

The counters.

Equations

• EQ.counters K D γ = (EQ.pow K).evaluatePlain D γ

The set recursion's rounds, as the term iterated on the base

def bagStep {α : Type} (B : Multiset α) (L₁ : α → Multiset α) (X : Multiset α) : Multiset α

The step of a set recursion μ^∪R.(B, L(R)) with L linear, as a bag before the duplicate elimination.

Equations

• bagStep B L₁ X = B + X.bind L₁

The simulation computes the set recursion

theorem AggQueryIn.evaluatePlain_simResult {T : Type} [ValueType T] {c : ℕ} (s s' : String) (n K : ℕ) (EQ : AggQueryIn T c 1 (ColKind.allReg 1)) (BQ qC q₀ : AggQueryIn T c n (ColKind.allReg n)) (L q₁ : AggQueryIn T c n (ColKind.allReg n) [(s, n)]) (hL : recLinear s n L) (hLs : noMention s' L) (hEs : noMention s' EQ) (hC : noMention s qC) (D : Database T) (γ : Fin c → T) (hset : (MuSet s q₀ q₁).SettlesAt D γ) (hsplit : ∀ (X : Relation T n), q₁.SettlesAt (Database.assign s X D) γ → q₁.evaluatePlain (Database.assign s X D) γ = L.evaluatePlain (Database.assign s X D) γ + qC.evaluatePlain (Database.assign s X D) γ) (hB : BQ.evaluatePlain D γ = q₀.evaluatePlain D γ + qC.evaluatePlain D γ) (hE : ∀ e ∈ unaryVals (EQ.evaluatePlain D γ), ValueType.isNull e = false) (hcard : Multiset.card ((MuSet s q₀ q₁).evaluatePlain D γ) ≤ (unaryVals (EQ.evaluatePlain D γ)).toFinset.card ^ K) : (simResult s s' n K EQ BQ L).evaluatePlain D γ = (MuSet s q₀ q₁).evaluatePlain D γ ∧ ∀ (j : ℕ) (t : Tuple T n), j < (EQ.counters K D γ).toFinset.card → t ∈ (fun (X : Multiset (Tuple T n)) => X.bind (rowTerm s n L D γ))^[j] (BQ.evaluatePlain D γ) → Multiset.Mem ((MuSet s q₀ q₁).evaluatePlain D γ) t

μ^∪ from μ^⊎ (the correctness of the construction): for a set recursion μ^∪R.(q₀, q₁) whose term splits as L ⊎ C with L linear, a base query computing q₀ ⊎ C, and a counter relation E of non-null values with |E|^K at least the size of the fixpoint, the simulation's tuples are the fixpoint, wherever the recursion is defined.

The counter relation

The simulation runs its counter over E^K for a unary relation E of non-null values with |E|^K at least the size of the fixpoint. E is computed from what the fixpoint's values can be – the values of the base (so of q₀ and of C), of the relations the term reads off the instance, the term's constants and the context's values – with two constants of the domain so that it holds at least two values, and a selection keeping the non-null ones.

def AggQueryIn.listSum {T : Type} [ValueType T] {c n : ℕ} : List (AggQueryIn T c n (ColKind.allReg n)) → AggQueryIn T c n (ColKind.allReg n)

The sum of a list of queries.

Equations

• AggQueryIn.listSum [] = AggQueryIn.emptyRel n
• AggQueryIn.listSum (q :: l) = q.Sum (AggQueryIn.listSum l)

def AggQueryIn.colRel {T : Type} {c n : ℕ} (q : AggQueryIn T c n (ColKind.allReg n)) (i : Fin n) : AggQueryIn T c 1 (ColKind.allReg 1)

Column i of a query, as a unary relation.

Equations

• q.colRel i = AggQueryIn.castKind AggQueryIn.colRel._proof_1 (AggQueryIn.Proj (fun (x : Fin 1) => ProjColIn.term (TermGIn.index i ⋯)) q)

def AggQueryIn.constRel {T : Type} {c : ℕ} (a : T) : AggQueryIn T c 1 (ColKind.allReg 1)

A constant, as a one-row unary relation.

Equations

• AggQueryIn.constRel a = AggQueryIn.castKind AggQueryIn.colRel._proof_1 (AggQueryIn.Proj (fun (x : Fin 1) => ProjColIn.term (TermGIn.const a)) AggQueryIn.unitC)

def AggQueryIn.outerRel {T : Type} {c : ℕ} (j : Fin c) : AggQueryIn T c 1 (ColKind.allReg 1)

A context value, as a one-row unary relation.

Equations

• AggQueryIn.outerRel j = AggQueryIn.castKind AggQueryIn.colRel._proof_1 (AggQueryIn.Proj (fun (x : Fin 1) => ProjColIn.term (TermGIn.outer j)) AggQueryIn.unitC)

def AggQueryIn.nonNullPred {T : Type} {c : ℕ} : GenPredIn T c (ColKind.allReg 1)

x IS NOT NULL, spelled x = x: the comparison is unknown exactly at the null.

Equations

• AggQueryIn.nonNullPred = GenPredIn.cmp CompOp.eq (TermGIn.index 0 AggQueryIn.nonNullPred._proof_1) (TermGIn.index 0 AggQueryIn.nonNullPred._proof_1)

def AggQueryIn.counterParts {T : Type} {c n : ℕ} (B : AggQueryIn T c n (ColKind.allReg n)) (ls : List (ℕ × String)) (cs : List T) : List (AggQueryIn T c 1 (ColKind.allReg 1))

The unary relations the counter relation is the union of.

Equations

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

def AggQueryIn.counterRel {T : Type} [ValueType T] {c n : ℕ} (B : AggQueryIn T c n (ColKind.allReg n)) (ls : List (ℕ × String)) (cs : List T) : AggQueryIn T c 1 (ColKind.allReg 1)

The counter relation: the non-null values among the columns of B, the columns of the relations ls names, the constants cs and the context's values.

Equations

• B.counterRel ls cs = AggQueryIn.Sel AggQueryIn.nonNullPred (AggQueryIn.listSum (B.counterParts ls cs)) ⋯

What the simulation is made of

The structural facts the pass needs of the simulation: which classes it uses, that its recursion is restricted, its signature, its schema, its names. Each is read off its parts.

Bridges for the pass

The set recursion replaced

The simulation as the pass needs it: where the target classes hold no μ^∪, a set recursion is replaced by the simulation – its base the rewritten base and closed part summed, its term the rewritten body, its counter the counter relation over the values the fixpoint can hold – and the unions the counter relation is built with go by the bag recursion afterwards.

The whole algebra with one recursion

def basisRecOps : Set OpKind

The basis of the whole algebra in the minimal universe: the construction's classes and the windows, {∅, Π, σ, apply, γ, win, μ^⊎}. basisRecOps_generatesOnRec says it generates, and Provenance.RecursionBasisTheorem that no proper subset does.

Equations

• basisRecOps = insert OpKind.win AggQueryIn.sumMuOps

theorem basisRecOps_generatesOnRec {T : Type} [ValueType T] (sch : Schema) (cnt : SeqAggFunc T) (hcnt : cnt.IsCount) : GeneratesOnRec T sch cnt basisRecOps

μ^∪ is not needed, for every restricted term: over a schema declaring finitely many names, every query of the whole algebra in the minimal universe with restricted recursions is matched over ∅, Π, σ, the apply, γ, win and μ^⊎ – defined wherever the query is and equal to it there. A set recursion is simulated by a bag recursion whose counter runs over the instance's values at the recursion's leaves, the recursion's constants and its context: the fixpoint is duplicate-free over those values and the counts the recursion computes, of which there are polynomially many (AggQueryIn.exists_card_bound_muSet, off the order types of Provenance.Genericity), so a counter of a width fixed by the query covers it. With the necessary classes (required_mem_of_generatesOnRec), a basis of the whole algebra in the minimal universe is ∅, Π, γ, μ^⊎, one of σ and −, one of × and the apply, and win (Provenance.WinRow); μ^∪ is in none.

theorem sumMuOps_generatesOnRec_of_winsDerivable {T : Type} [ValueType T] (sch : Schema) (cnt : SeqAggFunc T) (hcnt : cnt.IsCount) {n : ℕ} {κ : Fin n → ColKind} (q : AggQuery T n κ) (ho : AggQueryIn.overSchema sch q) (hq : AggQueryIn.usesOnly plainRecOps q) (hi : AggQueryIn.inMinimalSig cnt q) (hw : AggQueryIn.WinsDerivable q) : ∃ (q' : AggQuery T n (ColKind.allReg n)), AggQueryIn.overSchema sch q' ∧ AggQueryIn.usesOnly AggQueryIn.sumMuOps q' ∧ AggQueryIn.inMinimalSig cnt q' ∧ AggQueryIn.Extends q' q

And without the window class, for the windows an apply derives (evaluatePlain_winByApplyOf): the six classes ∅, Π, σ, the apply, γ and μ^⊎ match every query of the whole algebra in the minimal universe whose windows are derivable (AggQueryIn.WinsDerivable).

Home · Documentation · Publications · Contributors · Source · Cite