The recursions in the classification

The basis classification grades the two recursion operators as it grades the others. This module carries the row of μ^⊎, the recursion of SQL's WITH RECURSIVE … UNION ALL: in the minimal signature, a query without it has at most p(n) tuples over an instance of n tuples, multiplicities included, for a polynomial p of the query, and a bag recursion breaks that, counting the derivations of a tuple rather than deriving it once.

The witness is a chain of n diamonds, 4n edges and no duplicate row, over which reachability from the source reaches the sink by 2ⁿ paths, so the sink carries that multiplicity. The query is μ^⊎R.(S, Π_{#3}(σ_{#1=#2}(R × E))), which is SQL's

WITH RECURSIVE R(x) AS (SELECT * FROM S UNION ALL
                        SELECT E.t FROM R, E WHERE R.x = E.s)
SELECT * FROM R

and the rounds are the layers of the graph: the recursion's i-th round holds the nodes at distance i from the source, each with its number of paths, and the round past the sink is empty, which is where SQL's iteration stops (MuSettles).

The instance: a chain of diamonds

def node (a : ℕ) : Tuple ℕ 1

A row of arity one, written so that the rows a projection builds are exactly it: Fin.cons reduces only under a case on the index, which would leave every computation below short of a funext.

Equations

• node a x✝ = a

def schemaSE : Schema

The schema of the witness: a source relation and an edge relation.

Equations

• schemaSE = Schema.ofFn (fun (s : String) => if s = "S" then some 1 else if s = "E" then some 2 else none) {"S", "E"} ⋯

def diamondEdges : ℕ → Multiset (Tuple ℕ 2)

The edges of a chain of n diamonds. Diamond i runs from 3i to 3(i+1) through the two nodes 3i+1 and 3i+2, so its four edges are distinct, no two diamonds share an edge, and the instance holds no duplicate row: the blow-up below is not one the instance already had.

Equations

• diamondEdges 0 = 0
• diamondEdges n.succ = diamondEdges n + {![3 * n, 3 * n + 1], ![3 * n, 3 * n + 2], ![3 * n + 1, 3 * n + 3], ![3 * n + 2, 3 * n + 3]}

def dChain (n : ℕ) : Database ℕ

The instance: the source (0) and the chain's edges.

Equations

• dChain n = [("S", ⟨1, {node 0}⟩), ("E", ⟨2, diamondEdges n⟩)]

The query, and one round of it

def reachStep : AggQueryIn ℕ 0 1 (ColKind.allReg 1) [("R", 1)]

The recursion's body: Π_{#3}(σ_{#1=#2}(R × E)), the successors of the previous round.

Equations

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

def chainWitness : AggQuery ℕ 1 (ColKind.allReg 1)

The witness: μ^⊎R.(S, Π_{#3}(σ_{#1=#2}(R × E))).

Equations

• chainWitness = AggQueryIn.Mu "R" (AggQueryIn.Rel 1 "S") reachStep

def succs (E : Multiset (Tuple ℕ 2)) (a : ℕ) : Multiset (Tuple ℕ 1)

The successors of a node, as rows of arity one.

Equations

• succs E a = Multiset.map (fun (e : Tuple ℕ 2) => node (e 1)) (Multiset.filter (fun (e : Tuple ℕ 2) => a = e 0) E)

theorem evaluatePlain_reachStep (n : ℕ) (X : Multiset (Tuple ℕ 1)) : (reachStep.evaluatePlain (Database.assign "R" X (dChain n)) fun (j : Fin 0) => j.elim0) = X.bind fun (u : Tuple ℕ 1) => succs (diamondEdges n) (u 0)

One round: every row of the previous round contributes its successors, with its own multiplicity.

The successors of a node in the chain

def diamond (i : ℕ) : Multiset (Tuple ℕ 2)

The four edges of diamond i.

Equations

• diamond i = {![3 * i, 3 * i + 1], ![3 * i, 3 * i + 2], ![3 * i + 1, 3 * i + 3], ![3 * i + 2, 3 * i + 3]}

The rounds are the layers of the chain

noncomputable def chainStep (n : ℕ) : Multiset (Tuple ℕ 1) → Multiset (Tuple ℕ 1)

The round function of the witness over the chain of n diamonds.

Equations

• chainStep n X = reachStep.evaluatePlain (Database.assign "R" X (dChain n)) fun (j : Fin 0) => j.elim0

theorem chainStep_iterate_even {n : ℕ} (i : ℕ) : i ≤ n → (chainStep n)^[2 * i] {node 0} = Multiset.replicate (2 ^ i) (node (3 * i))

The even rounds: the entry node of diamond i, with one copy per path to it – 2ⁱ of them, the diamonds doubling the count.

theorem chainStep_iterate_odd {n : ℕ} (i : ℕ) (h : i < n) : (chainStep n)^[2 * i + 1] {node 0} = Multiset.replicate (2 ^ i) (node (3 * i + 1)) + Multiset.replicate (2 ^ i) (node (3 * i + 2))

The odd rounds: the two sides of diamond i.

theorem muSettles_chain (n : ℕ) : MuSettles (chainStep n) {node 0}

The recursion settles: the graph is acyclic, so the rounds end.

The sink's multiplicity

The row: no polynomial bounds a bag recursion

theorem count_chainWitness (n : ℕ) : Multiset.count (node (3 * n)) (AggQueryIn.evaluatePlain chainWitness (dChain n) fun (j : Fin 0) => j.elim0) = 2 ^ n

The sink of the chain carries 2ⁿ copies: one per path through the n diamonds, which is what a bag recursion counts.

theorem chainWitness_no_polynomial_bound : ¬∃ (c : ℕ) (k : ℕ), ∀ (n : ℕ), Multiset.card (AggQueryIn.evaluatePlain chainWitness (dChain n) fun (j : Fin 0) => j.elim0) ≤ c * ((dChain n).size + 1) ^ k

μ^⊎ is in every basis: a bag recursion counts the derivations of a tuple, and over the chain of n diamonds – 4n + 1 rows, none of them duplicated – the sink has 2ⁿ of them, which no polynomial in the size of the instance bounds. Every other operator of the minimal signature keeps the result polynomial.

Half of the invariant: the operators that are not a recursion

The necessity of μ^⊎ rests on an invariant: a query without it has at most p(n) tuples over an instance of n tuples, multiplicities included. The operators other than the two recursions bound their result by sums and products of the bounds of their arguments, in numbers fixed by the query, and an apply by the bound of its left side times that of its right side – which does not depend on the parameters, so the bound is uniform in the context. That is this section; the set recursion is the other half, and is where the minimal signature comes in.

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

No recursion.

Equations

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

theorem AggQueryIn.exists_polyBound {T : Type} [ValueType T] {c n : ℕ} {κ : Fin n → ColKind} {l : List (String × ℕ)} (q : AggQueryIn T c n κ l) : q.noRec → ∃ (b : ℕ) (k : ℕ), ∀ (D : Database T) (γ : Fin c → T), Multiset.card (q.evaluatePlain D γ) ≤ b * (D.size + 1) ^ k

A recursion-free query has polynomially many rows, multiplicities included, and the polynomial is uniform in the context: an apply's right side is bounded independently of the parameters it reads.

What the values of a result can be

The necessity of μ^⊎ reads the values of a result, not only its size: in the minimal signature a value is one of the instance, a constant of the query, or a count, and a count is bounded by the size of what it counts. That is what bounds a set recursion, whose fixpoint has no bound in terms of its arguments': a duplicate-free relation of arity k over |V| values has at most |V|^k rows.

def Relation.valsIn {T : Type} {n : ℕ} (r : Multiset (Tuple T n)) (V : Finset T) : Prop

Every value of the relation lies in V. The argument is spelled as a multiset and not as a Relation, which is an opaque def that instance search for ∈ and ≤ cannot see through.

Equations

• Relation.valsIn r V = ∀ u ∈ r, ∀ (j : Fin n), u j ∈ V

def SeqAggFunc.ReadsCount {T : Type} [ValueType T] (cnt : SeqAggFunc T) : Prop

An aggregate that reads only how many non-null values it is given: its value is a function of that number. This is what the genericity of a count rests on; it does not say the aggregate counts.

Equations

• cnt.ReadsCount = ∃ (g : ℕ → T), ∀ (L : List T), cnt L = g (List.countP (fun (x : T) => !ValueType.isNull x) L)

def SeqAggFunc.IsCount {T : Type} [ValueType T] (cnt : SeqAggFunc T) : Prop

An aggregate that is a count, SQL's count(e): its value is a function g of the number of non-null values it reads, never null, and zero exactly when that number is zero. It reads only that number (ReadsCount) and it counts matches (Counts).

Equations

• cnt.IsCount = ∃ (g : ℕ → T), (∀ (L : List T), cnt L = g (List.countP (fun (x : T) => !ValueType.isNull x) L)) ∧ (∀ (m : ℕ), ValueType.isNull (g m) = false) ∧ ∀ (m : ℕ), g m = 0 ↔ m = 0

def countVals {T : Type} [ValueType T] (g : ℕ → T) (m : ℕ) : Finset T

The values a count can take over a sequence of at most m values.

Equations

• countVals g m = Finset.image g (Finset.range (m + 1))

Helpers for where the values of a result lie

The set recursion

A set recursion's fixpoint has no bound in terms of its arguments': it iterates. What bounds it is its values – a duplicate-free relation of arity k over |V| values has at most |V|^k rows – and the rounds' values close on a set the instance fixes, which is what SQL's restriction on a recursive term buys. The body is read in the instance extended by the previous round, and the value analysis below (AggQueryIn.exists_polyBound_rec) reads it there, at every depth of recursion.

theorem card_le_pow_of_nodup_valsIn {T : Type} [ValueType T] {n : ℕ} {r : Multiset (Tuple T n)} {V : Finset T} (hnd : r.Nodup) (hv : Relation.valsIn r V) : r.card ≤ V.card ^ n

A duplicate-free relation over |V| values has at most |V|ⁿ rows.

The values the instance holds, as a set of polynomial size

The card of a set recursion's fixpoint is |V|ⁿ for the set V its rounds close on, so the invariant needs V built and not quantified over: a universally quantified set can be arbitrarily large, and a set asked to contain the counts over its own size cannot exist. The set is the instance's values at the arities the query reads, the query's constants, and the counts up to the bound – and it is the count bound that grows from one level of recursion to the next, which is what keeps the construction from circling.

def Tuple.valsL {T : Type} {k : ℕ} (u : Tuple T k) : List T

The values of a tuple.

Equations

• u.valsL = List.map u (List.finRange k)

def Relation.valsM {T : Type} {k : ℕ} (r : Multiset (Tuple T k)) : Multiset T

The values of a relation, as a bag.

Equations

• Relation.valsM r = r.bind fun (u : Tuple T k) => ↑u.valsL

def Database.instValsM {T : Type} (A : ℕ) : Database T → Multiset T

The values an instance holds in its relations of arity at most A.

Equations

• Database.instValsM A [] = 0
• Database.instValsM A ((fst, ⟨m, M⟩) :: tl) = (if m ≤ A then Relation.valsM M else 0) + Database.instValsM A tl

def Database.instVals {T : Type} [ValueType T] (A : ℕ) (D : Database T) : Finset T

And as a set.

Equations

• Database.instVals A D = (Database.instValsM A D).toFinset

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

The arities the query reads are at most A.

Equations

• AggQueryIn.aritiesLe A (AggQueryIn.Rel x✝ a) = (x✝ ≤ A)
• AggQueryIn.aritiesLe A (AggQueryIn.Hole x✝¹ s x✝) = (x✝¹ ≤ A)
• AggQueryIn.aritiesLe A (AggQueryIn.Param pv x✝) = True
• AggQueryIn.aritiesLe A AggQueryIn.Empty = True
• AggQueryIn.aritiesLe A (AggQueryIn.Proj ps q) = AggQueryIn.aritiesLe A q
• AggQueryIn.aritiesLe A (AggQueryIn.Sel φ q hφ) = AggQueryIn.aritiesLe A q
• AggQueryIn.aritiesLe A (q₁.Prod q₂) = (AggQueryIn.aritiesLe A q₁ ∧ AggQueryIn.aritiesLe A q₂)
• AggQueryIn.aritiesLe A (q₁.Apply q₂) = (AggQueryIn.aritiesLe A q₁ ∧ AggQueryIn.aritiesLe A q₂)
• AggQueryIn.aritiesLe A (q₁.Sum q₂) = (AggQueryIn.aritiesLe A q₁ ∧ AggQueryIn.aritiesLe A q₂)
• AggQueryIn.aritiesLe A q.Dedup = AggQueryIn.aritiesLe A q
• AggQueryIn.aritiesLe A (q₁.Diff q₂) = (AggQueryIn.aritiesLe A q₁ ∧ AggQueryIn.aritiesLe A q₂)
• AggQueryIn.aritiesLe A (AggQueryIn.Explode k a q) = AggQueryIn.aritiesLe A q
• AggQueryIn.aritiesLe A (AggQueryIn.Mu s a a_1) = (AggQueryIn.aritiesLe A a ∧ AggQueryIn.aritiesLe A a_1)
• AggQueryIn.aritiesLe A (AggQueryIn.MuSet s a a_1) = (AggQueryIn.aritiesLe A a ∧ AggQueryIn.aritiesLe A a_1)
• AggQueryIn.aritiesLe A (AggQueryIn.Gamma is ts fs q keep ord) = AggQueryIn.aritiesLe A q
• AggQueryIn.aritiesLe A (AggQueryIn.GammaScalar ts fs q ord) = AggQueryIn.aritiesLe A q
• AggQueryIn.aritiesLe A (AggQueryIn.GammaNest is his p f q) = AggQueryIn.aritiesLe A q
• AggQueryIn.aritiesLe A (AggQueryIn.ProvSum is his t q) = AggQueryIn.aritiesLe A q
• AggQueryIn.aritiesLe A (AggQueryIn.Retag h q) = AggQueryIn.aritiesLe A q
• AggQueryIn.aritiesLe A (AggQueryIn.GammaTok is his ts fs a q keep) = AggQueryIn.aritiesLe A q
• AggQueryIn.aritiesLe A (AggQueryIn.Win P O o w t f q a dist keep) = AggQueryIn.aritiesLe A q
• AggQueryIn.aritiesLe A (AggQueryIn.WinExpr P O o ws ts fs g q_1 keeps) = AggQueryIn.aritiesLe A q_1

The card and the values of a result, set recursions included

What pins the μ^⊎ row to μ^⊎ alone is that a query of the minimal signature without it – set recursions allowed – still has polynomially many rows. A set recursion's fixpoint has no bound in terms of its arguments' sizes, only in terms of its values: a duplicate-free relation of arity n over |V| values has at most |V|^n rows (card_le_pow_of_nodup_valsIn). So the card and the values have to be bounded together, by one induction that carries two statements: of a query, that its result's card is polynomial and its values lie in any set holding the instance's values (at the arities the query reads), the context's, the query's constants and the counts up to that polynomial; and of a recursive term, that its result read in the instance extended by a round has its values in any such set holding the round's values too. The second is what the first needs at a set recursion – the rounds then never leave the set – and the first is what the second needs for the sides of a term that do not read the recursive relation, which the restriction on recursive terms keeps the counts in: every count inside a recursive term is over a query the recursion does not feed, read off the instance the recursion started from (settlesAt_assign_of_noMention, evaluatePlain_assign_of_noMention).

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

The largest arity a query reads.

Equations

• (AggQueryIn.Rel x✝ a).maxArity = x✝
• (AggQueryIn.Hole x✝¹ s x✝).maxArity = x✝¹
• (AggQueryIn.Param pv x✝).maxArity = 0
• AggQueryIn.Empty.maxArity = 0
• (AggQueryIn.Proj ps q).maxArity = q.maxArity
• (AggQueryIn.Sel φ q hφ).maxArity = q.maxArity
• (q₁.Prod q₂).maxArity = max q₁.maxArity q₂.maxArity
• (q₁.Apply q₂).maxArity = max q₁.maxArity q₂.maxArity
• (q₁.Sum q₂).maxArity = max q₁.maxArity q₂.maxArity
• q.Dedup.maxArity = q.maxArity
• (q₁.Diff q₂).maxArity = max q₁.maxArity q₂.maxArity
• (AggQueryIn.Explode k a q).maxArity = q.maxArity
• (AggQueryIn.Mu s a a_1).maxArity = max a.maxArity a_1.maxArity
• (AggQueryIn.MuSet s a a_1).maxArity = max a.maxArity a_1.maxArity
• (AggQueryIn.Gamma is ts fs q keep ord).maxArity = q.maxArity
• (AggQueryIn.GammaScalar ts fs q ord).maxArity = q.maxArity
• (AggQueryIn.GammaNest is his p f q).maxArity = q.maxArity
• (AggQueryIn.ProvSum is his t q).maxArity = q.maxArity
• (AggQueryIn.Retag h q).maxArity = q.maxArity
• (AggQueryIn.GammaTok is his ts fs a q keep).maxArity = q.maxArity
• (AggQueryIn.Win P O o w t f q a dist keep).maxArity = q.maxArity
• (AggQueryIn.WinExpr P O o ws ts fs g q_1 keeps).maxArity = q_1.maxArity

theorem AggQueryIn.exists_polyBound_rec {T : Type} [ValueType T] {S : Set OpKind} (hmb : OpKind.muBag ∉ S) {cnt : SeqAggFunc T} (hcnt : cnt.ReadsCount) {c n : ℕ} {κ : Fin n → ColKind} {l : List (String × ℕ)} (q : AggQueryIn T c n κ l) (hq : usesOnly S q) (hr : q.hygienic) (hsig : inSig {cnt} q) : ∃ (b : ℕ) (k : ℕ), ∀ (D : Database T) (γ : Fin c → T), q.SettlesAt D γ → Multiset.card (q.evaluatePlain D γ) ≤ b * (D.size + 1) ^ k

Without μ^⊎, a query of the minimal signature has polynomially many rows wherever it is defined, set recursions included.

The row: a basis of the whole algebra holds a recursion

The recursions are classes like the others. The witness is the chain of diamonds: a class set holding neither recursion generates only queries whose answers are polynomial in the instance (AggQueryIn.exists_polyBound), and the sink of the chain has 2ⁿ rows.

The recursion-free rows of Provenance.BasisAssembly carry no hypothesis on the recursions: each holds of every class set, those holding a recursion included.

def plainRecOps : Set OpKind

The scope of the classification with the recursions.

Equations

• plainRecOps = insert OpKind.muBag (insert OpKind.muSet plainOps)

def GeneratesAt (T : Type) [ValueType T] (sch : Schema) (cnt : SeqAggFunc T) (S : Set OpKind) {n : ℕ} {κ : Fin n → ColKind} (q : AggQuery T n κ) : Prop

A generating set of the whole algebra, over a schema, in the minimal universe 𝒜(∅, {count}), where the classification with the recursions is stated: every query of the algebra over sch in the minimal signature is matched by one in the minimal signature using only the classes of S, which is defined wherever the query is and agrees with it there (AggQueryIn.SettlesAt). A query of the whole algebra is a partial function of the instance, so this is what equivalence means for it; nothing is asked where the query is undefined. The counting aggregate cnt is a parameter with SeqAggFunc.ReadsCount as its specification where a row needs it, as everywhere in the classification.

Equations

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

def GeneratesOnRec (T : Type) [ValueType T] (sch : Schema) (cnt : SeqAggFunc T) (S : Set OpKind) : Prop

The generation of every query of the algebra: GeneratesAt at each.

Equations

• GeneratesOnRec T sch cnt S = ∀ {n : ℕ} {κ : Fin n → ColKind} (q : AggQuery T n κ), GeneratesAt T sch cnt S q

theorem GeneratesOnRec.mono {T : Type} [ValueType T] {sch : Schema} {cnt : SeqAggFunc T} {S S' : Set OpKind} (hSS : S ⊆ S') (h : GeneratesOnRec T sch cnt S) : GeneratesOnRec T sch cnt S'

A set of classes generating the whole algebra does so with any class added.

The rows of the classification for the whole algebra

Each row below is the statement that a class is in every basis of the whole algebra in the minimal universe. The witnesses are the plain fragment's (Provenance.BasisAssembly), every one of them in the minimal signature and recursion-free, hence restricted and defined everywhere; the invariants are the ones of Provenance.PlainBasis extended through the recursions. What is not here is ⊎: its thin-instance invariant fails with a recursion (μ^⊎R.(S, Π_c(σ_{#1≠c}(R))) over {a} has the rows a and c), and the class is indeed not necessary – with a bag recursion the union is a derived operator (Provenance.SumByMu).

The rows against the generation of every query

theorem muBag_mem_of_generatesOnRec {cnt : SeqAggFunc ℕ} (hcnt : cnt.ReadsCount) {S : Set OpKind} (hS : GeneratesOnRec ℕ schemaSE cnt S) : OpKind.muBag ∈ S

μ^⊎ is in every basis of the whole algebra.

Home · Documentation · Publications · Contributors · Source · Cite