The symbolic evaluation settles on every instance #
A query's table is evaluated at every type of parameter row, including
types no actual row has, where the query itself may not settle. So the
table must settle on every instance, whatever its input: it does, its
recursions being bounded by counters (Sym.settlesAt_symMuQ), and so
does everything the environment and the cut are built of
(Sym.settlesAt_tabQ).
theorem
Sym.settlesAt_symMuQ
{T : Type}
[ValueType T]
{c N K : ℕ}
(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)))
(hS : AggQueryIn.noMention s Sq)
(D : Database T)
(γ : Fin c → T)
(hQ₀ : Q₀.SettlesAt D γ)
(hL : Lq.SettlesAt D γ)
(hSs : Sq.SettlesAt D γ)
(hB : ∀ (Y : Relation T (N + K)), Bq.SettlesAt (Database.assign s Y D) γ)
(hpres :
∀ (Y : Multiset (Tuple T (N + K))) (y : Tuple T (N + 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)
(hLv : Lq.evaluatePlain D γ = {cs[0]})
(hSv : Sq.evaluatePlain D γ = succRel cs)
:
A bounded recursion settles, whatever its body computes, as long as its body settles at every round and keeps each row's counter.
Dependency graph
The symbolic evaluation settles #
What the symbolic evaluation asks of its environment to settle: its queries settle, and the counters are a list without repetition.
Instances For
Dependency graph
The environment built from a cut settles #
The cut settles #
theorem
Sym.settlesAt_tabQ
{T : Type}
[ValueType T]
{k c : ℕ}
{cnt : SeqAggFunc T}
(hc : cnt.Counts)
(f : ℕ → String)
{n : ℕ}
{κ : Fin n → ColKind}
(q : AggQueryIn T (k + c) n κ)
(hf : ∀ (i : ℕ), AggQueryIn.noMention (f i) q)
(D : Database T)
(γ : Fin c → T)
:
The table settles on every instance.