Documentation

Provenance.Coherence

One family identifier, one value #

An operator building aggregate values stamps each with a family identifier: its label, the group key, the parameters it records, the column, and the terms applied since. This file proves that across all the evaluations a query performs – one per row of an apply's left side, one per round of a recursion – two values carrying the same identifier are the same value (AggQueryIn.builds_coherent). This is what lets a recursion's body build values: what it builds in one round, it builds again in the next.

Three things are asked of the query, each because an identifier would otherwise not determine the value:

The fences #

source
def AggQueryIn.allFramesContainSelf {T : Type} [ValueType T] {c n : ℕ} {κ : Fin n → ColKind} {l : List (String × ℕ)} :
AggQueryIn T c n κ l → Prop

Every window frame contains its current row, single-frame windows included.

Equations
Instances For
    Dependency graph
    source
    def AggQueryIn.sourceCols {T : Type} {c n : ℕ} {κ : Fin n → ColKind} {l : List (String × ℕ)} :
    AggQueryIn T c n κ l → Prop

    Every projection column is one of the source language's: none applies an arbitrary function to an aggregate value.

    Equations
    Instances For
      Dependency graph

      The values an evaluation builds #

      source
      noncomputable def AggQueryIn.Builds {T : Type} [ValueType T] {K : Type} [CommSemiringWithMonus K] [DecidableEq K] [HasAltLinearOrder K] {c n : ℕ} {κ : Fin n → ColKind} {l : List (String × ℕ)} :
      AggQueryIn T c n κ l → AnnotatedDatabase T K → (Fin c → T) → EvalEnv T K → AggTok T K → Prop

      The values the operators of a query build while it is evaluated: the columns an operator adds to its output rows, and what its subqueries build – once per row of an apply's left side, once per round of a recursion.

      Equations
      Instances For
        Dependency graph

        Values derived by terms #

        source
        inductive TermCl {T K₀ : Type} [ValueType T] (S : AggTok T K₀ → Prop) :
        AggTok T K₀ → Prop

        The values derived from S by terms: S and every term over one of them.

        Instances For
          Dependency graph
          source
          def FamFun {T K₀ : Type} (S : AggTok T K₀ → Prop) :
          Prop

          One family identifier, one value.

          Equations
          Instances For
            Dependency graph

            Terms over coherent values #

            source
            def FamId.terms' {T : Type} :
            FamId T → List (TermIn T 1 0)

            The terms a family identifier records.

            Equations
            Instances For
              Dependency graph
              source
              def FamId.root {T : Type} :
              FamId T → FamId T

              A family identifier with its terms forgotten.

              Equations
              Instances For
                Dependency graph
                source
                def AggTok.postcompTerms {T : Type} [ValueType T] {K₀ : Type} (x : AggTok T K₀) :
                List (TermIn T 1 0) → AggTok T K₀

                Terms applied in order.

                Equations
                Instances For
                  Dependency graph

                  What is built: the operator's label, no term #

                  The width of each operator #

                  source
                  def FamId.col {T : Type} :
                  FamId T → ℕ

                  The column a family identifier records.

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

                    Each operator's label with the number of columns it builds.

                    Equations
                    Instances For
                      Dependency graph

                      Where a row's values come from #

                      source
                      def EvalEnv.Toks {T K : Type} {c : ℕ} (E : EvalEnv T K) (γ : Fin c → T) (l : List (String × ℕ)) (x : AggTok T K) :
                      Prop

                      The values an environment provides to a query reading the rounds l: its context's, and those of the rounds bound to the names in l.

                      Equations
                      Instances For
                        Dependency graph
                        source
                        theorem AggQueryIn.rowToks {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) :
                        q.sourceCols → ∀ (d : AnnotatedDatabase T K) (γ : Fin c → T) (E : EvalEnv T K), ∀ r ∈ q.evaluate d γ E, ∀ (k : Fin n) (x : AggTok T K), r.1 k = Sum.inr x → TermCl (fun (y : AggTok T K) => q.Builds d γ E y ∨ E.Toks γ l y) x

                        Every value a row holds is built by the query or provided by the environment, up to terms.

                        Dependency graph

                        Equal parameters, equal inputs #

                        One evaluation of a window: the value is the tuple's #

                        One evaluation of an operator: one value per identifier #

                        Coherent situations #

                        source
                        def EvalEnv.SitOK {T K : Type} {c : ℕ} (E : EvalEnv T K) (γ : Fin c → T) :
                        Prop

                        A coherent situation: the plain context is the collapse of the environment's context, as the evaluator keeps it.

                        Equations
                        Instances For
                          Dependency graph

                          The values a situation provides #

                          What an operator stamps #

                          The rows an operator builds #

                          Two evaluations of one operator #

                          source
                          theorem AggQueryIn.coh_node {T : Type} [ValueType T] {K : Type} [CommSemiringWithMonus K] [DecidableEq K] [HasAltLinearOrder K] {c n : ℕ} {κ : Fin n → ColKind} (node : AggQueryIn T c n κ) (hrr : node.readsRecorded) {rd : Fin c → Bool} (hrd : rd = node.readsOuter) (lab : ℕ) (P : GenRow T K n → AggTok T K → Prop) (d : AnnotatedDatabase T K) (Q : AggTok T K → AggTok T K → Prop) (hfam : ∀ (γ : Fin c → T) (E : EvalEnv T K) (r : GenRow T K n) (x : AggTok T K), r ∈ node.evaluate d γ E → P r x → ∃ (key : List T) (j : ℕ), x.fam = FamId.mk lab key (E.paramKey rd γ) j []) (hfun : ∀ (γ : Fin c → T) (E : EvalEnv T K) (r r' : GenRow T K n) (x y : AggTok T K), r ∈ node.evaluate d γ E → r' ∈ node.evaluate d γ E → P r x → P r' y → x.fam.family = y.fam.family → Q x y) (U : AggTok T K → Prop) (M : ℕ) (hU : ∀ (x y : AggTok T K), U x → U y → x.fam = y.fam → sizeOf x.fam < M → x = y) {γ₁ γ₂ : Fin c → T} {E₁ E₂ : EvalEnv T K} (hs₁ : E₁.SitOK γ₁) (hs₂ : E₂.SitOK γ₂) (hc₁ : ∀ (k : Fin c) (x : AggTok T K), E₁.ctxAt c γ₁ k = Sum.inr x → U x) (hc₂ : ∀ (k : Fin c) (x : AggTok T K), E₂.ctxAt c γ₂ k = Sum.inr x → U x) {x y : AggTok T K} (hx : ∃ r ∈ node.evaluate d γ₁ E₁, P r x) (hy : ∃ r ∈ node.evaluate d γ₂ E₂, P r y) (hxy : x.fam.family = y.fam.family) (hM : ∀ (φ : FamId T), Sum.inr φ ∈ x.fam.family.2.2 → sizeOf φ < M) :
                          Q x y

                          One operator in two coherent situations builds one value per identifier, given that its parameters' identifiers – which are smaller – already determine their values (hU). Equal identifiers record equal parameters, so the two situations agree where the operator reads (EvalEnv.agree_of_paramKey), so the operator's two evaluations are one (AggQueryIn.evaluate_congr_reads), in which the identifier determines the value (hfun).

                          Dependency graph

                          Combining the cases #

                          Across the evaluations of a query #

                          source
                          def CohRel {T K : Type} [CommSemiringWithMonus K] (x y : AggTok T K) :
                          Prop

                          What coherence says of two values of one family: one identifier, one value, and one family, one class.

                          Equations
                          Instances For
                            Dependency graph
                            source
                            def AggQueryIn.CohAt {T : Type} [ValueType T] {K : Type} [CommSemiringWithMonus K] [DecidableEq K] [HasAltLinearOrder K] (U : AggTok T K → Prop) (M : ℕ) {c n : ℕ} {κ : Fin n → ColKind} {l : List (String × ℕ)} (q : AggQueryIn T c n κ l) (d : AnnotatedDatabase T K) :
                            Prop

                            What the induction carries: in two coherent situations whose provided and built values lie in U, two values the query builds with the same identifier, of size at most M, are equal.

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

                              The theorem #

                              source
                              def FamKeyed {T K₀ : Type} [CommSemiringWithMonus K₀] (S : AggTok T K₀ → Prop) :
                              Prop

                              One family, one class: values of one family are read in one listing, so they carry the same annotations.

                              Equations
                              Instances For
                                Dependency graph
                                source
                                theorem AggQueryIn.builds_coherent {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) (hld : q.labelsDistinct) (hrr : q.readsRecorded) (hsc : q.sourceCols) (hfc : q.allFramesContainSelf) (d : AnnotatedDatabase T K) (R₀ : AggTok T K → Prop) (hR₀t : ∀ (y : AggTok T K), R₀ y → y.fam.terms' = []) (hR₀ : FamFun R₀) (hR₀k : FamKeyed R₀) (hR₀l : ∀ (y : AggTok T K), R₀ y → y.lab ∉ q.labels) {γ₁ γ₂ : Fin c → T} {E₁ E₂ : EvalEnv T K} (hs₁ : E₁.SitOK γ₁) (hs₂ : E₂.SitOK γ₂) (ht₁ : ∀ (x : AggTok T K), E₁.Toks γ₁ l x → TermCl R₀ x) (ht₂ : ∀ (x : AggTok T K), E₂.Toks γ₂ l x → TermCl R₀ x) :
                                FamFun (TermCl fun (x : AggTok T K) => q.Builds d γ₁ E₁ x ∨ q.Builds d γ₂ E₂ x ∨ R₀ x) ∧ FamKeyed (TermCl fun (x : AggTok T K) => q.Builds d γ₁ E₁ x ∨ q.Builds d γ₂ E₂ x ∨ R₀ x)

                                One family identifier, one value, across every evaluation a query performs; one family, one class. In two coherent situations whose provided values are terms over a set R₀ of values that record no term, carry no label of the query and are themselves coherent, the values the query builds in either situation, those of R₀, and every term over them have one value per identifier and one class per family. The induction is on the size of the identifier: an operator's identifier records its parameters' identifiers, which are smaller, and equal parameters make equal inputs (AggQueryIn.coh_node).

                                Dependency graph