Documentation

Provenance.AggQueryRewriting

The rewriting rules (R1)–(R4), natively on the general syntax #

The rewriting of Sen, Maniu & Senellart, ProvSQL turns a query over annotated relations into an ordinary query over the composite encoding: one extra column carries the annotation, of the lifted value type T ⊕ K. With the three-kind discipline the rewriting is expressible natively: the annotation column is marked prov (ColKind.rewKinds), read back by TermG.provIndex terms, aggregated by AggQuery.ProvSum (the ⊕-gate creation of ε and ∖), and the value-kind bookkeeping is AggQuery.Retag – semantically the identity.

AggQuery.rewriting below mirrors the classical Query.rewriting rule for rule on the classical fragment (AggQuery.classical) of the general syntax. Its correctness against evaluateAnnotated is assembled in stages: faithfulness of the classical strip, the classical correctness theorem Query.rewriting_valid, and the plain-semantics agreement of the two rewritten queries.

The target kind vector #

source
def ColKind.rewKinds (n : ℕ) :
Fin (n + 1) → ColKind

The kind vector of a rewritten query: n data columns followed by the provenance column.

Equations
Instances For
    Dependency graph
    source
    theorem ColKind.rewKinds_lt {n : ℕ} {k : Fin (n + 1)} (h : ↑k < n) :
    rewKinds n k = reg
    Dependency graph
    source
    theorem ColKind.rewKinds_of_not_lt {n : ℕ} {k : Fin (n + 1)} (h : ¬↑k < n) :
    rewKinds n k = prov
    Dependency graph
    source
    theorem ColKind.rewKinds_base {n : ℕ} (k : Fin (n + 1)) :
    (rewKinds n k).base = reg
    Dependency graph
    source
    def AggQuery.retagToRew {T' : Type} {n : ℕ} {κ : Fin (n + 1) → ColKind} (h : ∀ (k : Fin (n + 1)), (κ k).base = ColKind.reg) (q : AggQuery T' (n + 1) κ) :
    AggQuery T' (n + 1) (ColKind.rewKinds n)

    Retag any pointwise value-kinded query to the rewriting kinds.

    Equations
    Instances For
      Dependency graph

      The classical fragment #

      source
      def AggQuery.classical {T : Type} {n : ℕ} {κ : Fin n → ColKind} :
      AggQuery T n κ → Prop

      The classical (R1)–(R4) source fragment of the general syntax: no grouping, no provenance aggregation, no retagging, projections through regular terms only, selections without aggregate atoms.

      Equations
      Instances For
        Dependency graph
        source
        theorem AggQuery.classical_kinds {T : Type} {n : ℕ} {κ : Fin n → ColKind} (q : AggQuery T n κ) :
        q.classical → ∀ (k : Fin n), κ k = ColKind.reg

        Classical queries have all-regular kinds (pointwise).

        Dependency graph

        Casting terms, predicates and columns to the composite domain #

        source
        def TermG.castComposite {T : Type} [ValueType T] {K : Type} {n : ℕ} {κ : Fin n → ColKind} (hκ : ∀ (k : Fin n), κ k = ColKind.reg) :
        TermG T κ → TermG (T ⊕ K) (ColKind.rewKinds n)

        A term over all-regular columns, over the composite domain with its columns shifted into the data block of the rewritten schema.

        Equations
        Instances For
          Dependency graph
          source
          def GenPred.castComposite {T : Type} [ValueType T] {K : Type} {n : ℕ} {κ : Fin n → ColKind} (hκ : ∀ (k : Fin n), κ k = ColKind.reg) (φ : GenPred T κ) :
          φ.hasAggAtom = false → GenPred (T ⊕ K) (ColKind.rewKinds n)

          An aggregate-atom-free predicate, over the composite domain.

          Equations
          Instances For
            Dependency graph
            source
            def ProjCol.castComposite {T : Type} [ValueType T] {K : Type} {n : ℕ} {κ : Fin n → ColKind} (hκ : ∀ (k : Fin n), κ k = ColKind.reg) (p : ProjCol T κ) :
            p.kind = ColKind.reg → ProjCol (T ⊕ K) (ColKind.rewKinds n)

            A regular projection column, over the composite domain.

            Equations
            Instances For
              Dependency graph
              source
              theorem TermG.castComposite_chiFree {T : Type} [ValueType T] {K : Type} {n : ℕ} {κ : Fin n → ColKind} (hκ : ∀ (k : Fin n), κ k = ColKind.reg) (t : TermG T κ) :
              (castComposite hκ t).chiFree

              The composite cast emits no indicator gate: a source gate, whose generic semantics is the junk constant, casts to that constant.

              Dependency graph
              source
              theorem GenPred.castComposite_chiFree {T : Type} [ValueType T] {K : Type} {n : ℕ} {κ : Fin n → ColKind} (hκ : ∀ (k : Fin n), κ k = ColKind.reg) (φ : GenPred T κ) (hφ : φ.hasAggAtom = false) :
              (castComposite hκ φ hφ).chiFree

              The composite cast of a predicate emits no indicator gate.

              Dependency graph
              source
              theorem ProjCol.castComposite_chiFree {T : Type} [ValueType T] {K : Type} {n : ℕ} {κ : Fin n → ColKind} (hκ : ∀ (k : Fin n), κ k = ColKind.reg) (p : ProjCol T κ) (hp : p.kind = ColKind.reg) :
              (castComposite hκ p hp).chiFree

              The composite cast of a projection column emits no indicator gate.

              Dependency graph
              source
              theorem ProjCol.castComposite_kind {T : Type} [ValueType T] {K : Type} {n : ℕ} {κ : Fin n → ColKind} (hκ : ∀ (k : Fin n), κ k = ColKind.reg) (p : ProjCol T κ) (hp : p.kind = ColKind.reg) :
              (castComposite hκ p hp).kind = ColKind.reg
              Dependency graph

              Join conditions on key columns #

              source
              def keyJoinCond {T' : Type} [Zero T'] {n m : ℕ} {κ : Fin m → ColKind} (posL posR : Fin n → Fin m) (hL : ∀ (k : Fin n), κ (posL k) = ColKind.reg) (hR : ∀ (k : Fin n), κ (posR k) = ColKind.reg) :
              GenPred T' κ

              The conjunction of equalities between two blocks of regular columns (the join condition of the Diff rewriting).

              Equations
              • One or more equations did not get rendered due to their size.
              Instances For
                Dependency graph
                source
                theorem keyJoinCond_chiFree {T' : Type} [Zero T'] {n m : ℕ} {κ : Fin m → ColKind} (posL posR : Fin n → Fin m) (hL : ∀ (k : Fin n), κ (posL k) = ColKind.reg) (hR : ∀ (k : Fin n), κ (posR k) = ColKind.reg) :
                (keyJoinCond posL posR hL hR).chiFree

                The join condition is a conjunction of column equalities: no indicator gate.

                Dependency graph

                The rewriting #

                source
                def AggQuery.rewriting {T : Type} [ValueType T] {K : Type} [CommSemiringWithMonus K] [HasAltLinearOrder K] {n : ℕ} {κ : Fin n → ColKind} (q : AggQuery T n κ) :
                q.classical → AggQuery (T ⊕ K) (n + 1) (ColKind.rewKinds n)

                The (R1)–(R4) rewriting, natively on the general syntax. Each rule mirrors the classical Query.rewriting: the base relation exposes its provenance column (R1), projections keep it verbatim (R2, key case), selections filter the data columns (R2), joins multiply the two provenance columns (R3), unions concatenate (R4, first case), deduplication ⊕-sums the provenance per surviving tuple (R4, ε), and difference combines the unmatched branch with the matched branch's α ⊖ Σβ (R4, ∖).

                Equations
                Instances For
                  Dependency graph

                  Stripping to the classical syntax #

                  The classical fragment of the general syntax maps back to the classical Query syntax; the correctness of the native rewriting is assembled through this strip, the classical correctness theorem, and the plain-semantics agreement of the two rewritten queries.

                  source
                  def TermG.strip {T : Type} [ValueType T] {n : ℕ} {κ : Fin n → ColKind} :
                  TermG T κ → Term T n

                  Strip a term over regular columns to a classical term (the provIndex arm is unreachable on the classical fragment and mapped harmlessly).

                  Equations
                  Instances For
                    Dependency graph
                    source
                    theorem TermG.strip_eval {T : Type} [ValueType T] {n : ℕ} {κ : Fin n → ColKind} (t : TermG T κ) (u : Tuple T n) :
                    t.strip.eval u = t.evalPlain u

                    Plain evaluation factors through the strip.

                    Dependency graph
                    source
                    def GenPred.strip {T : Type} [ValueType T] {n : ℕ} {κ : Fin n → ColKind} :
                    GenPred T κ → Selection T n

                    Strip an aggregate-atom-free predicate to a classical selection.

                    Equations
                    Instances For
                      Dependency graph
                      source
                      theorem GenPred.strip_eval {T : Type} [ValueType T] {n : ℕ} {κ : Fin n → ColKind} (φ : GenPred T κ) :
                      φ.hasAggAtom = false → ∀ (u : Tuple T n), φ.strip.eval u ↔ φ.holdsPlain u

                      Classical truth factors through the strip, on aggregate-atom-free predicates.

                      Dependency graph
                      source
                      def ProjCol.strip {T : Type} [ValueType T] {n : ℕ} {κ : Fin n → ColKind} :
                      ProjCol T κ → Term T n

                      Strip a regular projection column to a classical term.

                      Equations
                      Instances For
                        Dependency graph
                        source
                        def AggQuery.strip {T : Type} [ValueType T] {n : ℕ} {κ : Fin n → ColKind} (q : AggQuery T n κ) :
                        q.classical → Query T n

                        Strip a classical-fragment query to the classical syntax.

                        Equations
                        Instances For
                          Dependency graph
                          source
                          theorem AggQuery.strip_source {T : Type} [ValueType T] {n : ℕ} {κ : Fin n → ColKind} (q : AggQuery T n κ) (hq : q.classical) :
                          (q.strip hq).source

                          The strip is aggregation-free.

                          Dependency graph

                          Faithfulness of the strip #

                          source
                          theorem GenRow.Inv.plainTuple_eq {T K : Type} [CommSemiringWithMonus K] {n : ℕ} {r : GenRow T K n} {p : AnnotatedTuple T K n} (h : r.Inv p) :
                          plainTuple r.1 = p.1

                          The collapsed data part of an invariant row is its classical counterpart's data part.

                          Dependency graph
                          source
                          theorem AggQuery.strip_rel {T : Type} [ValueType T] {K : Type} [CommSemiringWithMonus K] [DecidableEq K] [HasAltLinearOrder K] {n : ℕ} {κ : Fin n → ColKind} (q : AggQuery T n κ) (hq : q.classical) (d : AnnotatedDatabase T K) :
                          Multiset.Rel GenRow.Inv (q.evaluate d) ((q.strip hq).evaluateAnnotated ⋯ d)

                          Row-wise faithfulness of the strip: on the classical fragment, the general evaluator produces rows satisfying the embedding invariant against the classical annotated evaluation of the stripped query.

                          Dependency graph
                          source
                          theorem AggQuery.strip_bridge {T : Type} [ValueType T] {K : Type} [CommSemiringWithMonus K] [DecidableEq K] [HasAltLinearOrder K] {n : ℕ} {κ : Fin n → ColKind} (q : AggQuery T n κ) (hq : q.classical) (d : AnnotatedDatabase T K) :
                          q.evaluateAnnotated d = (q.strip hq).evaluateAnnotated ⋯ d

                          Faithfulness of the strip: on the classical fragment the general annotated evaluator computes the classical annotated semantics of the stripped query.

                          Dependency graph

                          Plain-semantics agreement of the two rewritten queries #

                          source
                          theorem TermG.castComposite_evalPlain {T : Type} [ValueType T] {K : Type} [CommSemiringWithMonus K] [HasAltLinearOrder K] {n : ℕ} {κ : Fin n → ColKind} (hκ : ∀ (k : Fin n), κ k = ColKind.reg) (t : TermG T κ) (u : Tuple (T ⊕ K) (n + 1)) :
                          (castComposite hκ t).evalPlain u = t.strip.castToAnnotatedTuple.eval u

                          The composite cast of a term agrees with the classical cast of its strip.

                          Dependency graph
                          source
                          theorem GenPred.castComposite_holdsPlain {T : Type} [ValueType T] {K : Type} [CommSemiringWithMonus K] [HasAltLinearOrder K] {n : ℕ} {κ : Fin n → ColKind} (hκ : ∀ (k : Fin n), κ k = ColKind.reg) (φ : GenPred T κ) (hφ : φ.hasAggAtom = false) (u : Tuple (T ⊕ K) (n + 1)) :
                          (castComposite hκ φ hφ).holdsPlain u ↔ φ.strip.castToAnnotatedTuple.eval u

                          The composite cast of a predicate agrees with the classical cast of its strip.

                          Dependency graph
                          source
                          theorem ProjCol.castComposite_evalPlain {T : Type} [ValueType T] {K : Type} [CommSemiringWithMonus K] [HasAltLinearOrder K] {n : ℕ} {κ : Fin n → ColKind} (hκ : ∀ (k : Fin n), κ k = ColKind.reg) (p : ProjCol T κ) (hp : p.kind = ColKind.reg) (u : Tuple (T ⊕ K) (n + 1)) :
                          (castComposite hκ p hp).evalPlain u = p.strip.castToAnnotatedTuple.eval u

                          The composite cast of a projection column agrees with the classical cast of its strip.

                          Dependency graph
                          source
                          theorem Relation.cast_filter {T' : Type} {n m : ℕ} (hn : n = m) (p : Tuple T' m → Prop) [DecidablePred p] (r : Relation T' n) :
                          Multiset.filter p (cast hn r) = cast hn (Multiset.filter (fun (t : Tuple T' n) => p (Tuple.cast hn t)) r)
                          Dependency graph
                          source
                          theorem GenPred.holdsPlain_foldr_and {T' : Type} [ValueType T'] {N : ℕ} {κ' : Fin N → ColKind} {α : Type} (l : List α) (f : α → GenPred T' κ') (base : GenPred T' κ') (u : Tuple T' N) :
                          (List.foldr and base (List.map f l)).holdsPlain u ↔ (∀ x ∈ l, (f x).holdsPlain u) ∧ base.holdsPlain u
                          Dependency graph
                          source
                          theorem keyJoinCond_holdsPlain {T' : Type} [ValueType T'] {n m : ℕ} {κ' : Fin m → ColKind} (posL posR : Fin n → Fin m) (hL : ∀ (k : Fin n), κ' (posL k) = ColKind.reg) (hR : ∀ (k : Fin n), κ' (posR k) = ColKind.reg) (u : Tuple T' m) :
                          (keyJoinCond posL posR hL hR).holdsPlain u ↔ ∀ (k : Fin n), u (posL k) = u (posR k)
                          Dependency graph
                          source
                          theorem Tuple.cast_coord {T' : Type} {n m : ℕ} (heq : n = m) (t : Tuple T' n) (k : Fin m) :
                          cast heq t k = t ⟨↑k, ⋯⟩
                          Dependency graph
                          source
                          theorem AggQuery.rewriting_plain {T : Type} [ValueType T] {K : Type} [CommSemiringWithMonus K] [DecidableEq K] [HasAltLinearOrder K] {n : ℕ} {κ : Fin n → ColKind} (q : AggQuery T n κ) (hq : q.classical) (D : Database (T ⊕ K)) :
                          (q.rewriting hq).evaluatePlain D = ((q.strip hq).rewriting ⋯).evaluate D

                          Plain-semantics agreement: the native rewriting and the classical rewriting of the stripped query evaluate identically on any composite database.

                          Dependency graph

                          Rewriting correctness #

                          source
                          theorem AggQuery.rewriting_valid {T : Type} [ValueType T] {K : Type} [CommSemiringWithMonus K] [DecidableEq K] [HasAltLinearOrder K] {n : ℕ} {κ : Fin n → ColKind} (q : AggQuery T n κ) (hq : q.classical) (d : AnnotatedDatabase T K) :
                          (q.evaluateAnnotated d).toComposite = (q.rewriting hq).evaluatePlain d.toComposite

                          Correctness of the native rewriting. For a classical query in the general syntax, evaluating the annotated semantics and folding the result into composite T ⊕ K tuples agrees with evaluating the rewritten query under the plain semantics over the composite database. This is the general-syntax form of the classical rewriting correctness.

                          Dependency graph