Documentation

Provenance.QueryToAgg

Embedding the classical query syntax into the general evaluator #

Query.toAgg embeds a non-aggregating classical query into the kind-indexed general syntax AggQuery, over all-regular kinds: terms, selection predicates and every operator translate one to one. Query.toAgg_bridge proves the embedding faithful – the general evaluator computes the classical annotated semantics – via a row-wise invariant GenRow.Inv (regular data, finalized annotation) that absorbs the bookkeeping differences of the factored annotations (a pending multiset that stays empty, bases multiplied by empty products).

On top of the embedding, Query.toAggHaving_input reads the input relation of a general HAVING site over an embedded subquery off the classical query's annotated semantics, which is what the query-level HAVING correctness results consume.

This module sits below the classical HAVING correctness files (Provenance.HavingQueryCorrectness, Provenance.HavingJoinCompositional) so that they can state their theorems over the embedded general query directly, with no side hypothesis. The compositional JOIN rewriting built on top of the embedding lives in Provenance.AggQueryEmbedding.

Terms and selections over all-regular kinds #

source
def Term.toGenReg {T : Type} {n : ℕ} :
Term T n → TermG T (ColKind.allReg n)

A classical term, as a term over all-regular columns.

Equations
Instances For
    Dependency graph
    source
    theorem Term.toGenReg_eval {T : Type} [ValueType T] {K : Type} {n : ℕ} (t : Term T n) (x : Tuple T n) :
    (t.toGenReg.eval fun (k : Fin n) => Sum.inl (x k)) = t.eval x

    The embedded term evaluates on a regular-values row as the original term on the underlying tuple.

    Dependency graph
    source
    def BoolTerm.toGenPred {T : Type} {n : ℕ} :
    BoolTerm T n → GenPred T (ColKind.allReg n)

    A comparison atom, as a generalized regular atom.

    Equations
    Instances For
      Dependency graph
      source
      def Selection.toGenPred {T : Type} [ValueType T] {n : ℕ} :
      Selection T n → GenPred T (ColKind.allReg n)

      A classical selection predicate, as a generalized predicate without aggregate atoms (Selection.True becomes the tautology 𝟘 = 𝟘).

      Equations
      Instances For
        Dependency graph
        source
        theorem Selection.toGenPred_hasAggAtom {T : Type} [ValueType T] {n : ℕ} (φ : Selection T n) :
        φ.toGenPred.hasAggAtom = false

        Embedded selections have no aggregate atoms: the evaluator filters classically.

        Dependency graph
        source
        theorem Selection.toGenPred_holds {T : Type} [ValueType T] {K : Type} {n : ℕ} (φ : Selection T n) (x : Tuple T n) :
        (φ.toGenPred.holds fun (k : Fin n) => Sum.inl (x k)) ↔ φ.eval x

        The embedded predicate holds on a regular-values row exactly when the original selection accepts the underlying tuple.

        Dependency graph

        The embedding #

        source
        theorem ColKind.allReg_append (n₁ n₂ : ℕ) :
        Fin.append (allReg n₁) (allReg n₂) = allReg (n₁ + n₂)

        Appending all-regular kind vectors.

        Dependency graph
        source
        def Query.toAgg {T : Type} [ValueType T] {n : ℕ} (q : Query T n) :
        q.source → AggQuery T n (ColKind.allReg n)

        The embedding of the non-aggregating fragment: every classical operator translates to its general counterpart, over all-regular kinds.

        Equations
        Instances For
          Dependency graph

          Faithfulness #

          source
          def GenRow.Inv {T K : Type} [CommSemiringWithMonus K] {n : ℕ} (r : GenRow T K n) (p : AnnotatedTuple T K n) :
          Prop

          The row invariant of the embedding: regular data over the classical tuple, a factored annotation finalizing to the classical one, and no pending group factors (the embedding image contains no Gamma).

          Equations
          Instances For
            Dependency graph
            source
            theorem GenRow.Inv.toAnnotated_eq {T K : Type} [CommSemiringWithMonus K] {n : ℕ} {r : GenRow T K n} {p : AnnotatedTuple T K n} (h : r.Inv p) :
            r.toAnnotated = p

            Invariant rows finalize to their classical counterparts.

            Dependency graph
            source
            theorem rel_inv_ofAnnotated {T K : Type} [CommSemiringWithMonus K] {n : ℕ} (X : AnnotatedRelation T K n) :
            Multiset.Rel GenRow.Inv (Multiset.map GenRow.ofAnnotated X) X

            Embedded classical rows satisfy the invariant.

            Dependency graph
            source
            theorem Query.toAgg_rel {T : Type} [ValueType T] {K : Type} [CommSemiringWithMonus K] [DecidableEq K] [HasAltLinearOrder K] {n : ℕ} (q : Query T n) (hq : q.source) (d : AnnotatedDatabase T K) :
            Multiset.Rel GenRow.Inv ((q.toAgg hq).evaluate d) (q.evaluateAnnotated hq d)

            Faithfulness of the embedding, row for row: the general evaluator on the embedded query produces rows satisfying the invariant against the classical annotated evaluation.

            Dependency graph
            source
            theorem Query.toAgg_bridge {T : Type} [ValueType T] {K : Type} [CommSemiringWithMonus K] [DecidableEq K] [HasAltLinearOrder K] {n : ℕ} (q : Query T n) (hq : q.source) (d : AnnotatedDatabase T K) :
            (q.toAgg hq).evaluateAnnotated d = q.evaluateAnnotated hq d

            Faithfulness of the embedding: the general evaluator computes the classical annotated semantics on embedded queries.

            Dependency graph
            source
            theorem GenRow.Inv.row_eq {T K : Type} [CommSemiringWithMonus K] {n : ℕ} {r : GenRow T K n} {p : AnnotatedTuple T K n} (h : r.Inv p) :
            r = ofAnnotated p

            An invariant row is the embedding of its classical counterpart: the pending multiset is empty, so the base coincides with the finalized annotation.

            Dependency graph
            source
            theorem Query.toAgg_evaluate_eq {T : Type} [ValueType T] {K : Type} [CommSemiringWithMonus K] [DecidableEq K] [HasAltLinearOrder K] {n : ℕ} (q : Query T n) (hq : q.source) (d : AnnotatedDatabase T K) :
            (q.toAgg hq).evaluate d = Multiset.map GenRow.ofAnnotated (q.evaluateAnnotated hq d)

            The embedding at the row level: the general evaluator on an embedded query produces exactly the embedded classical rows.

            Dependency graph

            The fused HAVING, in context #

            source
            theorem Query.toAggHaving_input {T : Type} [ValueType T] {K : Type} [CommSemiringWithMonus K] [DecidableEq K] [HasAltLinearOrder K] {m : ℕ} (q : Query T m) (hq : q.source) (d : AnnotatedDatabase T K) :
            (q.toAgg hq).evaluateAnnotated d = q.evaluateAnnotated hq d

            The fused HAVING site over an embedded subquery: its input relation is the classical subquery's annotated evaluation, so the closed form AggQuery.havingSite_evaluateAnnotated specializes to the classical setting with no side hypothesis.

            Dependency graph