The rounds of a bag recursion that settles are bounded

A recursive term reads its hole once, so it is linear in the recursive relation: a round of a bag recursion is the previous round bound through a function of the row (AggQueryIn.bind_of_body). A row of round j is therefore the end of a path of j steps from the base, and a path longer than the number of rows the rounds can hold repeats a row, whose segment then pumps forever: a recursion that settles does so within |V|^m rounds, V the values its rounds hold (bindStep_round_eq_zero_of_settles), and its value is the sum of that many rounds (AggQueryIn.mu_eq_muSum_of_valsIn).

This is what any bounded simulation of a bag recursion rests on – a simulation that settles everywhere and agrees with the recursion wherever the recursion settles.

A body is linear in its hole

theorem AggQueryIn.bind_of_body {T : Type} [ValueType T] {s : String} {m c n : ℕ} {κ : Fin n → ColKind} {l : List (String × ℕ)} (q : AggQueryIn T c n κ l) : l = [(s, m)] → noMention s q → ∀ (D : Database T) (γ : Fin c → T), ∃ (F : Tuple T m → Multiset (Tuple T n)) (C : Multiset (Tuple T n)), ∀ (X : Multiset (Tuple T m)), q.evaluatePlain (Database.assign s X D) γ = X.bind F + C

A recursive term is linear in its hole: read at a round X, it is X bound through a function of the row, plus what it reads at the empty round. The hole occurs once, under projections, selections, products, the left of an apply and unions, each of which distributes over the bind.

Paths through the rounds of a bind

def bindStep {α : Type} (F : α → Multiset α) : Multiset α → Multiset α

The round function of a linear term with nothing read at the empty round: a round is the previous one bound through F.

Equations

• bindStep F X = X.bind F

theorem exists_path_of_mem_round {α : Type} (F : α → Multiset α) (M : Multiset α) (j : ℕ) (t : α) : t ∈ (bindStep F)^[j] M → ∃ (p : ℕ → α), p 0 ∈ M ∧ (∀ i < j, p (i + 1) ∈ F (p i)) ∧ p j = t

A row of round j is the end of a path of j steps from the base.

theorem mem_round_pump {α : Type} (F : α → Multiset α) (M : Multiset α) (p : ℕ → α) {a b : ℕ} (hab : a < b) (hp : ∀ i < b, p (i + 1) ∈ F (p i)) (hrep : p a = p b) (hb : p b ∈ (bindStep F)^[b] M) (k : ℕ) : p b ∈ (bindStep F)^[b + k * (b - a)] M

A repeated row pumps: if a path visits the same row at a < b, that row is in round b + k (b - a) for every k.

The bound

theorem bindStep_round_eq_zero_of_settles {T : Type} [ValueType T] {m : ℕ} (F : Tuple T m → Multiset (Tuple T m)) (M : Multiset (Tuple T m)) (V : Finset T) (hV : ∀ (j : ℕ), ∀ u ∈ (bindStep F)^[j] M, ∀ (i : Fin m), u i ∈ V) (hs : MuSettles (bindStep F) M) : (bindStep F)^[V.card ^ m] M = 0

A bag recursion that settles does so within |V|^m rounds, V holding every value of every round: a row of round |V|^m ends a path of |V|^m + 1 rows over V^m, two of which coincide, and the segment between them pumps a non-empty round past every bound.

theorem AggQueryIn.mu_eq_muSum_of_valsIn {T : Type} [ValueType T] {c m : ℕ} (s : String) (q₀ : AggQueryIn T c m (ColKind.allReg m)) (q₁ : AggQueryIn T c m (ColKind.allReg m) [(s, m)]) (hr : noMention s q₁) (D : Database T) (γ : Fin c → T) (V : Finset T) (h0 : q₁.evaluatePlain (Database.assign s 0 D) γ = 0) (hs : MuSettles (fun (X : Multiset (Tuple T m)) => q₁.evaluatePlain (Database.assign s X D) γ) (q₀.evaluatePlain D γ)) (hV : ∀ (j : ℕ) (u : Tuple T m), ((fun (X : Multiset (Tuple T m)) => q₁.evaluatePlain (Database.assign s X D) γ)^[j] (q₀.evaluatePlain D γ)).Mem u → ∀ (i : Fin m), u i ∈ V) : (Mu s q₀ q₁).evaluatePlain D γ = muSum (fun (X : Multiset (Tuple T m)) => q₁.evaluatePlain (Database.assign s X D) γ) (V.card ^ m) (q₀.evaluatePlain D γ)

A bag recursion that settles is the sum of |V|^m rounds, V holding every value of every round: the round function of a body that reads nothing at the empty round is a bind (AggQueryIn.bind_of_body), so the bound applies.

Home · Documentation · Publications · Contributors · Source · Cite