Windows are needed in every basis of the whole algebra

win is in every basis of the whole algebra in the minimal universe. The witness is count(*) OVER (… EXCLUDE CURRENT ROW) on a unary relation holding n copies of one value, which writes n − 1 on every row. A window-free query of the minimal universe writes, on that family of instances and for n large, only values p(n) for finitely many polynomials p with natural coefficients, which n − 1 is not.

The polynomials are Mathlib's Polynomial ℕ; what the invariant needs of them is that two of them are eventually equal, or eventually strictly ordered one way, which is read off their real asymptotics.

def WinRow.dRep (n : ℕ) : Database ℕ

The instance holding n copies of the row (1) in R.

Equations

• WinRow.dRep n = [("R", ⟨1, Multiset.replicate n ![1]⟩)]

def WinRow.wholeExcludeSelf : ValueFrame ℕ 0

The whole partition less the current row: ROWS BETWEEN UNBOUNDED PRECEDING AND UNBOUNDED FOLLOWING EXCLUDE CURRENT ROW.

Equations

• WinRow.wholeExcludeSelf = { cond := FrameCond.whole, self := false }

def WinRow.winWitness : AggQuery ℕ (1 + 1) (Fin.snoc (ColKind.allReg 1) ColKind.agg)

The witness: count(#1) OVER (EXCLUDE CURRENT ROW) on R.

Equations

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

Eventual comparison of polynomials with natural coefficients

@[reducible, inline]

abbrev WinRow.Poly : Type

A polynomial with natural coefficients, read as a function of n.

Equations

• WinRow.Poly = Polynomial ℕ

inductive WinRow.Poly.Cmp (p q : Poly) (N : ℕ) : Prop

How two polynomials compare from some point on.

• lt {p q : Poly} {N : ℕ} (h : ∀ n ≥ N, Polynomial.eval n p < Polynomial.eval n q) : p.Cmp q N
• eq {p q : Poly} {N : ℕ} (h : ∀ n ≥ N, Polynomial.eval n p = Polynomial.eval n q) : p.Cmp q N
• gt {p q : Poly} {N : ℕ} (h : ∀ n ≥ N, Polynomial.eval n q < Polynomial.eval n p) : p.Cmp q N

def WinRow.Decided (V : Set Poly) (N : ℕ) : Prop

Every pair of a finite set of polynomials is decided from N on.

Equations

• WinRow.Decided V N = ∀ p ∈ V, ∀ q ∈ V, p.Cmp q N

Polynomial bags

A relation computed on the instance with n copies is, for n large, a bag of finitely many shapes: a row of polynomials, each repeated a polynomial number of times.

structure WinRow.Shape (k : ℕ) : Type

A shape: a row of polynomials with a polynomial multiplicity.

• mult : Poly
• row : Fin k → Poly

def WinRow.Shape.rowAt {k : ℕ} (s : Shape k) (n : ℕ) : Tuple ℕ k

The row of a shape at n.

Equations

• s.rowAt n j = Polynomial.eval n (s.row j)

def WinRow.Shape.inst {k : ℕ} (s : Shape k) (n : ℕ) : Multiset (Tuple ℕ k)

The copies of a shape at n.

Equations

• s.inst n = Multiset.replicate (Polynomial.eval n s.mult) (s.rowAt n)

@[reducible, inline]

abbrev WinRow.PolyBag (k : ℕ) : Type

A bag of shapes.

Equations

• WinRow.PolyBag k = List (WinRow.Shape k)

def WinRow.PolyBag.inst {k : ℕ} (L : PolyBag k) (n : ℕ) : Multiset (Tuple ℕ k)

The relation a bag of shapes stands for at n.

Equations

• L.inst n = (List.map (fun (s : WinRow.Shape k) => s.inst n) L).sum

def WinRow.PolyBag.vals {k : ℕ} (L : PolyBag k) : Set Poly

The polynomials the rows of a bag hold.

Equations

• L.vals = {p : WinRow.Poly | ∃ s ∈ L, ∃ (j : Fin k), s.row j = p}

def WinRow.PolyBag.mults {k : ℕ} (L : PolyBag k) : Set Poly

The multiplicities of a bag.

Equations

• L.mults = {p : WinRow.Poly | ∃ s ∈ L, s.mult = p}

noncomputable def WinRow.PolyBag.scale {k : ℕ} (m : Poly) (L : PolyBag k) : PolyBag k

Scaling every multiplicity.

Equations

• WinRow.PolyBag.scale m L = List.map (fun (s : WinRow.Shape k) => { mult := m * s.mult, row := s.row }) L

def WinRow.PolyBag.mapRows {k k' : ℕ} (f : (Fin k → Poly) → Fin k' → Poly) (L : PolyBag k) : PolyBag k'

Mapping the rows.

Equations

• WinRow.PolyBag.mapRows f L = List.map (fun (s : WinRow.Shape k) => { mult := s.mult, row := f s.row }) L

noncomputable def WinRow.PolyBag.bindShapes {k₁ k₂ : ℕ} (L₁ : PolyBag k₁) (F : Shape k₁ → PolyBag k₂) : PolyBag (k₁ + k₂)

A bag of shapes under each shape, as an apply reads its right side.

Equations

• L₁.bindShapes F = List.flatMap (fun (s : WinRow.Shape k₁) => List.map (fun (t : WinRow.Shape k₂) => { mult := s.mult * t.mult, row := Fin.append s.row t.row }) (F s)) L₁

Symbolic terms, and the shift from the threshold

A function-free term over a row of polynomials is a polynomial. A predicate over decided polynomials reads alike at the threshold and at every larger n, because the values at n are the image of the values at the threshold under a faithful map (Provenance.Genericity).

def WinRow.ctxAt {c : ℕ} (cγ : Fin c → Poly) (n : ℕ) : Fin c → ℕ

A context of polynomials at n.

Equations

• WinRow.ctxAt cγ n j = Polynomial.eval n (cγ j)

def WinRow.Cset (A : Finset ℕ) : Set Poly

The constants of a query as polynomials.

Equations

• WinRow.Cset A = (fun (a : ℕ) => Polynomial.C a) '' ↑A

noncomputable def WinRow.TermIn.polyOf {c k : ℕ} (t : TermIn ℕ c k) (row : Fin k → Poly) (cγ : Fin c → Poly) : Poly

The polynomial a function-free term reads as.

Equations

• WinRow.TermIn.polyOf (TermIn.const a) row cγ = Polynomial.C a
• WinRow.TermIn.polyOf (TermIn.outer j) row cγ = cγ j
• WinRow.TermIn.polyOf (#j) row cγ = row j
• WinRow.TermIn.polyOf t row cγ = 0

noncomputable def WinRow.TermGIn.polyOf {c k : ℕ} {κ : Fin k → ColKind} (t : TermGIn ℕ c κ) (row : Fin k → Poly) (cγ : Fin c → Poly) : Poly

The polynomial a function-free term of the general syntax reads as.

Equations

• WinRow.TermGIn.polyOf (TermGIn.const a) row cγ = Polynomial.C a
• WinRow.TermGIn.polyOf (TermGIn.outer j) row cγ = cγ j
• WinRow.TermGIn.polyOf (TermGIn.index j a) row cγ = row j
• WinRow.TermGIn.polyOf (TermGIn.provIndex j a) row cγ = row j
• WinRow.TermGIn.polyOf t row cγ = 0

noncomputable def WinRow.ProjColIn.polyOf {c k : ℕ} {κ : Fin k → ColKind} (p : ProjColIn ℕ c κ) (row : Fin k → Poly) (cγ : Fin c → Poly) : Poly

The polynomial a function-free projection column reads as.

Equations

• WinRow.ProjColIn.polyOf (ProjColIn.term t) row cγ = WinRow.TermGIn.polyOf t row cγ
• WinRow.ProjColIn.polyOf (ProjColIn.token j a) row cγ = row j
• WinRow.ProjColIn.polyOf (ProjColIn.aggTerm k_1 a a_1) row cγ = 0
• WinRow.ProjColIn.polyOf (ProjColIn.aggTermOf j a t) row cγ = WinRow.TermIn.polyOf t (fun (i : Fin 0) => i.elim0) fun (x : Fin 1) => row j
• WinRow.ProjColIn.polyOf (ProjColIn.provTerm t) row cγ = WinRow.TermGIn.polyOf t row cγ

The count polynomials of a query

A polynomial is a count polynomial of a query if, for n large, its value is one of the counts the query computes on the instance with n copies (AggQueryIn.countValsAll, over every context). There are finitely many, because the counts a query computes on that instance are at most a constant in number (AggQueryIn.exists_polyBound_countTypes over a base set of constant size).

def WinRow.CountPolys {c k : ℕ} {κ : Fin k → ColKind} {l : List (String × ℕ)} (q : AggQueryIn ℕ c k κ l) : Set Poly

The count polynomials of a closed query.

Equations

• WinRow.CountPolys q = {p : WinRow.Poly | ∃ (N : ℕ), ∀ n ≥ N, Polynomial.eval n p ∈ q.countValsAll (WinRow.dRep n)}

def WinRow.CountPolysHole {c k : ℕ} {κ : Fin k → ColKind} {l : List (String × ℕ)} (q : AggQueryIn ℕ c k κ l) (s : String) (m : ℕ) : Set Poly

The count polynomials of a term with a hole, over every binding of it.

Equations

• WinRow.CountPolysHole q s m = {p : WinRow.Poly | ∃ (N : ℕ), ∀ n ≥ N, ∃ (X : Relation ℕ m), Polynomial.eval n p ∈ q.countValsAll (Database.assign s X (WinRow.dRep n))}

def WinRow.baseSet (A : Finset ℕ) : Finset ℕ

The base set of the instance family: the instance's value, the zero, and the query's constants.

Equations

• WinRow.baseSet A = insert 0 (insert 1 A)

The invariant's vocabulary

def WinRow.Univ {c k : ℕ} {κ : Fin k → ColKind} {l : List (String × ℕ)} (q : AggQueryIn ℕ c k κ l) (cγ : Fin c → Poly) : Set Poly

The values a closed query may write at a context of polynomials: its constants, the instance's value, the context, and its counts.

Equations

• WinRow.Univ q cγ = WinRow.Cset q.allConsts ∪ {1} ∪ Set.range cγ ∪ WinRow.CountPolys q

def WinRow.UnivHole {c k : ℕ} {κ : Fin k → ColKind} {l : List (String × ℕ)} (q : AggQueryIn ℕ c k κ l) (s : String) (m : ℕ) (cγ : Fin c → Poly) : Set Poly

The same for a term with a hole, its counts taken over every binding.

Equations

• WinRow.UnivHole q s m cγ = WinRow.Cset q.allConsts ∪ {1} ∪ Set.range cγ ∪ WinRow.CountPolysHole q s m

def WinRow.ClosedSym {c k : ℕ} {κ : Fin k → ColKind} {l : List (String × ℕ)} (q : AggQueryIn ℕ c k κ l) (cγ : Fin c → Poly) : Prop

The invariant for a closed query: for n large its result on the instance with n copies is a bag of shapes, with values in Univ, and whether it settles there does not depend on n.

Equations

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

def WinRow.BodySym {c k : ℕ} {κ : Fin k → ColKind} {l : List (String × ℕ)} (q : AggQueryIn ℕ c k κ l) (s : String) (m : ℕ) (cγ : Fin c → Poly) (W : Set Poly) : Prop

The invariant for a term with a hole: uniformly in the bag the hole is bound to, provided its values lie in a given finite set.

Equations

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

Bag lemmas the cases need

def WinRow.PolyBag.allZero {k : ℕ} (L : PolyBag k) : Prop

Every multiplicity is the zero polynomial: the bag is empty at every n ≥ 1.

Equations

• L.allZero = ∀ s ∈ L, s.mult = 0

def WinRow.dedupAt {k : ℕ} (N : ℕ) : PolyBag k → PolyBag k

Duplicate elimination at the threshold: one copy of each row the shapes of non-zero multiplicity have at N, the last of them kept.

Equations

• WinRow.dedupAt N [] = []
• WinRow.dedupAt N (s :: L) = if s.mult = 0 ∨ ∃ t ∈ L, t.mult ≠ 0 ∧ t.rowAt N = s.rowAt N then WinRow.dedupAt N L else { mult := 1, row := s.row } :: WinRow.dedupAt N L

Universe bookkeeping

Counting the rows of a bag

The invariant

The row

theorem win_mem_of_generatesOnRec {S : Set OpKind} (hS : GeneratesOnRec ℕ schemaR SeqAggFunc.count S) : OpKind.win ∈ S

Windows are needed: win is in every basis of the whole algebra over ℕ with the counting aggregate.

Home · Documentation · Publications · Contributors · Source · Cite