Documentation

Provenance.SymCorrect

The symbolic evaluation is correct #

Under the descriptor of a parameter row, the symbolic evaluation of a query holds the encodings of the rows the query computes at that row (Sym.sym_correct), provided the environment is sound (Sym.EnvOK: the descriptors without repetition and every parameter row's among them, and enough counters for every bag recursion) and every value the evaluation compares or groups is good (Sym.Good): a value of the cut, the null, or a component of the parameter row. What makes the second hold is the cut, a separate matter.

What the evaluation asks of the query and of the values #

source
def Sym.winAllReg {T : Type} {c n : ℕ} {κ : Fin n → ColKind} {l : List (String × ℕ)} :
AggQueryIn T c n κ l → Prop

Every window reads an all-regular input, which is what the windows the passes build do.

Equations
Instances For
    Dependency graph
    source
    def Sym.Good {T : Type} [ValueType T] (G : T → Prop) {c n : ℕ} {κ : Fin n → ColKind} {l : List (String × ℕ)} :
    AggQueryIn T c n κ l → Database T → (Fin c → T) → Prop

    Every value the evaluation of a query compares, groups or emits from nowhere is a value of the cut (CG): the values of the relations it reads, the constants, the values its aggregations compute; and under a recursion, at every round.

    Equations
    Instances For
      Dependency graph
      source
      noncomputable def Sym.cutAt {T : Type} [ValueType T] {k c : ℕ} (env : SymEnv T k c) (D : Database T) (γ : Fin c → T) :
      Finset T

      The cut at an instance, as a finite set of values.

      Equations
      Instances For
        Dependency graph
        source
        def Sym.EnvOK {T : Type} [ValueType T] {k c : ℕ} (env : SymEnv T k c) (D : Database T) (γ : Fin c → T) :
        Prop

        The environment is sound at an instance: the descriptors are listed once each and hold every parameter row's, and every arity of a bag recursion has a list of counters long enough for the rounds it can run.

        Equations
        • One or more equations did not get rendered due to their size.
        Instances For
          Dependency graph

          The relations the symbolic evaluation names #

          source
          def Sym.EnvNoMention {T : Type} [ValueType T] {k c : ℕ} (env : SymEnv T k c) (s : String) :
          Prop

          The environment names no relation s.

          Equations
          Instances For
            Dependency graph

            A symbolic recursive term keeps each row's further columns #

            The correctness of the symbolic evaluation #

            source
            def Sym.padRow {T : Type} [ValueType T] {k : ℕ} (m : ℕ) (d : Tuple T (k * (7 + k))) :
            Tuple T ((k + m) * (7 + k))

            The padding row a scalar aggregation adds under a descriptor: the descriptor's cells, then constant cells.

            Equations
            Instances For
              Dependency graph
              source
              noncomputable def Sym.goodSet {T : Type} [ValueType T] {k : ℕ} (C : Finset T) (par : Fin k → T) :
              Finset T

              The good values, as a finite set.

              Equations
              Instances For
                Dependency graph
                source
                def Sym.SymSrc {T : Type} [ValueType T] {c n : ℕ} {κ : Fin n → ColKind} {l : List (String × ℕ)} (Θ : Set (SeqAggFunc T)) (q : AggQueryIn T c n κ l) :
                Prop

                What the symbolic evaluation asks of its input query: a signature whose aggregates count, windows over all-regular inputs, and restricted recursions.

                Equations
                Instances For
                  Dependency graph

                  Goodness depends on the instance only where the query reads it #

                  source
                  theorem Sym.sym_correct {T : Type} [ValueType T] {k c : ℕ} (env : SymEnv T k c) (Θ : Set (SeqAggFunc T)) (f : ℕ → String) {n : ℕ} {κ : Fin n → ColKind} (q : AggQueryIn T (k + c) n κ) (hsrc : SymSrc Θ q) (hfresh : ∀ (i : ℕ), AggQueryIn.noMention (f i) q ∧ EnvNoMention env (f i)) (D : Database T) (γ : Fin c → T) (par : Fin k → T) (henv : EnvOK env D γ) (hamb : ∀ (j : Fin c), CG (cutAt env D γ) (γ j)) (hgood : Good (CG (cutAt env D γ)) q D (Fin.append par γ)) (hset : q.SettlesAt D (Fin.append par γ)) :
                  SliceIs (cutAt env D γ) par ((sym env f q).evaluatePlain D γ) (Multiset.map (fun (v : Tuple T n) => (v, Fin.elim0)) (q.evaluatePlain D (Fin.append par γ)))

                  The symbolic evaluation is correct on a closed query: under the descriptor of a parameter row, its symbolic relation holds the encodings of the rows the query computes at that row.

                  Dependency graph