Documentation

Provenance.AggQueryBridges

Regression bridges for the general evaluator #

The fused HAVING operator is recovered from the decomposed general syntax: on its fragment – one aggregate comparison directly above the grouping – the general evaluator σ_ψ ∘ Gamma computes exactly the fused semantics in closed form (AggQuery.havingSite_evaluateAnnotated). Row by row, the pending group factor introduced by Gamma is superseded by the predicate provenance of the comparison (the token's predProv, which is the fused Having.havingProv by AggValue.predProv_ofGroup), and the data part collapses to the whole-group aggregate values.

Every theorem about the fused semantics – the possible-world collapses of Provenance.HavingSemantics, the query-level correctness results – is therefore stated directly against the general evaluator, with this closed form as the working lemma; no separate fused evaluator is needed. The kind transport AggQuery.castKind is transparent to evaluation (AggQuery.evaluate_castKind).

source
theorem AggQuery.evaluate_castKind {T : Type} [ValueType T] {K : Type} [CommSemiringWithMonus K] [DecidableEq K] [HasAltLinearOrder K] {n : ℕ} {κ κ' : Fin n → ColKind} (h : κ = κ') (q : AggQuery T n κ) (d : AnnotatedDatabase T K) :
(castKind h q).evaluate d = q.evaluate d

Kind transport is transparent to evaluation (row types do not mention the kind vector).

Dependency graph
source
@[reducible, inline]
abbrev ColKind.gammaKinds (n₁ n₂ : ℕ) :
Fin (n₁ + n₂) → ColKind

The kind vector of a Gamma output: key columns then token columns.

Equations
Instances For
    Dependency graph
    source
    def Term.toGenKey {T : Type} {n₁ : ℕ} (n₂ : ℕ) :
    Term T n₁ → TermG T (ColKind.gammaKinds n₁ n₂)

    A term over the group key, embedded as a term over the key columns of a Gamma output.

    Equations
    Instances For
      Dependency graph
      source
      theorem Term.toGenKey_eval {T : Type} [ValueType T] {K : Type} {n₁ n₂ : ℕ} (s : Term T n₁) (g : Tuple T n₁) (h : Fin n₂ → AggValue T K) :
      (toGenKey n₂ s).eval (Fin.append (fun (k : Fin n₁) => Sum.inl (g k)) fun (j : Fin n₂) => Sum.inr (h j)) = s.eval g

      The embedded key term evaluates on a Gamma output row as the original term on the group key.

      Dependency graph
      source
      theorem AggValue.annList_ofGroup {T : Type} [ValueType T] {K : Type} {m : ℕ} (f : SeqAggFunc T) (t : Term T m) (U : List (AnnotatedTuple T K m)) :
      List.map Prod.snd (ofGroup f t U).occs = List.map Prod.snd U

      The annotation list of a group token is the group's annotation list.

      Dependency graph
      source
      def GenPred.fusedCmp {T : Type} {n₁ n₂ : ℕ} (op : CompOp) (l : Fin n₂) (s : Term T n₁) :
      GenPred T (ColKind.gammaKinds n₁ n₂)

      The fused aggregate comparison, as a generalized selection atom on a Gamma output: the l-th token column compared against a term over the group key.

      Equations
      Instances For
        Dependency graph
        source
        @[reducible, inline]
        abbrev AggQuery.havingSite {T : Type} {m n₁ n₂ : ℕ} (is : Tuple (Fin m) n₁) (ts : Tuple (Term T m) n₂) (fs : Tuple (SeqAggFunc T) n₂) (op : CompOp) (l : Fin n₂) (s : Term T n₁) (qg : AggQuery T m (ColKind.allReg m)) :
        AggQuery T (n₁ + n₂) (ColKind.gammaKinds n₁ n₂)

        The fused HAVING site as a general query: one aggregate comparison directly above the grouping.

        Equations
        Instances For
          Dependency graph
          source
          theorem AggQuery.havingSite_evaluateAnnotated {T : Type} [ValueType T] {K : Type} [CommSemiringWithMonus K] [DecidableEq K] [HasAltLinearOrder K] {m n₁ n₂ : ℕ} (is : Tuple (Fin m) n₁) (ts : Tuple (Term T m) n₂) (fs : Tuple (SeqAggFunc T) n₂) (op : CompOp) (l : Fin n₂) (s : Term T n₁) (qg : AggQuery T m (ColKind.allReg m)) (d : AnnotatedDatabase T K) :
          (havingSite is ts fs op l s qg).evaluateAnnotated d = Multiset.map (fun (g : Fin n₁ → T) => (Fin.append g fun (k : Fin n₂) => fs k (List.map (fun (p : AnnotatedTuple T K m) => (ts k).eval p.1) (Having.havingGroup is (qg.evaluateAnnotated d) g)), Having.havingProv (Having.havingGroup is (qg.evaluateAnnotated d) g) (ts l) (fs l) op (s.eval g))) (Multiset.map (fun (p : AnnotatedTuple T K m) (k : Fin n₁) => p.1 (is k)) (qg.evaluateAnnotated d)).dedup

          Closed form of the fused HAVING site. On its fragment – one aggregate comparison directly above the grouping – the general evaluator produces one row per group key of the subquery, carrying the key followed by the whole-group aggregate values and annotated by the predicate provenance Having.havingProv of the group's occurrence sequence. This is what makes the fused site a theorem rather than a semantics of its own: the pending group factor introduced by Gamma is superseded by the comparison's predicate provenance, and the data part collapses to the whole-group aggregate values.

          Dependency graph