Documentation

Provenance.AllRegular

Reading every column as a value #

In the plain semantics every column holds a value of the domain: the kind vector is a syntactic index, saying which operators may be written where, and AggQueryIn.evaluatePlain returns plain tuples. The operators that compare keys – duplicate elimination, the difference, a grouping's and a partition's indices – are the ones that insist on regular columns, and AggQueryIn.Explode is what bridges them: it reads an aggregate column as a key, and over a plain relation it is the identity (its own docstring says so). AggQueryIn.Retag does the same between the two value-armed kinds.

This module makes that into a theorem: every query is plain-equivalent to one whose columns are all regular (AggQueryIn.exists_allReg), so the kind discipline costs nothing in the plain semantics. Three readings of an aggregate column have exact regular counterparts – an aggregate atom is the same comparison on the column, a range atom is its two comparisons, and a column read as a token is the column – and the one that has none is ProjColIn.aggTerm, which post-composes the column with an arbitrary function of the domain: no term expresses that.

A window is the other exception, and for a different reason: it is the one operator whose plain semantics reads the kind vector, reading its input through ColKind.readTuple. That nulling is how the library lists a frame, and it is one listing the clause allows. An aggregation is determinate where the listing cannot matter – the aggregate is symmetric, or any two peers of the clause carry equal values of the aggregated term – and then every listing the clause allows gives one value. Re-typing changes the listing, since an aggregate column read as a value enters the tie-break, but only inside a block of peers, so a determinate window reads the same value either way (ValueFrame.windowValueOpt_readTuple_of_det). That is what AggQueryIn.Retypable asks of a window – determinacy on every instance, quantified as AggQueryIn.recSettles is, or an all-regular input where no column moves. A FILTER clause is asked to read the occurrence's regular columns, as SQL has it (an aggregate may not occur inside the FILTER of an aggregate), and is then carried through with nothing further to prove.

What this is for: the swaps of AggQueryIn.exists_selFree and AggQueryIn.exists_prodFree – a selection written with a difference, a product written with an apply – are stated over queries whose columns are regular, because that is what Diff and an apply's left side take. Regularizing first is what lets them apply to a query that has aggregate columns in its type and ordinary values in its rows.

The three readings that have regular counterparts #

source
def TermGIn.toReg {T : Type} [ValueType T] {c n : ℕ} {κ : Fin n → ColKind} :
TermGIn T c κ → TermGIn T c (ColKind.allReg n)

A term reading every column as a regular one. A provenance column is read as the value it holds; the aggregate-comparison gate has no plain value of its own (the generic evaluators give it 0), so it becomes that constant.

Equations
Instances For
    Dependency graph
    source
    def GenPredIn.toReg {T : Type} [ValueType T] {c n : ℕ} {κ : Fin n → ColKind} :
    GenPredIn T c κ → GenPredIn T c (ColKind.allReg n)

    A predicate reading every column as a regular one. An aggregate atom becomes the same comparison on the column, and a range atom the conjunction of its two – which is what it says on a row, the difference between them being what they annotate.

    Equations
    Instances For
      Dependency graph
      source
      def ProjColIn.toReg {T : Type} [ValueType T] {c n : ℕ} {κ : Fin n → ColKind} :
      ProjColIn T c κ → ProjColIn T c (ColKind.allReg n)

      A projection column read as a regular one. A column read as a token is the column; a provenance column is the value it holds; a term over an aggregate column is the same term over that column read as a regular one (TermIn.atCol). Only the rewritten world's column, which carries an arbitrary function, has no counterpart, and is sent to a constant – which is why the lemma below asks sourceCol.

      Equations
      Instances For
        Dependency graph
        source
        @[simp]
        theorem ProjColIn.kind_toReg {T : Type} [ValueType T] {c n : ℕ} {κ : Fin n → ColKind} (p : ProjColIn T c κ) :
        p.toReg.kind = ColKind.reg

        Every column it builds is regular.

        Dependency graph

        Reading a query's own columns as values #

        Explode reads one aggregate column as a key and Retag reads the provenance columns as values, so regularizing a query's columns is a recursion over them. Both are the identity over a plain relation, which is what makes the whole thing invisible to evaluatePlain.

        source
        def regBelow {n : ℕ} (κ : Fin n → ColKind) (m : ℕ) :
        Fin n → ColKind

        The kind vector with the columns below m read as regular.

        Equations
        Instances For
          Dependency graph
          source
          theorem regBelow_zero {n : ℕ} (κ : Fin n → ColKind) :
          regBelow κ 0 = κ
          Dependency graph
          source
          theorem regBelow_ge {n m : ℕ} (κ : Fin n → ColKind) (h : n ≤ m) :
          regBelow κ m = ColKind.allReg n
          Dependency graph
          source
          theorem regBelow_succ_of_le {n : ℕ} (κ : Fin n → ColKind) {m : ℕ} (h : n ≤ m) :
          regBelow κ (m + 1) = regBelow κ m
          Dependency graph
          source
          theorem regBelow_succ {n : ℕ} (κ : Fin n → ColKind) {m : ℕ} (h : m < n) :
          regBelow κ (m + 1) = Function.update (regBelow κ m) ⟨m, h⟩ ColKind.reg
          Dependency graph
          source
          def AggQueryIn.explodeBelow {T : Type} {c n : ℕ} (m : ℕ) {κ : Fin n → ColKind} {l : List (String × ℕ)} :
          AggQueryIn T c n κ l → AggQueryIn T c n (regBelow κ m) l

          Every column below m read as a value.

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

            A query with every column read as a value.

            Equations
            Instances For
              Dependency graph

              The one reading with no regular counterpart #

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

              What a query has to be for its columns to be readable as values. Two things, and both are real.

              No projection column may post-compose an aggregate column (ProjColIn.aggTerm): its value is gf of the column, and the term language applies no arbitrary gf.

              And every window either reads an all-regular input or is determinate on every instance, with no FILTER clause. A window is the one operator whose plain semantics reads the kind vector: it reads its input through ColKind.readTuple, which nulls the aggregate columns, so a window over a re-typed input reads values where the original read 0. Both are listings the clause allows, and they differ only inside a block of peers – an aggregate column read as a value enters the tie-break and nothing else. Determinacy is exactly the condition under which that cannot be seen: the aggregate reads its frame as a bag, or the term it aggregates is constant on the rows the clause leaves tied (Relation.rowsAgree of Provenance.Determinacy, read on the rows the window reads, AggQueryIn.readRows). Since it is a condition on the rows, it is quantified over the instance here, in the manner of AggQueryIn.recSettles; ValueFrame.windowValueOpt_readTuple_of_det is what it buys, and ValueFrame.windowValue_readTuple the symmetric case of the same thing. A query the condition refuses does tell the two readings apart: over the rows (2,5), (2,6), (1,7) whose first column is an aggregate one, with no ORDER BY, so that all three are peers, first_value of the second column reads 5 before the re-typing and 7 after. A FILTER clause is asked to read the occurrence's regular columns, as SQL has it: its truth is then unchanged by the nulling, so it keeps the same rows on both sides.

              Equations
              Instances For
                Dependency graph
                source
                theorem AggQueryIn.retypable_of_usesOnly {T : Type} [ValueType T] {S : Set OpKind} (hw : OpKind.win ∉ S) {c n : ℕ} {κ : Fin n → ColKind} {l : List (String × ℕ)} (q : AggQueryIn T c n κ l) :
                usesOnly S q → q.Retypable

                A window-free query is re-typable. The window is the only thing AggQueryIn.Retypable asks about, every column of the source language re-typing on its own (a column reading an aggregate column reads it through a term, ProjColIn.aggTermOf, and AggQueryIn.usesOnly refuses the rewritten world's arbitrary function). So a query whose classes exclude the window is re-typable outright – which is the case the three passes of Provenance.BasisAssembly are in, the first of them replacing every window by an apply of a scalar aggregation.

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

                What the swaps ask of a query: the input of every selection has regular columns and its predicate has no aggregate atom (so that the selection can become a difference, which takes regular columns), and the left factor of every product has regular columns (so that the product can become an apply, whose left side takes them). It is what AggQueryIn.exists_allReg leaves behind.

                Equations
                Instances For
                  Dependency graph
                  source
                  theorem AggQueryIn.swapReady_selByDiff {T : Type} {k : ℕ} (yes : T) (t : TermGIn T 0 (ColKind.allReg k)) {q : AggQuery T k (ColKind.allReg k)} (hq : SwapReady q) :
                  SwapReady (selByDiff yes t q)

                  The difference a selection becomes is ready for the product swap wherever its input is: it projects, tags and takes differences, and introduces no product and no selection of its own. This is what lets the two swaps be composed, so that the basis with − for σ and the apply for × is reached.

                  Dependency graph

                  A window over columns it does not read #

                  A window reads the regular columns of its input and carries the aggregate ones through: ColKind.readTuple nulls an aggregate column before the partition, the frame, the order and the term see the row. It is one listing of the frame among those the clause allows, which is all the semantics asks for, an aggregation being admitted only where its value does not depend on the listing.

                  That is why re-typing is not free here: reading an aggregate column as a value puts it into the tie-break, which can reorder rows the clause leaves tied, and an order-dependent aggregate reads the reordered sequence. Where the aggregate reads its frame as a bag the reordering is immaterial, and this section proves that much.

                  source
                  theorem ValueFrame.windowValueOpt_readTuple_of_det {T : Type} [ValueType T] {n m p c : ℕ} {κ : Fin n → ColKind} (P : Tuple (Fin n) m) (O : Tuple (Fin n) p) (o : OrderSpec p) (w : ValueFrame T p) (t : TermIn T c n) {f : SeqAggFunc T} (keep : Option (Selection T n)) (hrr : WinReadsReg κ P O t) (hkeep : ∀ (y : Tuple T n), Selection.keepsOpt keep (ColKind.readTuple κ y) = Selection.keepsOpt keep y) (R : Multiset (Tuple T n)) {u : Tuple T n} (hu : u ∈ R) (γ : Fin c → T) (hsym : f.Symmetric ∨ Relation.rowsAgree (Multiset.map (ColKind.readTuple κ) R) (fun (y z : Tuple T n) => o.peer (O.key y) (O.key z)) fun (y : Tuple T n) => t.eval y γ) :
                  windowValueOpt P O o w t f keep (Multiset.map (ColKind.readTuple κ) R) (ColKind.readTuple κ u) γ = windowValueOpt P O o w t f keep R u γ

                  A determinate window reads the same value before and after the nulling, symmetric or not, and with a FILTER clause or without: the two listings of the frame are sorted by the clause's keys and differ only inside a block of peers, where the term does not look (OrderSpec.map_eq_of_keySorted), and a clause that reads the occurrence's regular columns keeps the same rows on both sides. The hypothesis is determinacy – the aggregate reads its frame as a bag, or the term it aggregates is constant on the rows the clause leaves tied.

                  Dependency graph

                  Every query is one whose columns are all values #

                  source
                  theorem AggQueryIn.exists_allReg {T : Type} [ValueType T] {S : Set OpKind} {sch : Schema} (hmb : OpKind.muBag ∉ S) (hms : OpKind.muSet ∉ S) {c n : ℕ} {κ : Fin n → ColKind} {l : List (String × ℕ)} (q : AggQueryIn T c n κ l) :
                  usesOnly S q → q.Retypable → overSchema sch q → ∃ (q' : AggQueryIn T c n (ColKind.allReg n) l), usesOnly S q' ∧ overSchema sch q' ∧ q'.SwapReady ∧ ∀ (D : Database T) (γ : Fin c → T), q.evaluatePlain D γ = q'.evaluatePlain D γ

                  The kind discipline costs nothing in the plain semantics: every query whose projections post-compose no aggregate column is plain-equivalent to one all of whose columns are regular, using the same operator classes and naming the same relations.

                  Each case rebuilds the operator over re-typed children and then reads the columns it produces as values (AggQueryIn.allRegOf), which is the identity there. Explode and Retag disappear: their children come back already regular.

                  Dependency graph