A bag recursion run against a counter

The table a body apply is tabulated by evaluates the right side at every type of the parameter row, those no row of the recursive relation ever has included, and a bag recursion inside the right side may run forever there. Inside the table, every bag recursion is therefore bounded: its rounds carry a counter, the base the least of a list of counters, and each round moves the counter to its successor, so that the recursion stops after as many rounds as there are counters, on every instance. As long as the original recursion settles within that many rounds – which a restricted recursion over a bounded set of values does (AggQueryIn.mu_eq_muSum_of_valsIn) – the bounded one computes the same rows, the counter projected away.

The bounded recursion is Sym.symMuQ; every row of a round carries that round's counter and the recursion stops after the last one (Sym.simStep_suf, Sym.simStep_last), and over symbolic rows its slice under a descriptor is the encoding of the recursion's rows (Sym.sliceIs_symMu).

def Sym.pre {T : Type} {N K : ℕ} (x : Tuple T (N + K)) : Tuple T N

The first block of a row.

Equations

• Sym.pre x i = x (Fin.castAdd K i)

def Sym.suf {T : Type} {N K : ℕ} (x : Tuple T (N + K)) : Tuple T K

The second block of a row.

Equations

• Sym.suf x i = x (Fin.natAdd N i)

def Sym.succRel {T : Type} {K : ℕ} (cs : List (Tuple T K)) : Multiset (Tuple T (K + K))

The successor relation of a list of counters: each counter with the next.

Equations

• Sym.succRel cs = ↑(List.map (fun (ab : Tuple T K × Tuple T K) => Fin.append ab.1 ab.2) (cs.zip cs.tail))

def Sym.simStep {T : Type} [ValueType T] {N K : ℕ} (B : Multiset (Tuple T (N + K)) → Multiset (Tuple T (N + K))) (S : Multiset (Tuple T (K + K))) (Z : Multiset (Tuple T (N + K))) : Multiset (Tuple T (N + K))

A round of the bounded recursion: the round function on the rows, each output row moved to the successor of its counter.

Equations

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

The bounded recursion as a query

theorem Sym.appendKinds (a b : ℕ) : Fin.append (ColKind.allReg a) (ColKind.allReg b) = ColKind.allReg (a + b)

def Sym.prodR {T : Type} {c : ℕ} {l₁ l₂ : List (String × ℕ)} {a b : ℕ} (q₁ : AggQueryIn T c a (ColKind.allReg a) l₁) (q₂ : AggQueryIn T c b (ColKind.allReg b) l₂) : AggQueryIn T c (a + b) (ColKind.allReg (a + b)) (l₁ ++ l₂)

The product of two all-regular queries, all-regular.

Equations

• Sym.prodR q₁ q₂ = AggQueryIn.castKind ⋯ (q₁.Prod q₂)

def Sym.ctrEqSP {T : Type} {N K c : ℕ} : SP T c (N + K + (K + K))

The counters of a round and of the successor agree.

Equations

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

def Sym.stepCols {T : Type} {N K c : ℕ} : Fin (N + K) → SA T c (N + K + (K + K))

The columns a bounded round keeps: the row's, and the successor's counter.

Equations

• Sym.stepCols i = Fin.addCases (fun (i : Fin N) => Sym.SA.col (Fin.castAdd (K + K) (Fin.castAdd K i))) (fun (z : Fin K) => Sym.SA.col (Fin.natAdd (N + K) (Fin.natAdd K z))) i

def Sym.stepQ {T : Type} [ValueType T] {N K c : ℕ} (s : String) (Bq : AggQueryIn T c (N + K) (ColKind.allReg (N + K)) [(s, N + K)]) (Sq : AggQueryIn T c (K + K) (ColKind.allReg (K + K))) : AggQueryIn T c (N + K) (ColKind.allReg (N + K)) [(s, N + K)]

A round of the bounded recursion, as a query: the body's rows whose counter has a successor, moved to it.

Equations

• Sym.stepQ s Bq Sq = AggQueryIn.castKind ⋯ (AggQueryIn.Proj (Sym.projSA Sym.stepCols) (AggQueryIn.Sel Sym.ctrEqSP.toGen (Sym.prodR Bq Sq) ⋯))

def Sym.symMuQ {T : Type} [ValueType T] {N K c : ℕ} (s : String) (Q₀ : AggQueryIn T c N (ColKind.allReg N)) (Bq : AggQueryIn T c (N + K) (ColKind.allReg (N + K)) [(s, N + K)]) (Lq : AggQueryIn T c K (ColKind.allReg K)) (Sq : AggQueryIn T c (K + K) (ColKind.allReg (K + K))) : AggQueryIn T c N (ColKind.allReg N)

The bounded recursion: the base paired with the least counter, each round moved to the next counter, the counter projected away.

Equations

• Sym.symMuQ s Q₀ Bq Lq Sq = AggQueryIn.castKind ⋯ (AggQueryIn.Proj (Sym.projSA fun (i : Fin N) => Sym.SA.col (Fin.castAdd K i)) (AggQueryIn.Mu s (Sym.prodR Q₀ Lq) (Sym.stepQ s Bq Sq)))

The rounds of the bounded recursion, round by round

theorem Sym.simStep_suf {T : Type} [ValueType T] {N K : ℕ} (B : Multiset (Tuple T (N + K)) → Multiset (Tuple T (N + K))) (hpres : ∀ (Y : Multiset (Tuple T (N + K))), ∀ y ∈ B Y, ∃ x ∈ Y, suf x = suf y) (cs : List (Tuple T K)) (hnd : cs.Nodup) (Z₀ : Multiset (Tuple T (N + K))) (hne : 0 < cs.length) (h₀ : ∀ z ∈ Z₀, suf z = cs[0]) (j : ℕ) (z : Tuple T (N + K)) : z ∈ (simStep B (succRel cs))^[j] Z₀ → ∃ (h : j < cs.length), suf z = cs[j]

Every row of a round carries that round's counter, and there are no rows past the last counter, as long as the round function keeps each row's counter.

theorem Sym.simStep_last {T : Type} [ValueType T] {N K : ℕ} (B : Multiset (Tuple T (N + K)) → Multiset (Tuple T (N + K))) (hpres : ∀ (Y : Multiset (Tuple T (N + K))), ∀ y ∈ B Y, ∃ x ∈ Y, suf x = suf y) (cs : List (Tuple T K)) (hnd : cs.Nodup) (Z₀ : Multiset (Tuple T (N + K))) (hne : 0 < cs.length) (h₀ : ∀ z ∈ Z₀, suf z = cs[0]) : (simStep B (succRel cs))^[cs.length] Z₀ = 0

The bounded recursion stops after the last counter.

The symbolic bounded recursion's slices

theorem Sym.sliceIs_symMu {T : Type} [ValueType T] {k c n : ℕ} {C : Finset T} {par : Fin k → T} {K' : ℕ} (s : String) (Q₀ : AggQueryIn T c ((k + n) * (7 + k)) (ColKind.allReg ((k + n) * (7 + k)))) (Bq : AggQueryIn T c ((k + n) * (7 + k) + K') (ColKind.allReg ((k + n) * (7 + k) + K')) [(s, (k + n) * (7 + k) + K')]) (Lq : AggQueryIn T c K' (ColKind.allReg K')) (Sq : AggQueryIn T c (K' + K') (ColKind.allReg (K' + K'))) (hS : AggQueryIn.noMention s Sq) (D : Database T) (γ : Fin c → T) (step : Multiset (Tuple T n) → Multiset (Tuple T n)) (X₀ : Multiset (Tuple T n)) (hQ₀ : SliceIs C par (Q₀.evaluatePlain D γ) (Multiset.map (fun (v : Tuple T n) => (v, Fin.elim0)) X₀)) (hpres : ∀ (Y : Multiset (Tuple T ((k + n) * (7 + k) + K'))) (y : Tuple T ((k + n) * (7 + k) + K')), Multiset.Mem (Bq.evaluatePlain (Database.assign s Y D) γ) y → ∃ x ∈ Y, suf x = suf y) (cs : List (Tuple T K')) (hnd : cs.Nodup) (hne : 0 < cs.length) (hbody : ∀ (j : ℕ), j + 1 < cs.length → ∀ (Y : Multiset (Tuple T ((k + n) * (7 + k) + K'))) (e : Tuple T K'), SliceIs C par Y (Multiset.map (fun (v : Tuple T n) => (v, e)) (step^[j] X₀)) → SliceIs C par (Bq.evaluatePlain (Database.assign s Y D) γ) (Multiset.map (fun (v : Tuple T n) => (v, e)) (step (step^[j] X₀)))) (hLv : Lq.evaluatePlain D γ = {cs[0]}) (hSv : Sq.evaluatePlain D γ = succRel cs) (h0 : step 0 = 0) (hset : step^[cs.length] X₀ = 0) : SliceIs C par ((symMuQ s Q₀ Bq Lq Sq).evaluatePlain D γ) (Multiset.map (fun (v : Tuple T n) => (v, Fin.elim0)) (muSumFix step X₀))

The symbolic bounded recursion's slice: the encodings of the recursion's rows, wherever the recursion settles within as many rounds as there are counters and its rounds hold good values.

Home · Documentation · Publications · Contributors · Source · Cite