Monotone HAVING conditions: absorptivity suffices

The join-based rewriting of a HAVING condition is correct in every absorptive commutative m-semiring – distributivity of ⊗ over ⊖ not required – as soon as the condition is monotone: a Boolean combination, by ∧ and ∨ only, of atoms whose validity is preserved when occurrences are added to the group. The atoms covered are COUNT(*) ≥ C, COUNT(*) > C (Query.joinCount_monotone_correct, Provenance.HavingQueryCorrectness), and the existential comparisons MIN(t) ≤ c, MIN(t) < c, MAX(t) ≥ c, MAX(t) > c, which hold in a world iff it contains a qualifying occurrence (Having.Existential).

• Existential atoms are rewritten as ε(Π_{#0}(σ_{t op c}(q))) (existentialQuery): per group key, the ⊕-sum of the annotations of the qualifying occurrences, which is the fused predicate provenance by Having.havingProv_existential (existential_perKey); padded, the rewriting is the key-projected fused site as a multiset (existential_site_rewrite, with the four instances minLe_site_rewrite, minLt_site_rewrite, maxGe_site_rewrite, maxGt_site_rewrite).

• Boolean closure. A conjunction is rewritten as the join of the two rewritings on the group key (keyJoin, which multiplies the per-key annotations, keyJoin_perKeySum) and a disjunction as their set union (keyUnion, which adds them, keyUnion_perKeySum): exactly how the fused semantics HavingPred.prov interprets ∧ and ∨. The syntax MonoCond of monotone conditions over the token columns of a grouping comes with its compositional rewriting MonoCond.rewrite, its reading MonoCond.toHavingPred as a Boolean combination of fused comparisons, and its reading MonoCond.toGenPred as a generalized selection predicate. MonoCond.site_evaluateAnnotated is the closed form of the fused site σ_ψ(γ_{#0}[ts : fs](q)) in the general evaluator, extending AggQuery.havingSite_evaluateAnnotated to positive combinations, and MonoCond.site_rewrite is the site substitution: the key-projected fused site and the padded rewriting are the same multiset of annotated tuples, in every absorptive commutative m-semiring.

The base query has the (key, value, identifier) schema of Provenance.HavingQueryCorrectness, with the group key in column #0.

Comparison atoms as selection predicates

def BoolTerm.ofCompOp {T : Type} {n : ℕ} (op : CompOp) (t s : Term T n) : BoolTerm T n

The Boolean term t op s.

Equations

• BoolTerm.ofCompOp CompOp.eq t s = BoolTerm.EQ t s
• BoolTerm.ofCompOp CompOp.ne t s = BoolTerm.NE t s
• BoolTerm.ofCompOp CompOp.lt t s = BoolTerm.LT t s
• BoolTerm.ofCompOp CompOp.le t s = BoolTerm.LE t s
• BoolTerm.ofCompOp CompOp.gt t s = BoolTerm.GT t s
• BoolTerm.ofCompOp CompOp.ge t s = BoolTerm.GE t s

theorem BoolTerm.ofCompOp_eval {T : Type} [ValueType T] {n : ℕ} (op : CompOp) (t s : Term T n) (u : Tuple T n) : (ofCompOp op t s).eval u ↔ op.eval (t.eval u) (s.eval u)

t op s holds on a tuple iff the comparison of the two values does.

Existential atoms: ε(Π_{#0}(σ_{t op c}(q)))

def atomSel (t : Term ℕ 3) (op : CompOp) (c : ℕ) : Selection ℕ 3

The selection predicate t op c of an existential atom.

Equations

• atomSel t op c = Selection.BT (BoolTerm.ofCompOp op t (Term.const c))

def existentialQuery (t : Term ℕ 3) (op : CompOp) (c : ℕ) (q : Query ℕ 3) : Query ℕ 1

The rewriting ε(Π_{#0}(σ_{t op c}(q))) of an existential comparison f(t) op c: the group keys of the qualifying occurrences, duplicate- eliminated.

Equations

• existentialQuery t op c q = ε (Π keyTerm (σ (atomSel t op c) q))

theorem existentialQuery_source (t : Term ℕ 3) (op : CompOp) (c : ℕ) (q : Query ℕ 3) (hq : q.source) : (existentialQuery t op c q).source

theorem existentialQuery_key_mem {K : Type} [CommSemiringWithMonus K] [DecidableEq K] (t : Term ℕ 3) (op : CompOp) (c : ℕ) (q : Query ℕ 3) (hq : q.source) (d : AnnotatedDatabase ℕ K) (x : AnnotatedTuple ℕ K 1) (hx : x ∈ (existentialQuery t op c q).evaluateAnnotated ⋯ d) : x.1 ∈ (Multiset.map keyOf (q.evaluateAnnotated hq d)).dedup

Every row of the existential rewriting carries a key of the base query.

theorem existentialQuery_perKeySum {K : Type} [CommSemiringWithMonus K] [DecidableEq K] (t : Term ℕ 3) (op : CompOp) (c : ℕ) (q : Query ℕ 3) (hq : q.source) (d : AnnotatedDatabase ℕ K) (g : Tuple ℕ 1) : (Multiset.map Prod.snd (Multiset.filter (fun (p : Tuple ℕ 1 × K) => p.1 = g) ((existentialQuery t op c q).evaluateAnnotated ⋯ d))).sum = (Multiset.map Prod.snd (Multiset.filter (fun (p : AnnotatedTuple ℕ K 3) => keyOf p = g ∧ op.eval (t.eval p.1) c) (q.evaluateAnnotated hq d))).sum

Per key, the existential rewriting sums the annotations of the base rows of that key satisfying t op c.

theorem existential_perKey {K : Type} [CommSemiringWithMonus K] [DecidableEq K] [HasAltLinearOrder K] (h_abs : absorptive K) {f : SeqAggFunc ℕ} {op : CompOp} (hf : Having.Existential f op) (q : Query ℕ 3) (hq : q.source) (d : AnnotatedDatabase ℕ K) (ts : Tuple (Term ℕ 3) 1) (c : ℕ) (g : Tuple ℕ 1) : (Multiset.map Prod.snd (Multiset.filter (fun (p : Tuple ℕ 1 × K) => p.1 = g) ((existentialQuery (ts 0) op c q).evaluateAnnotated ⋯ d))).sum = Having.havingProv (Having.havingGroup keyIdx (q.evaluateAnnotated hq d) g) (ts 0) f op c

Existential atoms, per key. In an absorptive commutative m-semiring, the existential rewriting gives every group key the fused f(t) op c predicate provenance of its group, for any existential comparison (MIN with ≤/<, MAX with ≥/>). No distributivity of ⊗ over ⊖ is assumed (Having.havingProv_existential).

theorem existential_site_rewrite {K : Type} [CommSemiringWithMonus K] [DecidableEq K] [HasAltLinearOrder K] (h_abs : absorptive K) {f : SeqAggFunc ℕ} {op : CompOp} (hf : Having.Existential f op) (q : Query ℕ 3) (hq : q.source) (d : AnnotatedDatabase ℕ K) (ts' : Tuple (Term ℕ 3) 1) (c : ℕ) : Multiset.map (fun (p : AnnotatedTuple ℕ K (1 + 1)) => (fun (x : Fin 1) => p.1 ⟨0, ⋯⟩, p.2)) ((AggQuery.havingSite keyIdx ts' (fun (x : Fin 1) => f) op 0 (Term.const c) (q.toAgg hq)).evaluateAnnotated d) = (keyPadded (existentialQuery (ts' 0) op c) q).evaluateAnnotated ⋯ d

Site substitution for existential atoms. In every absorptive commutative m-semiring, the key-projected fused HAVING f(t) op c site and the padded rewriting ε(Π_{#0}(σ_{t op c}(q))) evaluate to the same multiset of annotated tuples, for any existential comparison.

theorem minLe_site_rewrite {K : Type} [CommSemiringWithMonus K] [DecidableEq K] [HasAltLinearOrder K] (h_abs : absorptive K) (q : Query ℕ 3) (hq : q.source) (d : AnnotatedDatabase ℕ K) (ts' : Tuple (Term ℕ 3) 1) (c : ℕ) : Multiset.map (fun (p : AnnotatedTuple ℕ K (1 + 1)) => (fun (x : Fin 1) => p.1 ⟨0, ⋯⟩, p.2)) ((AggQuery.havingSite keyIdx ts' (fun (x : Fin 1) => SeqAggFunc.minD) CompOp.le 0 (Term.const c) (q.toAgg hq)).evaluateAnnotated d) = (keyPadded (existentialQuery (ts' 0) CompOp.le c) q).evaluateAnnotated ⋯ d

MIN(t) ≤ c.

theorem minLt_site_rewrite {K : Type} [CommSemiringWithMonus K] [DecidableEq K] [HasAltLinearOrder K] (h_abs : absorptive K) (q : Query ℕ 3) (hq : q.source) (d : AnnotatedDatabase ℕ K) (ts' : Tuple (Term ℕ 3) 1) (c : ℕ) : Multiset.map (fun (p : AnnotatedTuple ℕ K (1 + 1)) => (fun (x : Fin 1) => p.1 ⟨0, ⋯⟩, p.2)) ((AggQuery.havingSite keyIdx ts' (fun (x : Fin 1) => SeqAggFunc.minD) CompOp.lt 0 (Term.const c) (q.toAgg hq)).evaluateAnnotated d) = (keyPadded (existentialQuery (ts' 0) CompOp.lt c) q).evaluateAnnotated ⋯ d

MIN(t) < c.

theorem maxGe_site_rewrite {K : Type} [CommSemiringWithMonus K] [DecidableEq K] [HasAltLinearOrder K] (h_abs : absorptive K) (q : Query ℕ 3) (hq : q.source) (d : AnnotatedDatabase ℕ K) (ts' : Tuple (Term ℕ 3) 1) (c : ℕ) : Multiset.map (fun (p : AnnotatedTuple ℕ K (1 + 1)) => (fun (x : Fin 1) => p.1 ⟨0, ⋯⟩, p.2)) ((AggQuery.havingSite keyIdx ts' (fun (x : Fin 1) => SeqAggFunc.maxD) CompOp.ge 0 (Term.const c) (q.toAgg hq)).evaluateAnnotated d) = (keyPadded (existentialQuery (ts' 0) CompOp.ge c) q).evaluateAnnotated ⋯ d

MAX(t) ≥ c.

theorem maxGt_site_rewrite {K : Type} [CommSemiringWithMonus K] [DecidableEq K] [HasAltLinearOrder K] (h_abs : absorptive K) (q : Query ℕ 3) (hq : q.source) (d : AnnotatedDatabase ℕ K) (ts' : Tuple (Term ℕ 3) 1) (c : ℕ) : Multiset.map (fun (p : AnnotatedTuple ℕ K (1 + 1)) => (fun (x : Fin 1) => p.1 ⟨0, ⋯⟩, p.2)) ((AggQuery.havingSite keyIdx ts' (fun (x : Fin 1) => SeqAggFunc.maxD) CompOp.gt 0 (Term.const c) (q.toAgg hq)).evaluateAnnotated d) = (keyPadded (existentialQuery (ts' 0) CompOp.gt c) q).evaluateAnnotated ⋯ d

MAX(t) > c.

Boolean closure: join on the group key and set union

A conjunction of conditions is rewritten as the join of the two rewritings on the group key, ε(Π_{#0}(σ_{#0 = #1}(Q₁ × Q₂))), and a disjunction as their set union ε(Q₁ ⊎ Q₂). Per key, the join multiplies and the union adds the annotations, which is exactly how the fused semantics (HavingPred.prov) interprets ∧ and ∨.

def joinSel : Selection ℕ 2

The key-equality predicate #0 = #1 on a pair of one-column rows.

Equations

• joinSel = Selection.BT (BoolTerm.EQ #⟨0, joinSel._proof_3⟩ #⟨1, joinSel._proof_4⟩)

def pairKey : Tuple (Term ℕ 2) 1

The projection of a pair of one-column rows to its first column.

Equations

• pairKey x✝ = #⟨0, joinSel._proof_3⟩

def keyJoinInner (Q₁ Q₂ : Query ℕ 1) : Query ℕ 2

The key-equality selection over the product, σ_{#0 = #1}(Q₁ × Q₂).

Equations

• keyJoinInner Q₁ Q₂ = σ joinSel (Q₁ × Q₂)

def keyJoin (Q₁ Q₂ : Query ℕ 1) : Query ℕ 1

Join on the group key, ε(Π_{#0}(σ_{#0 = #1}(Q₁ × Q₂))).

Equations

• keyJoin Q₁ Q₂ = ε (Π pairKey (keyJoinInner Q₁ Q₂))

def keyUnion (Q₁ Q₂ : Query ℕ 1) : Query ℕ 1

Set union, ε(Q₁ ⊎ Q₂).

Equations

• keyUnion Q₁ Q₂ = ε (Q₁ ⊎ Q₂)

theorem keyJoin_source (Q₁ Q₂ : Query ℕ 1) (h₁ : Q₁.source) (h₂ : Q₂.source) : (keyJoin Q₁ Q₂).source

theorem keyUnion_source (Q₁ Q₂ : Query ℕ 1) (h₁ : Q₁.source) (h₂ : Q₂.source) : (keyUnion Q₁ Q₂).source

def pairRow {K : Type} [CommSemiringWithMonus K] (z : AnnotatedTuple ℕ K 1 × AnnotatedTuple ℕ K 1) : AnnotatedTuple ℕ K 2

The row of a product: appended data parts, multiplied annotations.

Equations

• pairRow z = (Fin.append z.1.1 z.2.1, z.1.2 * z.2.2)

theorem keyJoinInner_eval {K : Type} [CommSemiringWithMonus K] [DecidableEq K] (Q₁ Q₂ : Query ℕ 1) (h₁ : Q₁.source) (h₂ : Q₂.source) (d : AnnotatedDatabase ℕ K) : (keyJoinInner Q₁ Q₂).evaluateAnnotated ⋯ d = Multiset.filter (fun (ta : AnnotatedTuple ℕ K 2) => joinSel.eval ta.1) (Multiset.map pairRow (Multiset.product (Q₁.evaluateAnnotated h₁ d) (Q₂.evaluateAnnotated h₂ d)))

The annotated semantics of the key-equality selection over the product, in closed form.

theorem sum_map_mul_product {K : Type} [CommSemiringWithMonus K] {α β : Type} (f : α → K) (h : β → K) (s : Multiset α) (t : Multiset β) : (Multiset.map (fun (z : α × β) => f z.1 * h z.2) (s ×ˢ t)).sum = (Multiset.map f s).sum * (Multiset.map h t).sum

A sum of products over a product multiset factorizes.

theorem keyJoin_perKeySum {K : Type} [CommSemiringWithMonus K] [DecidableEq K] (Q₁ Q₂ : Query ℕ 1) (h₁ : Q₁.source) (h₂ : Q₂.source) (d : AnnotatedDatabase ℕ K) (g : Tuple ℕ 1) : (Multiset.map Prod.snd (Multiset.filter (fun (p : Tuple ℕ 1 × K) => p.1 = g) ((keyJoin Q₁ Q₂).evaluateAnnotated ⋯ d))).sum = (Multiset.map Prod.snd (Multiset.filter (fun (p : Tuple ℕ 1 × K) => p.1 = g) (Q₁.evaluateAnnotated h₁ d))).sum * (Multiset.map Prod.snd (Multiset.filter (fun (p : Tuple ℕ 1 × K) => p.1 = g) (Q₂.evaluateAnnotated h₂ d))).sum

Join on the key multiplies the per-key annotations.

theorem keyUnion_perKeySum {K : Type} [CommSemiringWithMonus K] [DecidableEq K] (Q₁ Q₂ : Query ℕ 1) (h₁ : Q₁.source) (h₂ : Q₂.source) (d : AnnotatedDatabase ℕ K) (g : Tuple ℕ 1) : (Multiset.map Prod.snd (Multiset.filter (fun (p : Tuple ℕ 1 × K) => p.1 = g) ((keyUnion Q₁ Q₂).evaluateAnnotated ⋯ d))).sum = (Multiset.map Prod.snd (Multiset.filter (fun (p : Tuple ℕ 1 × K) => p.1 = g) (Q₁.evaluateAnnotated h₁ d))).sum + (Multiset.map Prod.snd (Multiset.filter (fun (p : Tuple ℕ 1 × K) => p.1 = g) (Q₂.evaluateAnnotated h₂ d))).sum

Set union adds the per-key annotations.

theorem keyJoin_key_mem {K : Type} [CommSemiringWithMonus K] [DecidableEq K] (Q₁ Q₂ : Query ℕ 1) (h₁ : Q₁.source) (h₂ : Q₂.source) (d : AnnotatedDatabase ℕ K) (x : AnnotatedTuple ℕ K 1) (hx : x ∈ (keyJoin Q₁ Q₂).evaluateAnnotated ⋯ d) : ∃ y ∈ Q₁.evaluateAnnotated h₁ d, x.1 = y.1

Rows of a key join carry keys of the left argument.

theorem keyUnion_key_mem {K : Type} [CommSemiringWithMonus K] [DecidableEq K] (Q₁ Q₂ : Query ℕ 1) (h₁ : Q₁.source) (h₂ : Q₂.source) (d : AnnotatedDatabase ℕ K) (x : AnnotatedTuple ℕ K 1) (hx : x ∈ (keyUnion Q₁ Q₂).evaluateAnnotated ⋯ d) : (∃ y ∈ Q₁.evaluateAnnotated h₁ d, x.1 = y.1) ∨ ∃ y ∈ Q₂.evaluateAnnotated h₂ d, x.1 = y.1

Rows of a set union carry keys of one of the arguments.

Monotone conditions and their compositional rewriting

inductive MonoCond (n₂ : ℕ) : Type

Monotone HAVING conditions over the aggregate columns of a grouping: COUNT(*) ≥ C + 1 and COUNT(*) > C + 1 on the token column l, an existential comparison f(t) op c on the token column l, and conjunctions and disjunctions. Negation is excluded: it flips monotonicity.

• countGe {n₂ : ℕ} (l : Fin n₂) (C : ℕ) : MonoCond n₂
• countGt {n₂ : ℕ} (l : Fin n₂) (C : ℕ) : MonoCond n₂
• exist {n₂ : ℕ} (l : Fin n₂) (op : CompOp) (c : ℕ) : MonoCond n₂
• and {n₂ : ℕ} (ψ₁ ψ₂ : MonoCond n₂) : MonoCond n₂
• or {n₂ : ℕ} (ψ₁ ψ₂ : MonoCond n₂) : MonoCond n₂

def MonoCond.WF {n₂ : ℕ} (fs : Tuple (SeqAggFunc ℕ) n₂) : MonoCond n₂ → Prop

Well-formedness with respect to the aggregates fs of the grouping: the COUNT(*) atoms sit on COUNT(*) columns and the existential atoms on existential aggregate/operator pairs (MIN with ≤/<, MAX with ≥/>, see Having.Existential).

Equations

• MonoCond.WF fs (MonoCond.countGe l C) = (fs l = SeqAggFunc.count)
• MonoCond.WF fs (MonoCond.countGt l C) = (fs l = SeqAggFunc.count)
• MonoCond.WF fs (MonoCond.exist l op c) = Having.Existential (fs l) op
• MonoCond.WF fs (ψ₁.and ψ₂) = (MonoCond.WF fs ψ₁ ∧ MonoCond.WF fs ψ₂)
• MonoCond.WF fs (ψ₁.or ψ₂) = (MonoCond.WF fs ψ₁ ∧ MonoCond.WF fs ψ₂)

def MonoCond.toHavingPred {n₂ : ℕ} (ts : Tuple (Term ℕ 3) n₂) (fs : Tuple (SeqAggFunc ℕ) n₂) : MonoCond n₂ → HavingPred ℕ 3 1

The condition as a Boolean combination of fused aggregate comparisons, whose provenance is HavingPred.prov (∧ ↦ ⊗, ∨ ↦ ⊕).

Equations

• MonoCond.toHavingPred ts fs (MonoCond.countGe l C) = HavingPred.cmp (ts l) (fs l) CompOp.ge (Term.const (C + 1))
• MonoCond.toHavingPred ts fs (MonoCond.countGt l C) = HavingPred.cmp (ts l) (fs l) CompOp.gt (Term.const (C + 1))
• MonoCond.toHavingPred ts fs (MonoCond.exist l op c) = HavingPred.cmp (ts l) (fs l) op (Term.const c)
• MonoCond.toHavingPred ts fs (ψ₁.and ψ₂) = (MonoCond.toHavingPred ts fs ψ₁).and (MonoCond.toHavingPred ts fs ψ₂)
• MonoCond.toHavingPred ts fs (ψ₁.or ψ₂) = (MonoCond.toHavingPred ts fs ψ₁).or (MonoCond.toHavingPred ts fs ψ₂)

def MonoCond.rewrite {n₂ : ℕ} (ts : Tuple (Term ℕ 3) n₂) : MonoCond n₂ → Query ℕ 3 → Query ℕ 1

The compositional positive rewriting Q_ψ: COUNT(*) atoms become the join chains Q₂^{≥ C}, existential atoms ε(Π_{#0}(σ_{t op c}(q))), a conjunction the join of the two rewritings on the group key, and a disjunction their set union.

Equations

• MonoCond.rewrite ts (MonoCond.countGe l C) x✝ = joinChainQuery x✝ C
• MonoCond.rewrite ts (MonoCond.countGt l C) x✝ = joinChainQuery x✝ (C + 1)
• MonoCond.rewrite ts (MonoCond.exist l op c) x✝ = existentialQuery (ts l) op c x✝
• MonoCond.rewrite ts (ψ₁.and ψ₂) x✝ = keyJoin (MonoCond.rewrite ts ψ₁ x✝) (MonoCond.rewrite ts ψ₂ x✝)
• MonoCond.rewrite ts (ψ₁.or ψ₂) x✝ = keyUnion (MonoCond.rewrite ts ψ₁ x✝) (MonoCond.rewrite ts ψ₂ x✝)

theorem MonoCond.rewrite_source {n₂ : ℕ} (ts : Tuple (Term ℕ 3) n₂) (q : Query ℕ 3) (hq : q.source) (ψ : MonoCond n₂) : (rewrite ts ψ q).source

theorem MonoCond.perKey_correct {K : Type} [CommSemiringWithMonus K] [DecidableEq K] [HasAltLinearOrder K] {n₂ : ℕ} (h_abs : absorptive K) (ts : Tuple (Term ℕ 3) n₂) (fs : Tuple (SeqAggFunc ℕ) n₂) (q : Query ℕ 3) (hq : q.source) (d : AnnotatedDatabase ℕ K) (hnodup : (Multiset.map Prod.fst (q.evaluateAnnotated hq d)).Nodup) (g : Tuple ℕ 1) (ψ : MonoCond n₂) : WF fs ψ → (Multiset.map Prod.snd (Multiset.filter (fun (p : Tuple ℕ 1 × K) => p.1 = g) ((rewrite ts ψ q).evaluateAnnotated ⋯ d))).sum = HavingPred.prov (Having.havingGroup keyIdx (q.evaluateAnnotated hq d) g) g (toHavingPred ts fs ψ)

Per-key correctness of the compositional rewriting. In an absorptive commutative m-semiring, for every well-formed monotone condition ψ, the rewriting Q_ψ gives every group key the fused provenance HavingPred.prov of ψ on its group. Induction on ψ: the atoms are Query.joinChain_count_correct and existential_perKey, and ∧/∨ are keyJoin_perKeySum/keyUnion_perKeySum. Distributivity of ⊗ over ⊖ is not assumed.

theorem MonoCond.key_mem {K : Type} [CommSemiringWithMonus K] [DecidableEq K] {n₂ : ℕ} (ts : Tuple (Term ℕ 3) n₂) (q : Query ℕ 3) (hq : q.source) (d : AnnotatedDatabase ℕ K) (ψ : MonoCond n₂) (x : AnnotatedTuple ℕ K 1) : x ∈ (rewrite ts ψ q).evaluateAnnotated ⋯ d → x.1 ∈ (Multiset.map keyOf (q.evaluateAnnotated hq d)).dedup

Every row of the rewriting carries a key of the base query.

theorem MonoCond.padded_correct {K : Type} [CommSemiringWithMonus K] [DecidableEq K] [HasAltLinearOrder K] {n₂ : ℕ} (h_abs : absorptive K) (ts : Tuple (Term ℕ 3) n₂) (fs : Tuple (SeqAggFunc ℕ) n₂) (q : Query ℕ 3) (hq : q.source) (d : AnnotatedDatabase ℕ K) (hnodup : (Multiset.map Prod.fst (q.evaluateAnnotated hq d)).Nodup) (ψ : MonoCond n₂) (hwf : WF fs ψ) : (keyPadded (rewrite ts ψ) q).evaluateAnnotated ⋯ d = Multiset.map (fun (g : Tuple ℕ 1) => (g, HavingPred.prov (Having.havingGroup keyIdx (q.evaluateAnnotated hq d) g) g (toHavingPred ts fs ψ))) (Multiset.map keyOf (q.evaluateAnnotated hq d)).dedup

Multiset-level correctness of the compositional rewriting. In an absorptive commutative m-semiring, the padded rewriting Q_ψ of a well-formed monotone condition evaluates to exactly one row per group key of the base query, annotated with the fused provenance HavingPred.prov of ψ on the group.

The fused site of a compound condition, in the general evaluator

def MonoCond.toGenPred {n₂ : ℕ} : MonoCond n₂ → GenPred ℕ (ColKind.gammaKinds 1 n₂)

The condition as a generalized selection predicate over the output of Gamma: each atom compares its token column against a constant (GenPred.fusedCmp), and ∧/∨ are the Boolean connectives of GenPred.

Equations

• (MonoCond.countGe l C).toGenPred = GenPred.fusedCmp CompOp.ge l (Term.const (C + 1))
• (MonoCond.countGt l C).toGenPred = GenPred.fusedCmp CompOp.gt l (Term.const (C + 1))
• (MonoCond.exist l op c).toGenPred = GenPred.fusedCmp op l (Term.const c)
• (ψ₁.and ψ₂).toGenPred = ψ₁.toGenPred.and ψ₂.toGenPred
• (ψ₁.or ψ₂).toGenPred = ψ₁.toGenPred.or ψ₂.toGenPred

@[reducible, inline]

abbrev MonoCond.site {n₂ : ℕ} (ts : Tuple (Term ℕ 3) n₂) (fs : Tuple (SeqAggFunc ℕ) n₂) (ψ : MonoCond n₂) (qg : AggQuery ℕ 3 (ColKind.allReg 3)) : AggQuery ℕ (1 + n₂) (ColKind.gammaKinds 1 n₂)

The fused site σ_ψ(γ_{#0}[ts : fs](qg)) of a monotone condition, as a general query.

Equations

• MonoCond.site ts fs ψ qg = AggQuery.Sel ψ.toGenPred (AggQuery.Gamma keyIdx ts fs qg)

theorem MonoCond.toGenPred_hasAggAtom {n₂ : ℕ} (ψ : MonoCond n₂) : ψ.toGenPred.hasAggAtom = true

theorem MonoCond.toGenPred_entailsExistence {n₂ : ℕ} (ψ : MonoCond n₂) : ψ.toGenPred.entailsExistence false = true

A positive combination of aggregate atoms entails the existence of the compared groups.

theorem MonoCond.toGenPred_comparedCols {n₂ : ℕ} (ψ : MonoCond n₂) (k : Fin (1 + n₂)) : k ∈ ψ.toGenPred.comparedCols → ∃ (l : Fin n₂), k = Fin.natAdd 1 l

Every compared column of the condition is a token column.

theorem MonoCond.toGenPred_comparedCols_nonempty {n₂ : ℕ} (ψ : MonoCond n₂) : ψ.toGenPred.comparedCols.Nonempty

The condition compares at least one token column.

theorem MonoCond.toGenPred_predsem {K : Type} [CommSemiringWithMonus K] [DecidableEq K] {n₂ : ℕ} (ts : Tuple (Term ℕ 3) n₂) (fs : Tuple (SeqAggFunc ℕ) n₂) (U : List (AnnotatedTuple ℕ K 3)) (g : Tuple ℕ 1) (ψ : MonoCond n₂) : ψ.toGenPred.predsem false (Fin.append (fun (k : Fin 1) => Sum.inl (g k)) fun (j : Fin n₂) => Sum.inr (AggValue.ofGroup (fs j) (ts j) U)) = HavingPred.prov U g (toHavingPred ts fs ψ)

The predicate provenance of the condition on the Gamma output row of the group g is HavingPred.prov of the condition on the group sequence.

theorem MonoCond.compared_all_eq {K : Type} {n₂ : ℕ} {f : Fin (1 + n₂) → Option (List K)} {L : List K} (hf : ∀ (l : Fin n₂), f (Fin.natAdd 1 l) = some L) (ψ : MonoCond n₂) (l' : List K) : l' ∈ Multiset.filterMap f ψ.toGenPred.comparedCols.val → l' = L

The compared annotation lists of the condition on the Gamma output row all equal the group's annotation list.

theorem MonoCond.compared_ne_zero {K : Type} {n₂ : ℕ} {f : Fin (1 + n₂) → Option (List K)} {L : List K} (hf : ∀ (l : Fin n₂), f (Fin.natAdd 1 l) = some L) (ψ : MonoCond n₂) : Multiset.filterMap f ψ.toGenPred.comparedCols.val ≠ 0

The condition compares at least one token, so its compared lists are not empty.

theorem MonoCond.finalize_eq_of_pending_eq_zero {K : Type} [CommSemiringWithMonus K] (b : K) (p : Multiset (List K)) (hp : p = 0) : { base := b, pending := p }.finalize = b

A row whose pending factors vanish finalizes to its concrete part.

theorem MonoCond.site_evaluateAnnotated {K : Type} [CommSemiringWithMonus K] [DecidableEq K] [HasAltLinearOrder K] {n₂ : ℕ} (ts : Tuple (Term ℕ 3) n₂) (fs : Tuple (SeqAggFunc ℕ) n₂) (ψ : MonoCond n₂) (qg : AggQuery ℕ 3 (ColKind.allReg 3)) (d : AnnotatedDatabase ℕ K) : (site ts fs ψ qg).evaluateAnnotated d = Multiset.map (fun (g : Fin 1 → ℕ) => (Fin.append g fun (k : Fin n₂) => fs k (List.map (fun (p : AnnotatedTuple ℕ K 3) => (ts k).eval p.1) (Having.havingGroup keyIdx (qg.evaluateAnnotated d) g)), HavingPred.prov (Having.havingGroup keyIdx (qg.evaluateAnnotated d) g) g (toHavingPred ts fs ψ))) (Multiset.map (fun (p : AnnotatedTuple ℕ K 3) (k : Fin 1) => p.1 (keyIdx k)) (qg.evaluateAnnotated d)).dedup

Closed form of the fused site of a monotone condition. 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 fused provenance HavingPred.prov of the condition on the group's occurrence sequence: the pending group factor introduced by Gamma is superseded by the compared tokens (every atom compares a token of that very group), and the atoms' predicate provenances combine by ⊗/⊕. Generalizes AggQuery.havingSite_evaluateAnnotated from one comparison to a positive Boolean combination.

theorem MonoCond.site_key_proj {K : Type} [CommSemiringWithMonus K] [DecidableEq K] [HasAltLinearOrder K] {n₂ : ℕ} (ts : Tuple (Term ℕ 3) n₂) (fs : Tuple (SeqAggFunc ℕ) n₂) (ψ : MonoCond n₂) (qg : AggQuery ℕ 3 (ColKind.allReg 3)) (q : Query ℕ 3) (hq : q.source) (d : AnnotatedDatabase ℕ K) (hin : qg.evaluateAnnotated d = q.evaluateAnnotated hq d) : Multiset.map (fun (p : AnnotatedTuple ℕ K (1 + n₂)) => (fun (x : Fin 1) => p.1 ⟨0, ⋯⟩, p.2)) ((site ts fs ψ qg).evaluateAnnotated d) = Multiset.map (fun (g : Tuple ℕ 1) => (g, HavingPred.prov (Having.havingGroup keyIdx (q.evaluateAnnotated hq d) g) g (toHavingPred ts fs ψ))) (Multiset.map keyOf (q.evaluateAnnotated hq d)).dedup

The key-projected fused site of a monotone condition is one row per group key of the base query, annotated with the fused provenance of the condition on its group (the shape the padded rewriting evaluates to).

theorem MonoCond.site_rewrite {K : Type} [CommSemiringWithMonus K] [DecidableEq K] [HasAltLinearOrder K] {n₂ : ℕ} (h_abs : absorptive K) (ts : Tuple (Term ℕ 3) n₂) (fs : Tuple (SeqAggFunc ℕ) n₂) (ψ : MonoCond n₂) (hwf : WF fs ψ) (q : Query ℕ 3) (hq : q.source) (d : AnnotatedDatabase ℕ K) (hnodup : (Multiset.map Prod.fst (q.evaluateAnnotated hq d)).Nodup) : Multiset.map (fun (p : AnnotatedTuple ℕ K (1 + n₂)) => (fun (x : Fin 1) => p.1 ⟨0, ⋯⟩, p.2)) ((site ts fs ψ (q.toAgg hq)).evaluateAnnotated d) = (keyPadded (rewrite ts ψ) q).evaluateAnnotated ⋯ d

Site substitution for monotone conditions: absorptivity suffices. In every absorptive commutative m-semiring – distributivity of ⊗ over ⊖ not required – the key-projected fused site σ_ψ(γ_{#0}[ts : fs](q)) of a well-formed monotone condition ψ and the padded compositional rewriting Q_ψ evaluate to the same multiset of annotated tuples: the rewriting can be substituted for the key-projected fused operator inside any surrounding query. The sole hypothesis on the instance is the global row-distinctness of the base query's output (the occurrence identifiers of the COUNT(*) join chains).

Home · Documentation · Publications · Contributors · Source · Cite