Documentation

Provenance.SymTab

The symbolic evaluation of a query, operator by operator #

Sym.sym maps a query whose context starts with k parameter components to a closed symbolic relation (Provenance.SymOps), and Sym.symB a recursive term to a symbolic term carrying P further columns through its rounds – the counter of a bounded recursion (Provenance.SymMu). The translation reads the relation of descriptors and the counters off an environment (Sym.SymEnv): what it is asked of those is stated where it is used, by the correctness theorem.

A construction outside the fragment the translation is for – an apply, a union, a difference, a duplicate elimination, a set recursion, the rewritten world's operators – translates to an empty relation: such a query is not a symbolic evaluation's input, and the correctness theorem excludes it by hypothesis.

source
structure Sym.SymEnv (T : Type) [ValueType T] (k c : ℕ) :
Type

What the symbolic evaluation reads off its environment: the cut, the relation of descriptors, and for each arity of a bag recursion the width of its counters, the least counter and the successor relation.

Instances For
    Dependency graph
    source
    def Sym.junkB {T : Type} [ValueType T] {c : ℕ} (N M : ℕ) (s : String) :
    AggQueryIn T c N (ColKind.allReg N) [(s, M)]

    An empty relation that reads a hole, for the recursive terms the translation has no case for.

    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      Dependency graph
      source
      def Sym.pvCS {T : Type} {k c m : ℕ} (pv : Fin m → T ⊕ Fin (k + c)) (j : Fin m) :
      CS T k c 0

      The source of a parameter leaf's column.

      Equations
      Instances For
        Dependency graph
        source
        def Sym.tagSA {T : Type} {c N : ℕ} (a : T) :
        Fin (N + 1) → SA T c N

        The row of a symbolic relation with one more column, the tag.

        Equations
        Instances For
          Dependency graph
          source
          def Sym.padSA {T : Type} [ValueType T] {k c : ℕ} (m : ℕ) :
          Fin ((k + m) * (7 + k) + 1) → SA T c (k * (7 + k))

          A padding row of a scalar aggregation's union: a descriptor, constant cells, and the tag 0.

          Equations
          • One or more equations did not get rendered due to their size.
          Instances For
            Dependency graph
            source
            @[irreducible]
            noncomputable def Sym.sym {T : Type} [ValueType T] {k c : ℕ} (env : SymEnv T k c) (f : ℕ → String) {n : ℕ} {κ : Fin n → ColKind} {l : List (String × ℕ)} :
            AggQueryIn T (k + c) n κ l → AggQueryIn T c ((k + n) * (7 + k)) (ColKind.allReg ((k + n) * (7 + k)))

            The symbolic evaluation of a closed query.

            Equations
            Instances For
              Dependency graph
              source
              @[irreducible]
              noncomputable def Sym.symB {T : Type} [ValueType T] {k c : ℕ} (env : SymEnv T k c) (f : ℕ → String) (P : ℕ) (s : String) (m : ℕ) {n : ℕ} {κ : Fin n → ColKind} {l : List (String × ℕ)} :
              AggQueryIn T (k + c) n κ l → AggQueryIn T c ((k + n) * (7 + k) + P) (ColKind.allReg ((k + n) * (7 + k) + P)) [(s, (k + m) * (7 + k) + P)]

              The symbolic evaluation of a recursive term, carrying P further columns through it.

              Equations
              Instances For
                Dependency graph