Documentation

Provenance.SymOver

The apply written with products is well formed over the schema #

A query is well formed over a schema when every relation it reads is declared, and every name it binds is fresh in its scope. The constructions of Provenance.SymApply bind names from a supply, sliced so that a construction never binds, inside a recursion, the name that recursion binds. Sym.Over sch A q says that q is well formed over sch and names nothing outside A; each construction is shown to keep it, with A the names of its input and its supply's.

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

Well formed over a schema, naming only names in A.

Equations
Instances For
    Dependency graph

    Supplies of names #

    The order queries and the environment #

    source
    structure Sym.EnvOver {T : Type} [ValueType T] {k c : ℕ} (sch : Schema) (A : String → Prop) (env : SymEnv T k c) :
    Prop

    The environment's queries are well formed, naming only A.

    Instances For
      Dependency graph

      The relations a query reads #

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

      Every relation the query reads is declared, its name in A.

      Equations
      Instances For
        Dependency graph

        Supplies, sliced #

        source
        def Sym.Sup (A : String → Prop) (f : ℕ → String) :
        String → Prop

        The names of A and of a supply.

        Equations
        Instances For
          Dependency graph
          source
          structure Sym.SupOK (sch : Schema) (A : String → Prop) (f : ℕ → String) :
          Prop

          A supply of fresh names: injective, undeclared, and outside A.

          Instances For
            Dependency graph

            The cut is well formed #

            source
            def Sym.SupP (A : String → Prop) (f : ℕ → String) (P : ℕ → Prop) :
            String → Prop

            The names of A and of a supply at the indices P holds of.

            Equations
            Instances For
              Dependency graph

              The table and the apply are well formed #

              source
              theorem Sym.over_applyX {T : Type} [ValueType T] {k c : ℕ} {sch : Schema} {A : String → Prop} (cnt : SeqAggFunc T) (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)} {AL AV : String → Prop} (hf : SupOK sch A f) (hL : Over sch AL L) (hR : RelsIn sch A R) (hV : Over sch AV VQ) (hAV : ∀ (i : ℕ), ¬AV (part f 1 i)) :
              Over sch (fun (x : String) => Sup A f x ∨ AL x ∨ AV x) (applyX cnt f L R VQ)

              The apply written with products is well formed, naming the names of its operands, of its pool and of its supply. The pool may name anything but the names of the union the apply builds over it.

              Dependency graph