What the apply written with products is made of #
The construction of Provenance.SymApply must stay in the fragment it is
for: its operators in {∅, Π, σ, ×, γ, win, μ^⊎} (Sym.basisProdOps),
its terms and aggregates in the signature, its recursions hygienic, and
every window over an all-regular input. Sym.Fine bundles the four, and
each construction is shown to keep it.
def
Sym.Fine
{T : Type}
[ValueType T]
{c n : ℕ}
{κ : Fin n → ColKind}
{l : List (String × ℕ)}
(Θ : Set (SeqAggFunc T))
(q : AggQueryIn T c n κ l)
:
A query of the fragment the construction lives in.
Equations
- Sym.Fine Θ q = (AggQueryIn.usesOnly Sym.basisProdOps q ∧ AggQueryIn.inSig Θ q ∧ Sym.winAllReg q ∧ q.hygienic)
Instances For
Dependency graph
Terms and predicates of comparisons #
The primitive constructions #
The order queries and the environment #
structure
Sym.EnvFine
{T : Type}
[ValueType T]
{c k : ℕ}
(Θ : Set (SeqAggFunc T))
(env : SymEnv T k c)
:
The environment's queries are of the fragment.
Instances For
Dependency graph
The symbolic evaluation #
The cut #
The table and the apply #
theorem
Sym.fine_applyX
{T : Type}
[ValueType T]
{c k : ℕ}
{Θ : Set (SeqAggFunc T)}
{cnt : SeqAggFunc T}
(hc : cnt ∈ Θ)
(f : ℕ → String)
{n₂ : ℕ}
{l : List (String × ℕ)}
{κ₂ : Fin n₂ → ColKind}
{L : AggQueryIn T c k (ColKind.allReg k) l}
{R : AggQueryIn T (k + c) n₂ κ₂}
{VQ : AggQueryIn T c 1 (ColKind.allReg 1)}
(hL : Fine Θ L)
(hR : AggQueryIn.inSig Θ R)
(hV : Fine Θ VQ)
(hfR : ∀ (i : ℕ), AggQueryIn.noMention (f i) R)
(hfV : AggQueryIn.noMention (part f 1 0) VQ ∧ AggQueryIn.noMention (part f 1 1) VQ)
:
The apply written with products is of the fragment.