Documentation

Provenance.AggQuerySubst

Substituting the outer columns #

The apply is defined by substitution: the right side of q₁ ⋈ᴬ q₂ is read, for each row u of the left, as the closed query q₂[u]. The evaluators of Provenance.AggQuery read it under an outer valuation instead, which is what makes them structurally recursive. This module defines the substitution and proves the two readings agree – in the plain semantics for every substitution (AggQueryIn.evaluatePlain_subst), and in the annotated one for a renaming (AggQueryIn.evaluate_substMap): an aggregating operator records the values of the parameters it reads in the family it stamps, and a constant put in a parameter's place is not read as one.

substMap sends each outer position either to a value or to an outer position of the target context. That generality is what the Apply case of the recursion needs: the right side of an apply reads its left neighbor's columns and the ambient outer ones, and closing the ambient part must leave the neighbor's alone. Closing everything is the special case subst.

The valuation a substitution induces #

source
def substVal {T : Type} {c d : ℕ} (θ : Fin c → T ⊕ Fin d) (γ : Fin d → T) :
Fin c → T

Reading the source context through a substitution: an outer position sent to a value reads that value, one sent to an outer position of the target reads the target's valuation there.

Equations
Instances For
    Dependency graph

    Substitution on terms, predicates and projection columns #

    source
    def TermIn.substMap {T : Type} {c d n : ℕ} (θ : Fin c → T ⊕ Fin d) :
    TermIn T c n → TermIn T d n

    Substitute the outer columns of a term.

    Equations
    Instances For
      Dependency graph
      source
      @[simp]
      theorem TermIn.regOnly_substMap {T : Type} {c d n : ℕ} (θ : Fin c → T ⊕ Fin d) (κ : Fin n → ColKind) (t : TermIn T c n) :
      regOnly κ (substMap θ t) = regOnly κ t

      Substituting the outer columns reads no column of the row, so what a term reads of them is unchanged – which is what a window's WinReadsReg asks of its term.

      Dependency graph
      source
      def TermGIn.substMap {T : Type} {c d n : ℕ} {κ : Fin n → ColKind} (θ : Fin c → T ⊕ Fin d) :
      TermGIn T c κ → TermGIn T d κ

      Substitute the outer columns of a generalized term.

      Equations
      Instances For
        Dependency graph
        source
        def GenPredIn.substMap {T : Type} {c d n : ℕ} {κ : Fin n → ColKind} (θ : Fin c → T ⊕ Fin d) :
        GenPredIn T c κ → GenPredIn T d κ

        Substitute the outer columns of a generalized predicate.

        Equations
        Instances For
          Dependency graph
          source
          @[simp]
          theorem GenPredIn.hasAggAtom_substMap {T : Type} {c d n : ℕ} {κ : Fin n → ColKind} (θ : Fin c → T ⊕ Fin d) (φ : GenPredIn T c κ) :
          (substMap θ φ).hasAggAtom = φ.hasAggAtom
          Dependency graph
          source
          def ProjColIn.substMap {T : Type} {c d n : ℕ} {κ : Fin n → ColKind} (θ : Fin c → T ⊕ Fin d) :
          ProjColIn T c κ → ProjColIn T d κ

          Substitute the outer columns of a projection column.

          Equations
          Instances For
            Dependency graph
            source
            @[simp]
            theorem ProjColIn.kind_substMap {T : Type} {c d n : ℕ} {κ : Fin n → ColKind} (θ : Fin c → T ⊕ Fin d) (p : ProjColIn T c κ) :
            (substMap θ p).kind = p.kind

            The substitution does not change an output column's kind.

            Dependency graph

            Substitution on queries #

            source
            def substRd {T : Type} {c d : ℕ} (θ : Fin c → T ⊕ Fin d) (rd : Fin c → Bool) :
            Fin d → Bool

            The parameters a substituted operator reads: those the source's parameters are sent to.

            Equations
            Instances For
              Dependency graph
              source
              def AggQueryIn.substMap {T : Type} {c d n : ℕ} {κ : Fin n → ColKind} {l : List (String × ℕ)} (θ : Fin c → T ⊕ Fin d) (q : AggQueryIn T c n κ l) :
              AggQueryIn T d n κ l

              Substitute the outer columns of a query. The right side of an apply reads its left neighbor's columns first and the ambient outer ones after, so the substitution passes under it by leaving the neighbor's block alone and shifting the ambient one.

              Equations
              Instances For
                Dependency graph
                source
                @[reducible, inline]
                abbrev AggQueryIn.subst {T : Type} {c n : ℕ} {κ : Fin n → ColKind} {l : List (String × ℕ)} (u : Fin c → T) (q : AggQueryIn T c n κ l) :
                AggQueryIn T 0 n κ l

                Close a query: give every outer column a value, written q[u].

                Equations
                Instances For
                  Dependency graph
                  source
                  def substCtx {T K : Type} {c d : ℕ} (θ : Fin c → T ⊕ Fin d) (u : Tuple (GenValue T K) d) :
                  Tuple (GenValue T K) c

                  Substituting a context of general values: a constant becomes a regular value.

                  Equations
                  Instances For
                    Dependency graph
                    source
                    def EvalEnv.substEnv {T K : Type} {c d : ℕ} (E : EvalEnv T K) (θ : Fin c → T ⊕ Fin d) (γ : Fin d → T) :
                    EvalEnv T K

                    The environment a substituted query is read in, seen from the source: its context substituted.

                    Equations
                    Instances For
                      Dependency graph

                      The two readings agree #

                      source
                      theorem AggQueryIn.evaluatePlain_substMap {T : Type} [ValueType T] {c n : ℕ} {κ : Fin n → ColKind} {l : List (String × ℕ)} (q : AggQueryIn T c n κ l) {d : ℕ} (θ : Fin c → T ⊕ Fin d) (D : Database T) (γ : Fin d → T) :
                      (substMap θ q).evaluatePlain D γ = q.evaluatePlain D (substVal θ γ)

                      Substituting and evaluating is evaluating under the substituted valuation, for the plain semantics.

                      Dependency graph

                      Tokens under substitution #

                      The parameters a substituted query reads #

                      A family records the values of the parameters its operator reads, so a substitution moves the family exactly when it moves those values. A renaming – every outer column sent to an outer column, in order – moves nothing: the substituted operator reads the renamed columns, which hold the same values in the same order. That is the substitution an apply's right side is read through (applyOuter). A substitution sending a parameter to a constant does change the family: the constant is no parameter of the substituted operator, so its value leaves the family.

                      source
                      def IsRenaming {T : Type} {c d : ℕ} (θ : Fin c → T ⊕ Fin d) :
                      Prop

                      A substitution that renames the outer columns, in order.

                      Equations
                      Instances For
                        Dependency graph
                        source
                        theorem AggQueryIn.evaluate_substMap {T : Type} [ValueType T] {K : Type} [CommSemiringWithMonus K] [DecidableEq K] [HasAltLinearOrder K] {c n : ℕ} {κ : Fin n → ColKind} {l : List (String × ℕ)} (q : AggQueryIn T c n κ l) {d : ℕ} (θ : Fin c → T ⊕ Fin d) (_hθ : IsRenaming θ) (dB : AnnotatedDatabase T K) (γ : Fin d → T) (E : EvalEnv T K) :
                        (substMap θ q).evaluate dB γ E = q.evaluate dB (substVal θ γ) (E.substEnv θ γ)

                        Substituting and evaluating is evaluating under the substituted valuation, for the annotated semantics.

                        Dependency graph

                        Closing a query: q[u] #

                        source
                        theorem AggQueryIn.evaluatePlain_subst {T : Type} [ValueType T] {c n : ℕ} {κ : Fin n → ColKind} {l : List (String × ℕ)} (u : Fin c → T) (q : AggQueryIn T c n κ l) (D : Database T) :
                        (subst u q).evaluatePlain D = q.evaluatePlain D u

                        Evaluating a closed instance is evaluating under the values it was closed with, in the plain semantics.

                        Dependency graph
                        source
                        theorem AggQueryIn.evaluatePlain_Apply_subst {T : Type} [ValueType T] {n₁ n₂ : ℕ} {κ₂ : Fin n₂ → ColKind} (q₁ : AggQuery T n₁ (ColKind.allReg n₁)) (q₂ : AggQueryIn T n₁ n₂ κ₂) (D : Database T) :
                        (Apply q₁ q₂).evaluatePlain D = Multiset.bind (evaluatePlain q₁ D) fun (u : Tuple T n₁) => Multiset.map (fun (v : Fin n₂ → T) => Fin.append u v) ((subst u q₂).evaluatePlain D)

                        Plain counterpart: ⟦q₁ ⋈ᴬ q₂⟧ = {(u, v) ∣ u ∈ ⟦q₁⟧, v ∈ ⟦q₂[u]⟧}.

                        Dependency graph

                        Stripping commutes with substituting #

                        What an apply's right side reads of its left row #

                        source
                        def GenRow.fin {T K : Type} [CommSemiringWithMonus K] {n : ℕ} (r : GenRow T K n) :
                        Tuple (GenValue T K) n × K

                        A row with its annotation finalized, its columns kept: what every reading of an annotated evaluation reads of a row.

                        Equations
                        Instances For
                          Dependency graph

                          Substitution keeps a query well-kinded #

                          A substitution sends a parameter to a constant or to a parameter of the new context; it keeps the query well-kinded when it sends each parameter to one of the same kind, a constant being regular.