Documentation

Provenance.AggQueryHavingRewriting

The rewritten world's evaluator: tokens as ordinary column values #

ProvSQL evaluates rewritten plans over a value universe that contains, next to the regular values and the provenance identifiers, the aggregate tokens produced by its provsql_agg gate; the provsql_having gate then reads a token and produces the predicate provenance of an aggregate comparison. The formal counterpart is the evaluator AggQuery.evaluateRew defined here: it runs a rewritten query (a AggQuery over the composite value type T ⊕ K) over rows Tuple (GenValue (T ⊕ K) K) n – the lifted-column carrier of the general evaluator, instantiated at the composite value type – with the kind vector saying which columns hold tokens.

On the value-kinded operators the evaluator is the plain semantics through the inl embedding (Dedup, Diff and Gamma collapse their statically all-regular rows to plain tuples, exactly as the general evaluator reads them through GenRow.toAnnotated).
AggQuery.GammaTok builds tokens: one AggValue.ofGroup per (term, aggregate) pair over the group's occurrence sequence, whose annotations are the values of the explicit annotation term – in rewritten plans, the provenance column of the subquery – and writes the group-existence guard δ(⊕ occs) into its prov output column.
TermG.cmpAgg is the cmp gate: TermG.evalRew interprets it by AggValue.predProv, the primitive the rewriting's correctness is stated against, faithfully to ProvSQL's own gate-relative correctness.
TermG.chiGate is the indicator gate a HAVING predicate needs for its regular atoms: TermG.evalRew interprets it by Having.chi, the characteristic value predsem gives such an atom. Having no kind constraint to keep it off plain columns, it is what AggQuery.chiFree excludes below.

The rewriting rules built on this evaluator live downstream: Provenance.AggQueryGroupRewriting (the bare grouping and the HAVING site) and Provenance.AggQueryClosure (the compositional closure).

Terms and predicates in the rewritten world #

def Sum.annPart {T K : Type} [CommSemiringWithMonus K] :

T ⊕ K → K

The annotation part of a composite value (𝟘 on data values: a malformed provenance read carries no worlds).

Equations

(Sum.inl val).annPart = 0
(Sum.inr k).annPart = k

Instances For

Dependency graph

def TermG.evalRew {T : Type} [ValueType T] {K : Type} [CommSemiringWithMonus K] [DecidableEq K] [HasAltLinearOrder K] {n : ℕ} {κ : Fin n → ColKind} :

TermG (T ⊕ K) κ → Tuple (GenValue (T ⊕ K) K) n → T ⊕ K

Term evaluation in the rewritten world: as TermG.eval on the value-reading constructors, with the cmpAgg gate interpreted by the predicate provenance of the token against the comparison term, and the chiGate gate by the characteristic value of its comparison.

Equations

(TermG.const a).evalRew x✝ = a
(TermG.index k a).evalRew x✝ = AggValue.collapseSum (x✝ k)
(TermG.provIndex k a).evalRew x✝ = AggValue.collapseSum (x✝ k)
(TermG.cmpAgg k a op c).evalRew x✝ = match x✝ k with | Sum.inl val => Sum.inr 0 | Sum.inr a => Sum.inr (a.predProv op (c.evalRew x✝))
(TermG.chiGate op t₁ t₂).evalRew x✝ = Sum.inr (Having.chi op (t₁.evalRew x✝) (t₂.evalRew x✝))
(t₁.add t₂).evalRew x✝ = t₁.evalRew x✝ + t₂.evalRew x✝
(t₁.sub t₂).evalRew x✝ = t₁.evalRew x✝ - t₂.evalRew x✝
(t₁.mul t₂).evalRew x✝ = t₁.evalRew x✝ * t₂.evalRew x✝

Instances For

Dependency graph

def ProjCol.evalRew {T : Type} [ValueType T] {K : Type} [CommSemiringWithMonus K] [DecidableEq K] [HasAltLinearOrder K] {n : ℕ} {κ : Fin n → ColKind} (p : ProjCol (T ⊕ K) κ) (u : Tuple (GenValue (T ⊕ K) K) n) :

GenValue (T ⊕ K) K

Projection-column evaluation in the rewritten world.

Equations

(ProjCol.term t).evalRew u = Sum.inl (t.evalRew u)
(ProjCol.token k a).evalRew u = u k
(ProjCol.provTerm t).evalRew u = Sum.inl (t.evalRew u)

Instances For

Dependency graph

def GenPred.holdsRew {T : Type} [ValueType T] {K : Type} [CommSemiringWithMonus K] [DecidableEq K] [HasAltLinearOrder K] {n : ℕ} {κ : Fin n → ColKind} :

GenPred (T ⊕ K) κ → Tuple (GenValue (T ⊕ K) K) n → Prop

Classical truth of a predicate in the rewritten world (compared tokens read through their deterministic collapse, as in GenPred.holds).

Equations

(GenPred.cmp op t₁ t₂).holdsRew x✝ = op.eval (t₁.evalRew x✝) (t₂.evalRew x✝)
(GenPred.aggCmp k a op t).holdsRew x✝ = op.eval (AggValue.collapseSum (x✝ k)) (t.evalRew x✝)
(φ.and ψ).holdsRew x✝ = (φ.holdsRew x✝ ∧ ψ.holdsRew x✝)
(φ.or ψ).holdsRew x✝ = (φ.holdsRew x✝ ∨ ψ.holdsRew x✝)
φ.not.holdsRew x✝ = ¬φ.holdsRew x✝

Instances For

Dependency graph

def GenPred.decHoldsRew {T : Type} [ValueType T] {K : Type} [CommSemiringWithMonus K] [DecidableEq K] [HasAltLinearOrder K] {n : ℕ} {κ : Fin n → ColKind} (φ : GenPred (T ⊕ K) κ) (u : Tuple (GenValue (T ⊕ K) K) n) :

Decidable (φ.holdsRew u)

Structural decidability of holdsRew.

Equations

(GenPred.cmp op a a_1).decHoldsRew u = GenPred.decHoldsRew._aux_1 u op a a_1
(GenPred.aggCmp k a op a_1).decHoldsRew u = GenPred.decHoldsRew._aux_3 u k a op a_1
(φ_2.and ψ).decHoldsRew u = instDecidableAnd
(φ_2.or ψ).decHoldsRew u = instDecidableOr
φ_2.not.decHoldsRew u = instDecidableNot

Instances For

Dependency graph

@[instance_reducible]

instance GenPred.instDecidableHoldsRew {T : Type} [ValueType T] {K : Type} [CommSemiringWithMonus K] [DecidableEq K] [HasAltLinearOrder K] {n : ℕ} {κ : Fin n → ColKind} (φ : GenPred (T ⊕ K) κ) :

DecidablePred φ.holdsRew

Equations

φ.instDecidableHoldsRew u = φ.decHoldsRew u

Dependency graph

The evaluator #

def AggQuery.evaluateRew {T : Type} [ValueType T] {K : Type} [CommSemiringWithMonus K] [DecidableEq K] [HasAltLinearOrder K] {n : ℕ} {κ : Fin n → ColKind} :

AggQuery (T ⊕ K) n κ → Database (T ⊕ K) → Multiset (Tuple (GenValue (T ⊕ K) K) n)

The rewritten world's evaluator: plain multiset semantics over token-bearing rows. Value-kinded operators act through the inl embedding; GammaTok builds tokens and the group guard; the gates inside terms are interpreted by predProv and Having.chi.

Equations

One or more equations did not get rendered due to their size.
(AggQuery.Rel x✝¹ s).evaluateRew x✝ = match Database.find x✝¹ s x✝ with | none => 0 | some rn => Multiset.map (fun (t : Tuple (T ⊕ K) x✝¹) (k : Fin x✝¹) => Sum.inl (t k)) rn
(AggQuery.Proj ps q).evaluateRew x✝ = Multiset.map (fun (u : Tuple (GenValue (T ⊕ K) K) n_1) (j : Fin x✝¹) => (ps j).evalRew u) (q.evaluateRew x✝)
(AggQuery.Sel φ q).evaluateRew x✝ = Multiset.filter φ.holdsRew (q.evaluateRew x✝)
(q₁.Sum q₂).evaluateRew x✝ = q₁.evaluateRew x✝ + q₂.evaluateRew x✝
(AggQuery.Retag h q).evaluateRew x✝ = q.evaluateRew x✝

Instances For

Dependency graph

Agreement with the plain semantics off the gates #

def AggQuery.noGammaTok {T' : Type} {n : ℕ} {κ : Fin n → ColKind} :

AggQuery T' n κ → Prop

No token-building grouping: together with gate-freeness, this cuts out the fragment on which the rewritten world's evaluator is the plain semantics through the inl embedding.

Equations

(AggQuery.Rel x✝ a).noGammaTok = True
(AggQuery.Proj ps q).noGammaTok = q.noGammaTok
(AggQuery.Sel a q).noGammaTok = q.noGammaTok
(q₁.Prod q₂).noGammaTok = (q₁.noGammaTok ∧ q₂.noGammaTok)
(q₁.Sum q₂).noGammaTok = (q₁.noGammaTok ∧ q₂.noGammaTok)
q.Dedup.noGammaTok = q.noGammaTok
(q₁.Diff q₂).noGammaTok = (q₁.noGammaTok ∧ q₂.noGammaTok)
(AggQuery.Gamma is ts fs q).noGammaTok = q.noGammaTok
(AggQuery.ProvSum is his t q).noGammaTok = q.noGammaTok
(AggQuery.Retag h q).noGammaTok = q.noGammaTok
(AggQuery.GammaTok is his ts fs a a_1).noGammaTok = False

Instances For

Dependency graph

def AggQuery.chiFree {T' : Type} {n : ℕ} {κ : Fin n → ColKind} :

AggQuery T' n κ → Prop

No indicator gate anywhere in a query's terms and predicates.

Equations

(AggQuery.Rel x✝ a).chiFree = True
(AggQuery.Proj ps q).chiFree = ((∀ (j : Fin x✝), (ps j).chiFree) ∧ q.chiFree)
(AggQuery.Sel a q).chiFree = (a.chiFree ∧ q.chiFree)
(q₁.Prod q₂).chiFree = (q₁.chiFree ∧ q₂.chiFree)
(q₁.Sum q₂).chiFree = (q₁.chiFree ∧ q₂.chiFree)
q.Dedup.chiFree = q.chiFree
(q₁.Diff q₂).chiFree = (q₁.chiFree ∧ q₂.chiFree)
(AggQuery.Gamma is ts fs q).chiFree = q.chiFree
(AggQuery.ProvSum is his t q).chiFree = (t.chiFree ∧ q.chiFree)
(AggQuery.Retag h q).chiFree = q.chiFree
(AggQuery.GammaTok is his ts fs a a_1).chiFree = (a.chiFree ∧ a_1.chiFree)

Instances For

Dependency graph

theorem TermG.evalRew_inl {T : Type} [ValueType T] {K : Type} [CommSemiringWithMonus K] [DecidableEq K] [HasAltLinearOrder K] {n : ℕ} {κ : Fin n → ColKind} (t : TermG (T ⊕ K) κ) :

t.chiFree → ∀ (u : Tuple (T ⊕ K) n), (t.evalRew fun (k : Fin n) => Sum.inl (u k)) = t.evalPlain u

On inl-embedded rows a gate-free term evaluates in the rewritten world as its plain evaluation – including the cmpAgg gate, whose junk reading 𝟘 is definitionally the composite zero on a row with no token. The indicator gate has no such escape: it returns a genuine annotation, which is why it is excluded here.

Dependency graph

theorem ProjCol.evalRew_inl {T : Type} [ValueType T] {K : Type} [CommSemiringWithMonus K] [DecidableEq K] [HasAltLinearOrder K] {n : ℕ} {κ : Fin n → ColKind} (p : ProjCol (T ⊕ K) κ) (hp : p.chiFree) (u : Tuple (T ⊕ K) n) :

(p.evalRew fun (k : Fin n) => Sum.inl (u k)) = Sum.inl (p.evalPlain u)

Gate-free projection columns on inl-embedded rows evaluate to the embedded plain reading.

Dependency graph

theorem GenPred.holdsRew_inl {T : Type} [ValueType T] {K : Type} [CommSemiringWithMonus K] [DecidableEq K] [HasAltLinearOrder K] {n : ℕ} {κ : Fin n → ColKind} (φ : GenPred (T ⊕ K) κ) :

φ.chiFree → ∀ (u : Tuple (T ⊕ K) n), (φ.holdsRew fun (k : Fin n) => Sum.inl (u k)) ↔ φ.holdsPlain u

Gate-free predicates on inl-embedded rows hold as their plain reading.

Dependency graph

theorem Multiset.map_product_map {α : Type u_1} {β : Type u_2} {α' : Type u_3} {β' : Type u_4} (f : α → α') (g : β → β') (s : Multiset α) (t : Multiset β) :

(map f s).product (map g t) = map (Prod.map f g) (s.product t)

Maps push through the multiset product.

Dependency graph

theorem map_plainTuple_map_inl {T K : Type} {m : ℕ} (X : Multiset (Tuple (T ⊕ K) m)) :

Multiset.map (fun (u : Tuple (GenValue (T ⊕ K) K) m) => GenRow.plainTuple u) (Multiset.map (fun (t : Tuple (T ⊕ K) m) (k : Fin m) => Sum.inl (t k)) X) = X

Collapsing inl-embedded rows is the identity.

Dependency graph

theorem AggQuery.evaluateRew_plain {T : Type} [ValueType T] {K : Type} [CommSemiringWithMonus K] [DecidableEq K] [HasAltLinearOrder K] {n : ℕ} {κ : Fin n → ColKind} (q : AggQuery (T ⊕ K) n κ) (_hq : q.noGammaTok) (_hc : q.chiFree) (D : Database (T ⊕ K)) :

q.evaluateRew D = Multiset.map (fun (t : Tuple (T ⊕ K) n) (k : Fin n) => Sum.inl (t k)) (q.evaluatePlain D)

Plain agreement. Off the token-building operator, the rewritten world's evaluator is the plain semantics through the inl embedding.

Dependency graph

The fused predicate provenance under the composite embedding #

The rewritten site groups composite rows – the inl-embedded data with the annotation appended as the provenance column – while the annotated site groups the original annotated tuples. The fused predicate provenance is invariant under this embedding: comparisons restrict along inl, the lifted aggregate computes on the embedded values, and the occurrence annotations are read off unchanged.

def SeqAggFunc.liftComposite {T : Type} [ValueType T] {K : Type} (f : SeqAggFunc T) :

SeqAggFunc (T ⊕ K)

Lift a sequence aggregate to the composite domain (junk on the annotation arm, faithful on inl-embedded values).

Equations

f.liftComposite l = Sum.inl (f (List.map (Sum.elim id fun (x : K) => 0) l))

Instances For

Dependency graph

theorem SeqAggFunc.liftComposite_map_inl {T : Type} [ValueType T] {K : Type} (f : SeqAggFunc T) (l : List T) :

f.liftComposite (List.map Sum.inl l) = Sum.inl (f l)

The lifted aggregate on inl-embedded values.

Dependency graph

theorem CompOp.eval_inl {T : Type} [ValueType T] {K : Type} [CommSemiringWithMonus K] [HasAltLinearOrder K] (op : CompOp) (x y : T) :

op.eval (Sum.inl x) (Sum.inl y) ↔ op.eval x y

Comparison operators restrict along the inl embedding.

Dependency graph

theorem Having.chi_inl {T : Type} [ValueType T] {K : Type} [CommSemiringWithMonus K] [HasAltLinearOrder K] (op : CompOp) (x y : T) :

chi op (Sum.inl x) (Sum.inl y) = chi op x y

The comparison indicator restricts along the inl embedding.

Dependency graph

The classical rewriting stays off the token operators #

theorem AggQuery.rewriting_noGammaTok {T : Type} [ValueType T] {K : Type} [CommSemiringWithMonus K] [HasAltLinearOrder K] {n : ℕ} {κ : Fin n → ColKind} (q : AggQuery T n κ) (hq : q.classical) :

(q.rewriting hq).noGammaTok

The classical rewriting emits no token-building grouping.

Dependency graph

theorem AggQuery.rewriting_chiFree {T : Type} [ValueType T] {K : Type} [CommSemiringWithMonus K] [HasAltLinearOrder K] {n : ℕ} {κ : Fin n → ColKind} (q : AggQuery T n κ) (hq : q.classical) :

(q.rewriting hq).chiFree

The classical rewriting emits no indicator gate: its terms are column reads, their ⊗/⊖ combinations, and composite casts of the source terms – the gate is introduced only by the HAVING site.

Dependency graph

The group sequence under the composite embedding #

theorem AnnotatedTuple.toComposite_coord {T K : Type} {m : ℕ} (p : AnnotatedTuple T K m) (j : Fin (m + 1)) :

p.toComposite j = if h : ↑j < m then Sum.inl (p.1 ⟨↑j, h⟩) else Sum.inr p.2

Coordinates of the composite embedding of an annotated tuple.

Dependency graph

theorem Sum.inl_lt_inl_composite {T : Type} [ValueType T] {K : Type} [CommSemiringWithMonus K] [HasAltLinearOrder K] (x y : T) :

inl x < inl y ↔ x < y

The composite order restricts to the value order on inl.

Dependency graph

theorem Sum.inr_lt_inr_composite {T : Type} [ValueType T] {K : Type} [CommSemiringWithMonus K] [HasAltLinearOrder K] (x y : K) :

inr x < inr y ↔ x < y

The composite order restricts to the alternative order on inr.

Dependency graph

theorem Having.havingGroup_toComposite {T : Type} [ValueType T] {K : Type} [CommSemiringWithMonus K] [HasAltLinearOrder K] {m n₁ : ℕ} (is : Tuple (Fin m) n₁) (r : AnnotatedRelation T K m) (g : Tuple T n₁) :

(havingGroup (fun (k : Fin n₁) => Fin.castLE ⋯ (is k)) (Multiset.map (fun (p : AnnotatedTuple T K m) => (p.toComposite, p.2)) r) fun (k : Fin n₁) => Sum.inl (g k)) = List.map (fun (p : AnnotatedTuple T K m) => (p.toComposite, p.2)) (havingGroup is r g)

The group sequence under the composite embedding: embedding the relation and the key inl-wise embeds the group sequence. The embedding is monotone for the sort's tie-break order (data columns compare on the inl arm, the appended provenance column and the annotation both by the alternative order), and sorted lists of the same multiset are unique.

Dependency graph

Reading a rewritten evaluation back as an annotated relation #

theorem map_comp_fst_groupByKey {T : Type} [ValueType T] {K : Type} [CommSemiringWithMonus K] [DecidableEq K] [HasAltLinearOrder K] {n : ℕ} {β : Type} (G : Tuple (T ⊕ K) n → β) (Y : AnnotatedRelation (T ⊕ K) K n) :

Multiset.map (G ∘ Prod.fst) ↑↑(groupByKey Y) = Multiset.map G (Multiset.map Prod.fst Y).dedup

Mapping a key-only function over a grouped relation is mapping it over the deduplicated keys (the accumulated annotations are unread).

Dependency graph

theorem AggQuery.rewriting_provRel {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.map (fun (u : Tuple (GenValue (T ⊕ K) K) (n + 1)) => (GenRow.plainTuple u, ((TermG.provIndex (Fin.last n) ⋯).evalRew u).annPart)) ((q.rewriting hq).evaluateRew d.toComposite) = Multiset.map (fun (p : AnnotatedTuple T K n) => (p.toComposite, p.2)) ((q.strip hq).evaluateAnnotated ⋯ d)

The rewritten world reads back as an annotated relation. Pairing the collapsed data columns of the rewritten evaluation of a classical rewriting with the annotation read off its provenance column recovers the composite embedding of the classical annotated semantics – the input the token-building groupings of the rewritten world consume.

Dependency graph