Query-level correctness of the fused HAVING operator vs the JOIN rewriting

This file proves the query-level correspondence between the possible-world semantics of the fused HAVING COUNT(*) operator and its JOIN-based rewriting, in absorptive commutative m-semirings in which ⊗ distributes over ⊖.

• C = 1 (AggQuery.havingSite_count_ge_one): the fused COUNT(*) ≥ 1 operator agrees – key by key, annotation by annotation – with the duplicate-eliminated key projection ε(Π_{keys}(q)), via the extensional characterization groupByKey_eq_dedup_map of duplicate elimination, Having.havingGroup_coe, and Having.havingProv_count_ge_one.

• General C (Query.joinChain_count_correct): the C-fold self-join chain ε(Π_{#0}(joinChain q C)) gives every group key the ⊕-sum S_{C+1} of the monomials of its (C+1)-element worlds, which is the fused COUNT(*) ≥ C + 1 predicate provenance. The tie-broken comparison <* of the rewriting is materialized by an occurrence identifier column: the base query has columns (key, value, identifier) and the chain condition compares (value, identifier) pairs lexicographically, so any injective assignment of identifiers within each group – the sole hypothesis – realizes an arbitrary resolution of ties between equal values; duplicate values are fully supported. The statement is per key: a group with fewer than C + 1 occurrences has provenance 𝟘 on both sides (the fused operator annotates its row with 𝟘, the join query has no row for it).

The proof of the general case runs through three layers: the pure chain algebra (chainAgg, summing to the elementary symmetric sum esymm of the group's annotations over any strictly increasing enumeration), the per-key evaluation invariant of the join chain (joinChain_eval_filter), and the collapse of the fused semantics (Having.havingProv_count_ge with S_eq_esymm).

• =/≤ comparisons (Query.joinChainDiff_count_eq_correct, Query.joinChainDiff_count_le_correct): the remaining comparison operators are differences of two ≥ chains (Q₂^{=C} = Q₂^{≥C} − Q₂^{≥C+1} and Q₂^{≤C} = Q₂^{≥1} − Q₂^{≥C+1}), assembled through the Diff semantics: since a duplicate-eliminated relation has one row per key, per-key annotation sums commute with Diff (diff_perKeySum), and the group-level content is Having.G_eq_S_monus_S and Having.atMost_eq_S_monus_S.

theorem groupByKey_eq_dedup_map {T : Type} [ValueType T] {K : Type} [SemiringWithMonus K] [DecidableEq K] {n : ℕ} (r : AnnotatedRelation T K n) : ↑↑(groupByKey r) = Multiset.map (fun (u : Tuple T n) => (u, (Multiset.map Prod.snd (Multiset.filter (fun (p : AnnotatedTuple T K n) => p.1 = u) r)).sum)) (Multiset.map Prod.fst r).dedup

Extensional characterization of duplicate elimination. groupByKey produces exactly one row per distinct key of the input, whose annotation is the ⊕-sum of the annotations of the matching rows.

theorem AggQuery.havingSite_count_ge_one {K : Type} [CommSemiringWithMonus K] [DecidableEq K] [HasAltLinearOrder K] (h_abs : absorptive K) (h_distrib : mul_sub_left_distributive K) {m n₁ : ℕ} (is : Tuple (Fin m) n₁) (ts : Tuple (Term ℕ m) 1) (q : Query ℕ m) (hq : q.source) (d : AnnotatedDatabase ℕ K) : Multiset.map (fun (p : AnnotatedTuple ℕ K (n₁ + 1)) => (fun (k : Fin n₁) => p.1 (Fin.castAdd 1 k), p.2)) ((havingSite is ts ![SeqAggFunc.count] CompOp.ge 0 (Term.const 1) (q.toAgg hq)).evaluateAnnotated d) = (ε ((Π fun (k : Fin n₁) => #(is k)) q)).evaluateAnnotated hq d

Query-level correctness for COUNT(*) ≥ 1. In an absorptive commutative m-semiring in which ⊗ distributes over ⊖, the fused HAVING COUNT(*) ≥ 1 site – with its output rows projected to the group key – computes exactly the duplicate-eliminated key projection ε(Π_{keys}(q)) of the inner query, which is the C = 1 join-based query: one row per non-empty group, annotated by the ⊕-sum of the group's annotations. Stated against any general subquery whose annotated evaluation is the classical inner query's.

The chain algebra of the C-fold self-join

The semantic content of the join chain: the annotated strictly increasing chains over a multiset of (value, annotation) pairs, and their ⊕-sum, which is the elementary symmetric sum of the annotations – the multiset form of the join-side provenance Having.S.

def Having.esymm {K : Type} [CommSemiringWithMonus K] (s : Multiset K) (C : ℕ) : K

The elementary symmetric sum of a multiset of annotations: the ⊕-sum, over the C-element sub-multisets, of their ⊗-products. This is the position-free form of the join-side provenance Having.S (S_eq_esymm).

Equations

• Having.esymm s C = (Multiset.map Multiset.prod (Multiset.powersetCard C s)).sum

@[simp]

theorem Having.esymm_zero {K : Type} [CommSemiringWithMonus K] (s : Multiset K) : esymm s 0 = 1

theorem Having.esymm_cons {K : Type} [CommSemiringWithMonus K] (a : K) (s : Multiset K) (C : ℕ) : esymm (a ::ₘ s) (C + 1) = esymm s (C + 1) + a * esymm s C

theorem Having.S_eq_esymm {K : Type} [CommSemiringWithMonus K] {ι : Type} [DecidableEq ι] [Fintype ι] (α : ι → K) (C : ℕ) : S α Finset.univ C = esymm (Multiset.map α Finset.univ.val) C

Having.S over a full position space is the elementary symmetric sum of the annotation multiset: the join-side provenance only depends on the multiset of the annotations, not on the position space carrying them.

def Having.chainAgg {V : Type} [LinearOrder V] {K : Type} [CommSemiringWithMonus K] (G : Multiset (V × K)) : ℕ → Multiset (V × K)

The annotated strictly increasing chains of length C + 1 over a multiset G of (value, annotation) pairs, each chain represented by its last value and the ⊗-product of its annotations. This is the semantic content of the C-fold self-join chain of the join-based rewriting.

Equations

• Having.chainAgg G 0 = G
• Having.chainAgg G C.succ = Multiset.map (fun (x : (V × K) × V × K) => (x.2.1, x.1.2 * x.2.2)) (Multiset.filter (fun (x : (V × K) × V × K) => x.1.1 < x.2.1) (Having.chainAgg G C ×ˢ G))

theorem Having.chainAgg_zero {V : Type} [LinearOrder V] {K : Type} [CommSemiringWithMonus K] (C : ℕ) : chainAgg 0 C = 0

theorem Having.chainAgg_fst_mem {V : Type} [LinearOrder V] {K : Type} [CommSemiringWithMonus K] (G : Multiset (V × K)) (C : ℕ) (x : V × K) : x ∈ chainAgg G C → x.1 ∈ Multiset.map Prod.fst G

The last value of a chain is one of the input values.

theorem Having.product_singleton_right {α β : Type} (s : Multiset α) (b : β) : s ×ˢ {b} = Multiset.map (fun (a : α) => (a, b)) s

theorem Having.chainAgg_add_of_max {V : Type} [LinearOrder V] {K : Type} [CommSemiringWithMonus K] (G : Multiset (V × K)) (u : V × K) (hmax : ∀ v ∈ Multiset.map Prod.fst G, v < u.1) (C : ℕ) : chainAgg (G + {u}) C = chainAgg G C + match C with | 0 => {u} | C'.succ => Multiset.map (fun (x : V × K) => (u.1, x.2 * u.2)) (chainAgg G C')

Appending an occurrence whose value dominates every value of G: the chains over G + {u} are the chains over G together with the chains ending at u (a u-free chain extended by u, or u alone).

theorem Having.chainAgg_sum_of_sorted {V : Type} [LinearOrder V] {K : Type} [CommSemiringWithMonus K] (U : List (V × K)) : List.Pairwise (fun (p q : V × K) => p.1 < q.1) U → ∀ (C : ℕ), (Multiset.map Prod.snd (chainAgg (↑U) C)).sum = esymm (↑(List.map Prod.snd U)) (C + 1)

The chain sum is the elementary symmetric sum. Over a list of (value, annotation) pairs with strictly increasing values, the ⊕-sum of the annotations of the strictly increasing chains of length C + 1 is the elementary symmetric sum of degree C + 1 of the annotations.

theorem Having.append_coord_left {m n : ℕ} (x : Tuple ℕ m) (y : Tuple ℕ n) (i : ℕ) (h : i < m) (h' : i < m + n) : Fin.append x y ⟨i, h'⟩ = x ⟨i, h⟩

Left coordinate of an appended tuple.

theorem Having.append_coord_right {m n : ℕ} (x : Tuple ℕ m) (y : Tuple ℕ n) (i : ℕ) (h : i < n) (h' : m + i < m + n) : Fin.append x y ⟨m + i, h'⟩ = y ⟨i, h⟩

Right coordinate of an appended tuple, at offset m + i.

theorem Having.append_coord_right₀ {m n : ℕ} (x : Tuple ℕ m) (y : Tuple ℕ n) (h : 0 < n) (h' : m < m + n) : Fin.append x y ⟨m, h'⟩ = y ⟨0, h⟩

Right coordinate of an appended tuple, at offset m.

theorem Having.singleton_product {α β : Type} (a : α) (t : Multiset β) : {a} ×ˢ t = Multiset.map (fun (b : β) => (a, b)) t

theorem Having.product_map_map {α β γ δ : Type} (f : α → γ) (g : β → δ) (s : Multiset α) (t : Multiset β) : Multiset.map f s ×ˢ Multiset.map g t = Multiset.map (Prod.map f g) (s ×ˢ t)

theorem Having.filter_product {α β : Type} (p : α → Prop) [DecidablePred p] (q : β → Prop) [DecidablePred q] (s : Multiset α) (t : Multiset β) : Multiset.filter p s ×ˢ Multiset.filter q t = Multiset.filter (fun (z : α × β) => p z.1 ∧ q z.2) (s ×ˢ t)

The join chain query and its per-key evaluation

The C-fold self-join chain of the join-based rewriting, over an arity-3 base query whose columns are (group key, compared value, occurrence identifier). The identifier column materializes the tie-broken comparison <*: the chain condition compares (value, identifier) pairs lexicographically, so any injective assignment of identifiers within each group realizes an arbitrary resolution of ties between equal values – duplicate values (and duplicate whole occurrences) are fully supported.

def chainCond (C : ℕ) : Selection ℕ (3 * (C + 1) + 3)

The chain condition relating a new copy of the base query to the last copy of the chain: equal group keys and lexicographically larger (value, identifier) pair – the tie-broken comparison <*.

Equations

• One or more equations did not get rendered due to their size.

def joinChain (q : Query ℕ 3) (C : ℕ) : Query ℕ (3 * C + 3)

The C-fold self-join chain: C + 1 copies of the base query, with consecutive copies related by chainCond. Copy j occupies columns 3j, 3j + 1, 3j + 2.

Equations

• joinChain q 0 = q
• joinChain q C.succ = σ (chainCond C) (joinChain q C × q)

theorem joinChain_source (q : Query ℕ 3) (hq : q.source) (C : ℕ) : (joinChain q C).source

def chainCombine {K : Type} [CommSemiringWithMonus K] (C : ℕ) : (Tuple ℕ (3 * C + 3) × K) × Tuple ℕ 3 × K → Tuple ℕ (3 * (C + 1) + 3) × K

The combining map of one chain step: append the new copy's tuple and multiply the annotations.

Equations

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

def groupPairs {K : Type} (r : Multiset (Tuple ℕ 3 × K)) (a : ℕ) : Multiset (Lex (ℕ × ℕ) × K)

The (value, identifier) pairs of the group of key a, with their annotations: the chain-algebra view of one group of the base relation.

Equations

• One or more equations did not get rendered due to their size.

theorem joinChain_eval_filter {K : Type} [CommSemiringWithMonus K] [DecidableEq K] (q : Query ℕ 3) (hq : q.source) (d : AnnotatedDatabase ℕ K) (a C : ℕ) : Multiset.map (fun (p : AnnotatedTuple ℕ K (3 * C + 3)) => (toLex (p.1 ⟨3 * C + 1, ⋯⟩, p.1 ⟨3 * C + 2, ⋯⟩), p.2)) (Multiset.filter (fun (p : AnnotatedTuple ℕ K (3 * C + 3)) => p.1 ⟨0, ⋯⟩ = a) ((joinChain q C).evaluateAnnotated ⋯ d)) = Having.chainAgg (groupPairs (q.evaluateAnnotated hq d) a) C

Per-key evaluation of the join chain. Within the group of key a, the rows of the C-fold chain, viewed through their last (value, identifier) pair and their annotation, are exactly the annotated strictly increasing chains of length C + 1 of the group.

Assembly: the join-based query computes the fused HAVING provenance

theorem map_snd_map_pair {α β γ : Type} (f : α × β → γ) (s : Multiset (α × β)) : Multiset.map Prod.snd (Multiset.map (fun (p : α × β) => (f p, p.2)) s) = Multiset.map Prod.snd s

Mapping to the annotation ignores a rebuilt data part.

theorem perKeySum_dedup_map {α β : Type} [DecidableEq α] [AddCommMonoid β] (s : Multiset α) (F : α → β) (u : α) : (Multiset.map Prod.snd (Multiset.filter (fun (p : α × β) => p.1 = u) (Multiset.map (fun (v : α) => (v, F v)) s.dedup))).sum = if u ∈ s then F u else 0

Per-key sums over a keyed rebuild of the distinct keys.

theorem perKeySum_groupByKey {K : Type} [CommSemiringWithMonus K] [DecidableEq K] {T : Type} [ValueType T] {n : ℕ} (r : AnnotatedRelation T K n) (u : Tuple T n) : (Multiset.map Prod.snd (Multiset.filter (fun (p : Tuple T n × K) => p.1 = u) ↑↑(groupByKey r))).sum = (Multiset.map Prod.snd (Multiset.filter (fun (p : Tuple T n × K) => p.1 = u) r)).sum

Per-key annotation sums are invariant under duplicate elimination.

theorem havingGroup_pairwise_fst_lt {K T : Type} [ValueType T] [HasAltLinearOrder K] {m n₁ : ℕ} (is : Tuple (Fin m) n₁) (r : AnnotatedRelation T K m) (g : Tuple T n₁) (hnodup : (Multiset.map Prod.fst r).Nodup) : List.Pairwise (fun (p q : AnnotatedTuple T K m) => p.1 < q.1) (Having.havingGroup is r g)

Under global row-distinctness, the group sequence is strictly increasing on its tuple part.

theorem tuple3_lt_pairLt {p q : Tuple ℕ 3} (h0 : p ⟨0, ⋯⟩ = q ⟨0, ⋯⟩) (h : p < q) : toLex (p ⟨1, ⋯⟩, p ⟨2, ⋯⟩) < toLex (q ⟨1, ⋯⟩, q ⟨2, ⋯⟩)

A strict tuple inequality between arity-3 tuples with equal first column is a strict lexicographic inequality on the (second, third) column pairs.

theorem groupPairs_eq_havingGroup {K : Type} [HasAltLinearOrder K] (r : AnnotatedRelation ℕ K 3) (g : Tuple ℕ 1) : groupPairs r (g 0) = ↑(List.map (fun (p : AnnotatedTuple ℕ K 3) => (toLex (p.1 ⟨1, ⋯⟩, p.1 ⟨2, ⋯⟩), p.2)) (Having.havingGroup (fun (x : Fin 1) => ⟨0, ⋯⟩) r g))

The chain-algebra view of a group is the (value, identifier) image of the group sequence.

theorem piChain_source (q : Query ℕ 3) (hq : q.source) (C : ℕ) : ((Π fun (x : Fin 1) => #⟨0, ⋯⟩) (joinChain q C)).source

theorem q2_source (q : Query ℕ 3) (hq : q.source) (C : ℕ) : (ε ((Π fun (x : Fin 1) => #⟨0, ⋯⟩) (joinChain q C))).source

theorem Query.joinChain_count_correct {K : Type} [CommSemiringWithMonus K] [DecidableEq K] [HasAltLinearOrder K] (h_abs : absorptive K) (h_distrib : mul_sub_left_distributive K) (q : Query ℕ 3) (hq : q.source) (d : AnnotatedDatabase ℕ K) (hnodup : (Multiset.map Prod.fst (q.evaluateAnnotated hq d)).Nodup) (ts : Tuple (Term ℕ 3) 1) (C : ℕ) (g : Tuple ℕ 1) : (Multiset.map Prod.snd (Multiset.filter (fun (p : Tuple ℕ 1 × K) => p.1 = g) ((ε ((Π fun (x : Fin 1) => #⟨0, ⋯⟩) (joinChain q C))).evaluateAnnotated ⋯ d))).sum = Having.havingProv (Having.havingGroup (fun (x : Fin 1) => ⟨0, ⋯⟩) (q.evaluateAnnotated hq d) g) (ts 0) SeqAggFunc.count CompOp.ge (C + 1)

Query-level correctness of the join-based rewriting, general C. In an absorptive commutative m-semiring in which ⊗ distributes over ⊖, for every group key g, the ⊕-sum of the annotations that the join-based query ε(Π_{#0}(joinChain q C)) gives to g equals the fused HAVING COUNT(*) ≥ C + 1 predicate provenance of the group of g. The hypothesis hnodup states that the occurrence identifiers of the base query's third column make its rows pairwise distinct: it is the formal counterpart of fixing an arbitrary tie-break <* between occurrences with equal compared values, and is satisfiable for every instance (annotate each occurrence with a distinct identifier). The statement is per-key: a group with fewer than C + 1 occurrences has provenance 𝟘 on both sides – the fused operator gives its row a 𝟘 annotation while the join query simply has no row for it.

theorem filter_fst_dedup_map {α β : Type} [DecidableEq α] (s : Multiset α) (F : α → β) (u : α) : Multiset.filter (fun (p : α × β) => p.1 = u) (Multiset.map (fun (v : α) => (v, F v)) s.dedup) = if u ∈ s then {(u, F u)} else 0

One row per distinct key, at the multiset level: filtering a keyed rebuild of the distinct keys by a key.

theorem perKeySum_map_pair {α β γ : Type} [DecidableEq α] [AddCommMonoid γ] (G : α × β → γ) (s : Multiset (α × β)) (u : α) : (Multiset.map Prod.snd (Multiset.filter (fun (p : α × γ) => p.1 = u) (Multiset.map (fun (p : α × β) => (p.1, G p)) s))).sum = (Multiset.map G (Multiset.filter (fun (p : α × β) => p.1 = u) s)).sum

Per-key sums through a key-preserving rebuild of the annotations.

theorem diff_perKeySum {K : Type} [CommSemiringWithMonus K] [DecidableEq K] {T : Type} [ValueType T] {n : ℕ} (q₁ q₂ : Query T n) (h₁ : q₁.source) (h₂ : q₂.source) (hd : (ε q₁ - q₂).source) (d : AnnotatedDatabase T K) (u : Tuple T n) : (Multiset.map Prod.snd (Multiset.filter (fun (p : Tuple T n × K) => p.1 = u) ((ε q₁ - q₂).evaluateAnnotated hd d))).sum = (Multiset.map Prod.snd (Multiset.filter (fun (p : Tuple T n × K) => p.1 = u) ((ε q₁).evaluateAnnotated h₁ d))).sum - (Multiset.map Prod.snd (Multiset.filter (fun (p : Tuple T n × K) => p.1 = u) (q₂.evaluateAnnotated h₂ d))).sum

Per-key sums through Diff. When the left argument of a difference is duplicate-eliminated (one row per key), the per-key annotation sum of the difference is the monus of the two per-key sums.

def joinChainQuery (q : Query ℕ 3) (C : ℕ) : Query ℕ 1

The join-based query for COUNT(*) ≥ C + 1: project the C-fold chain to its group key and eliminate duplicates.

Equations

• joinChainQuery q C = ε ((Π fun (x : Fin 1) => #⟨0, ⋯⟩) (joinChain q C))

theorem Query.joinChainDiff_count_eq_correct {K : Type} [CommSemiringWithMonus K] [DecidableEq K] [HasAltLinearOrder K] (h_abs : absorptive K) (h_distrib : mul_sub_left_distributive K) (q : Query ℕ 3) (hq : q.source) (d : AnnotatedDatabase ℕ K) (hnodup : (Multiset.map Prod.fst (q.evaluateAnnotated hq d)).Nodup) (ts : Tuple (Term ℕ 3) 1) (C : ℕ) (g : Tuple ℕ 1) : (Multiset.map Prod.snd (Multiset.filter (fun (p : Tuple ℕ 1 × K) => p.1 = g) ((joinChainQuery q C - joinChainQuery q (C + 1)).evaluateAnnotated ⋯ d))).sum = Having.havingProv (Having.havingGroup (fun (x : Fin 1) => ⟨0, ⋯⟩) (q.evaluateAnnotated hq d) g) (ts 0) SeqAggFunc.count CompOp.eq (C + 1)

Query-level correctness for COUNT(*) = C + 1. The join-based query Q₂^{≥C+1} − Q₂^{≥C+2} gives every group key the fused COUNT(*) = C + 1 predicate provenance.

theorem Query.joinChainDiff_count_le_correct {K : Type} [CommSemiringWithMonus K] [DecidableEq K] [HasAltLinearOrder K] (h_abs : absorptive K) (h_distrib : mul_sub_left_distributive K) (q : Query ℕ 3) (hq : q.source) (d : AnnotatedDatabase ℕ K) (hnodup : (Multiset.map Prod.fst (q.evaluateAnnotated hq d)).Nodup) (ts : Tuple (Term ℕ 3) 1) (C : ℕ) (g : Tuple ℕ 1) : (Multiset.map Prod.snd (Multiset.filter (fun (p : Tuple ℕ 1 × K) => p.1 = g) ((joinChainQuery q 0 - joinChainQuery q C).evaluateAnnotated ⋯ d))).sum = Having.havingProv (Having.havingGroup (fun (x : Fin 1) => ⟨0, ⋯⟩) (q.evaluateAnnotated hq d) g) (ts 0) SeqAggFunc.count CompOp.le C

Query-level correctness for COUNT(*) ≤ C. The join-based query Q₂^{≥1} − Q₂^{≥C+1} gives every group key the fused COUNT(*) ≤ C predicate provenance.

def Query.joinCountQuery (q : Query ℕ 3) : CompOp → ℕ → Query ℕ 1

The join-based query realizing COUNT(*) op (C + 1), for each comparison operator op: chains for ≥ and >, differences of two chains for ≤, < and =, and the union of the <- and >-queries for ≠.

Equations

• q.joinCountQuery CompOp.lt x✝ = (joinChainQuery q 0 - joinChainQuery q x✝)
• q.joinCountQuery CompOp.le x✝ = (joinChainQuery q 0 - joinChainQuery q (x✝ + 1))
• q.joinCountQuery CompOp.eq x✝ = (joinChainQuery q x✝ - joinChainQuery q (x✝ + 1))
• q.joinCountQuery CompOp.ne x✝ = ((joinChainQuery q 0 - joinChainQuery q x✝) ⊎ joinChainQuery q (x✝ + 1))
• q.joinCountQuery CompOp.ge x✝ = joinChainQuery q x✝
• q.joinCountQuery CompOp.gt x✝ = joinChainQuery q (x✝ + 1)

theorem Query.joinCountQuery_source (q : Query ℕ 3) (hq : q.source) (op : CompOp) (C : ℕ) : (q.joinCountQuery op C).source

theorem sum_perKeySum {K : Type} [CommSemiringWithMonus K] [DecidableEq K] {T : Type} [ValueType T] {n : ℕ} (q₁ q₂ : Query T n) (h₁ : q₁.source) (h₂ : q₂.source) (hs : (q₁ ⊎ q₂).source) (d : AnnotatedDatabase T K) (u : Tuple T n) : (Multiset.map Prod.snd (Multiset.filter (fun (p : Tuple T n × K) => p.1 = u) ((q₁ ⊎ q₂).evaluateAnnotated hs d))).sum = (Multiset.map Prod.snd (Multiset.filter (fun (p : Tuple T n × K) => p.1 = u) (q₁.evaluateAnnotated h₁ d))).sum + (Multiset.map Prod.snd (Multiset.filter (fun (p : Tuple T n × K) => p.1 = u) (q₂.evaluateAnnotated h₂ d))).sum

Per-key annotation sums are additive across Query.Sum.

theorem Query.joinCount_correct {K : Type} [CommSemiringWithMonus K] [DecidableEq K] [HasAltLinearOrder K] (h_abs : absorptive K) (h_distrib : mul_sub_left_distributive K) (q : Query ℕ 3) (hq : q.source) (d : AnnotatedDatabase ℕ K) (hnodup : (Multiset.map Prod.fst (q.evaluateAnnotated hq d)).Nodup) (ts : Tuple (Term ℕ 3) 1) (op : CompOp) (C : ℕ) (g : Tuple ℕ 1) : (Multiset.map Prod.snd (Multiset.filter (fun (p : Tuple ℕ 1 × K) => p.1 = g) ((q.joinCountQuery op C).evaluateAnnotated ⋯ d))).sum = Having.havingProv (Having.havingGroup (fun (x : Fin 1) => ⟨0, ⋯⟩) (q.evaluateAnnotated hq d) g) (ts 0) SeqAggFunc.count op (C + 1)

Query-level correctness of the JOIN rewriting for COUNT(*), for any comparison operator. For every op ∈ {<, ≤, =, ≠, ≥, >}, every threshold C + 1 ≥ 1 and every group key, in an absorptive commutative m-semiring whose ⊗ distributes over ⊖, the join-based query Query.joinCountQuery q op C gives the group key the fused COUNT(*) op (C + 1) predicate provenance.

Home · Documentation · Publications · Contributors · Source · Cite