Documentation

Provenance.Genericity

Genericity of the minimal universe: a query reads its parameters only up to order #

The order-type lemma: a recursion-free query of the minimal signature, with parameters, answers up to the substitution of its parameters the same on any two parameter tuples that fall the same way among a finite set of values the query and the instance fix. This module builds the pieces: a faithful value map – a function of values that keeps the null apart and the order among the values it is read on – and the fact that every comparison the evaluator makes commutes with one.

Faithful value maps #

source
structure FaithfulOn {T : Type} [ValueType T] (τ : T → T) (W : Set T) :
Prop

A value map faithful on a set: it keeps the null and the order among the values of the set. Every comparison the minimal signature makes between values of the set is preserved by it.

Instances For
    Dependency graph

    The constants a query names, all of them #

    AggQueryIn.consts lists a projection's constants only, which is what the value analysis needs; a value map that is to commute with the evaluator has to fix the constants of every comparison too.

    source
    def BoolTerm.consts {T : Type} [ValueType T] {k : ℕ} (b : BoolTerm T k) :
    Finset T

    The constants of a Boolean term.

    Equations
    Instances For
      Dependency graph
      source
      def Selection.consts {T : Type} [ValueType T] {k : ℕ} :
      Selection T k → Finset T

      The constants of a classical selection.

      Equations
      Instances For
        Dependency graph
        source
        def Selection.constsOpt {T : Type} [ValueType T] {k : ℕ} :
        Option (Selection T k) → Finset T

        The constants of a clause, or none.

        Equations
        Instances For
          Dependency graph
          source
          def GenPredIn.consts {T : Type} [ValueType T] {c k : ℕ} {κ : Fin k → ColKind} :
          GenPredIn T c κ → Finset T

          The constants of a predicate of the general syntax.

          Equations
          Instances For
            Dependency graph
            source
            def TermIn.constsFam {T : Type} [ValueType T] {c k m : ℕ} (ts : Fin m → TermIn T c k) :
            Finset T

            The constants of a family of terms.

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

              Every constant a query names, in its columns, its predicates, its clauses and the terms its aggregates read.

              Equations
              Instances For
                Dependency graph

                Terms, predicates and selections under a faithful map #

                A function-free term is a column, an outer column or a constant, so a map fixing the constants commutes with it; a comparison between values of the set the map is faithful on reads alike.

                What a count reads #

                A count is a function of how many non-null values its sequence holds (SeqAggFunc.ReadsCount), so it reads a listing of a bag through the bag's non-null count alone, and a faithful map of the bag's rows keeps that count.

                source
                def Multiset.nonNullCount {T : Type} [ValueType T] {c m : ℕ} (t : TermIn T c m) (γ : Fin c → T) (S : Multiset (Tuple T m)) :
                ℕ

                The non-null count of a term over a bag of rows.

                Equations
                Instances For
                  Dependency graph

                  Frames and window values under a faithful map #

                  The values a query computes #

                  In the minimal signature a query builds a value only by counting: every other value of its result is read off the instance, off the context or off its own constants. AggQueryIn.countValsAll collects the counts – the values of the aggregate columns of every aggregating node, at every context and, under a recursion, at every round – so that the value lemma AggQueryIn.valsIn_evaluatePlain can say where every value of a result comes from.

                  source
                  def Relation.mapVals {T : Type} (τ : T → T) {n : ℕ} (r : Relation T n) :
                  Relation T n

                  A relation with every value mapped.

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

                    The counts a query computes: the values of the aggregate columns of each of its aggregating nodes, over every context, and, under a recursion, over every relation the recursive name may be bound to. It is the set a faithful map must fix for the query to commute with it.

                    Equations
                    Instances For
                      Dependency graph
                      source
                      theorem AggQueryIn.valsIn_evaluatePlain {T : Type} [ValueType T] {Θ : Set (SeqAggFunc T)} {c n : ℕ} {κ : Fin n → ColKind} {l : List (String × ℕ)} (q : AggQueryIn T c n κ l) :
                      inSig Θ q → ∀ (D : Database T) (γ : Fin c → T) (V : Set T), (∀ p ∈ q.leaves, ∀ (r : Relation T p.1), Database.find p.1 p.2 D = some r → ∀ (u : Tuple T p.1), Multiset.Mem r u → ∀ (j : Fin p.1), u j ∈ V) → (∀ (j : Fin c), γ j ∈ V) → (∀ a ∈ q.allConsts, a ∈ V) → q.countValsAll D ⊆ V → ∀ (u : Tuple T n), Multiset.Mem (q.evaluatePlain D γ) u → ∀ (j : Fin n), u j ∈ V

                      Where every value of a result comes from: the instance at the relations the query reads (its holes included), the context, the query's constants, or a count the query computes. No settling is asked: a recursion's junk value is a sum of its rounds, which read like the rest.

                      Dependency graph

                      A query commutes with a faithful map #

                      A map that is faithful on the values a query reads, fixes its constants and fixes the counts it computes commutes with its evaluation: the result on the mapped instance in the mapped context is the mapped result. The counts have to be fixed because the query recomputes them – a count is the number of non-null values read, which the map preserves, so the mapped result holds the count and not its image. Nothing is asked of the recursions: their rounds correspond one by one, settling or not.

                      source
                      theorem AggQueryIn.evaluatePlain_faithful {T : Type} [ValueType T] {cnt : SeqAggFunc T} (hcnt : cnt.ReadsCount) {c n : ℕ} {κ : Fin n → ColKind} {l : List (String × ℕ)} (q : AggQueryIn T c n κ l) :
                      inSig {cnt} q → ∀ {τ : T → T} {W : Set T}, FaithfulOn τ W → τ 0 = 0 → 0 ∈ W → ∀ (D D' : Database T) (γ : Fin c → T), (∀ p ∈ q.leaves, Database.find p.1 p.2 D' = Option.map (Relation.mapVals τ) (Database.find p.1 p.2 D)) → (∀ p ∈ q.leaves, ∀ (r : Relation T p.1), Database.find p.1 p.2 D = some r → ∀ (u : Tuple T p.1), Multiset.Mem r u → ∀ (j : Fin p.1), u j ∈ W) → (∀ (j : Fin c), γ j ∈ W) → (∀ a ∈ q.allConsts, τ a = a ∧ a ∈ W) → (∀ v ∈ q.countValsAll D, τ v = v ∧ v ∈ W) → q.evaluatePlain D' (τ ∘ γ) = Multiset.map (fun (u : Fin n → T) => τ ∘ u) (q.evaluatePlain D γ)

                      A query of the minimal signature commutes with a faithful map that fixes its constants and its counts: on an instance whose relations at the query's leaves are the mapped ones, in the mapped context, it returns the mapped result.

                      Dependency graph

                      Order types #

                      Two parameter tuples have the same order type over a finite set of values when each parameter falls at the same place among the set's values and the parameters compare alike pairwise. A map sending one to the other and fixing the set is then faithful on the set and on the first tuple, which is what the commutation theorem asks; over a set holding the null, the order type decides nullness too. There are finitely many order types over a set, polynomially many in its size, which is what bounds the counts a query can compute as its parameters vary.

                      source
                      def Finset.cardLe {T : Type} [ValueType T] (S : Finset T) (x : T) :
                      ℕ

                      How many values of S are at most x.

                      Equations
                      Instances For
                        Dependency graph
                        source
                        theorem Finset.cardLe_le_card {T : Type} [ValueType T] (S : Finset T) (x : T) :
                        S.cardLe x ≤ S.card
                        Dependency graph
                        source
                        @[reducible, inline]
                        abbrev OrdType {T : Type} (S : Finset T) (c : ℕ) :
                        Type

                        The order types over S of tuples of c parameters.

                        Equations
                        Instances For
                          Dependency graph
                          source
                          def ordType {T : Type} [ValueType T] (S : Finset T) {c : ℕ} (u : Fin c → T) :
                          OrdType S c

                          The order type of a parameter tuple over S: for each parameter, how many values of S are at most it and whether it is one of them, and how the parameters compare pairwise.

                          Equations
                          Instances For
                            Dependency graph
                            source
                            theorem exists_faithful_of_ordType_eq {T : Type} [ValueType T] (S : Finset T) (hν : ∀ (ν : T), ValueType.nullVal = some ν → ν ∈ S) {c : ℕ} {u u' : Fin c → T} (h : ordType S u = ordType S u') :
                            ∃ (τ : T → T), FaithfulOn τ (↑S ∪ Set.range u) ∧ (∀ a ∈ S, τ a = a) ∧ ∀ (i : Fin c), τ (u i) = u' i

                            Two tuples of one order type are related by a faithful map fixing the set, where the set holds the null.

                            Dependency graph
                            source
                            noncomputable def ordRep {T : Type} [ValueType T] (S : Finset T) (c : ℕ) (ω : OrdType S c) :
                            Fin c → T

                            A representative parameter tuple of an order type, where one exists.

                            Equations
                            Instances For
                              Dependency graph
                              source
                              def Relation.valsAtCols {T : Type} [ValueType T] {n : ℕ} (r : Multiset (Tuple T n)) (J : Finset (Fin n)) :
                              Finset T

                              The values a relation holds at some of its columns.

                              Equations
                              Instances For
                                Dependency graph
                                source
                                noncomputable def AggQueryIn.repVals {T : Type} [ValueType T] (S : Finset T) {c n : ℕ} {κ : Fin n → ColKind} {l : List (String × ℕ)} (Q : AggQueryIn T c n κ l) (J : Finset (Fin n)) (D : Database T) :
                                Finset T

                                The values at some columns of a query's result at a representative of each order type over S.

                                Equations
                                Instances For
                                  Dependency graph
                                  source
                                  noncomputable def AggQueryIn.countTypes {T : Type} [ValueType T] (B : Finset T) {c n : ℕ} {κ : Fin n → ColKind} {l : List (String × ℕ)} :
                                  AggQueryIn T c n κ l → Database T → Finset T

                                  The count types of a query over a base set B: at each aggregating node, the values of its aggregate columns at a representative of each order type of its context over B and the count types of its input. Every count the query computes is one of these, and there are polynomially many in |B|.

                                  Equations
                                  Instances For
                                    Dependency graph

                                    Every count is a count type #

                                    At an aggregating node, the counts at a context are the counts at the representative of its order type: the two contexts are related by a faithful map fixing the base set and the input's count types, with which the input commutes.

                                    source
                                    theorem AggQueryIn.countValsAll_subset {T : Type} [ValueType T] {cnt : SeqAggFunc T} (hcnt : cnt.ReadsCount) {B : Finset T} (hν : ∀ (ν : T), ValueType.nullVal = some ν → ν ∈ B) (h0 : 0 ∈ B) {c n : ℕ} {κ : Fin n → ColKind} {l : List (String × ℕ)} (q : AggQueryIn T c n κ l) :
                                    inSig {cnt} q → q.hygienic → (∀ p ∈ l, noMention p.1 q) → ∀ (D D' : Database T), (∀ p ∈ q.leaves, (p.2, p.1) ∉ l → Database.find p.1 p.2 D' = Database.find p.1 p.2 D) → (∀ p ∈ q.leaves, (p.2, p.1) ∉ l → ∀ (r : Relation T p.1), Database.find p.1 p.2 D = some r → ∀ (u : Tuple T p.1), Multiset.Mem r u → ∀ (j : Fin p.1), u j ∈ B) → (∀ a ∈ q.allConsts, a ∈ B) → q.countValsAll D' ⊆ ↑(B ∪ countTypes B q D)

                                    Every count a query computes is a count type: over a base set holding the instance's values at the query's leaves, its constants, the zero and the null, the counts of a hygienic query of the minimal signature lie in the base set and its count types. The instance it is read at may differ from the one the count types are taken over at the holes, which is what a recursion's rounds need.

                                    Dependency graph

                                    There are polynomially many count types #

                                    An aggregating node's count types at one order type are the values of its aggregate columns at one context, no more than its groups, which are tuples over the base set, the count types of its input and the context; and there are polynomially many order types.

                                    source
                                    def PolyBounded (f : ℕ → ℕ) :
                                    Prop

                                    A function of a natural number bounded by a polynomial.

                                    Equations
                                    Instances For
                                      Dependency graph
                                      source
                                      theorem card_ordType {T : Type} (S : Finset T) (c : ℕ) :
                                      Fintype.card (OrdType S c) = (2 * (S.card + 1)) ^ c * 2 ^ (c * c)

                                      There are (2(|S|+1))^c · 2^(c·c) order types over S of c parameters.

                                      Dependency graph
                                      source
                                      theorem AggQueryIn.exists_polyBound_countTypes {T : Type} [ValueType T] {cnt : SeqAggFunc T} (hcnt : cnt.ReadsCount) {c n : ℕ} {κ : Fin n → ColKind} {l : List (String × ℕ)} (q : AggQueryIn T c n κ l) :
                                      inSig {cnt} q → q.hygienic → (∀ p ∈ l, noMention p.1 q) → ∃ (f : ℕ → ℕ), PolyBounded f ∧ ∀ (B : Finset T) (D : Database T), (∀ (ν : T), ValueType.nullVal = some ν → ν ∈ B) → 0 ∈ B → (∀ p ∈ q.leaves, (p.2, p.1) ∉ l → ∀ (r : Relation T p.1), Database.find p.1 p.2 D = some r → ∀ (u : Tuple T p.1), Multiset.Mem r u → ∀ (j : Fin p.1), u j ∈ B) → (∀ a ∈ q.allConsts, a ∈ B) → (countTypes B q D).card ≤ f B.card

                                      There are polynomially many count types: the count types of a hygienic query of the minimal signature over a base set holding its instance values, its constants, the zero and the null number at most a polynomial, fixed by the query, in the size of the base set.

                                      Dependency graph
                                      source
                                      theorem AggQueryIn.exists_card_bound_muSet {T : Type} [ValueType T] {cnt : SeqAggFunc T} (hcnt : cnt.ReadsCount) {c n : ℕ} (s : String) (q₀ : AggQueryIn T c n (ColKind.allReg n)) (q₁ : AggQueryIn T c n (ColKind.allReg n) [(s, n)]) (hs : inSig {cnt} (MuSet s q₀ q₁)) (hh : (MuSet s q₀ q₁).hygienic) :
                                      ∃ (f : ℕ → ℕ), PolyBounded f ∧ ∀ (B : Finset T) (D : Database T) (γ : Fin c → T), (∀ (ν : T), ValueType.nullVal = some ν → ν ∈ B) → 0 ∈ B → (∀ (j : Fin c), γ j ∈ B) → (∀ p ∈ (MuSet s q₀ q₁).leaves, ∀ (r : Relation T p.1), Database.find p.1 p.2 D = some r → ∀ (u : Tuple T p.1), Multiset.Mem r u → ∀ (j : Fin p.1), u j ∈ B) → (∀ a ∈ (MuSet s q₀ q₁).allConsts, a ∈ B) → Multiset.card ((MuSet s q₀ q₁).evaluatePlain D γ) ≤ f B.card

                                      A set recursion's fixpoint is polynomially bounded in the number of values it may read: its rows are duplicate-free tuples over the base set and the count types, of which there are polynomially many.

                                      Dependency graph