Compositional correctness of the JOIN rewriting for HAVING COUNT(*)

Provenance.HavingQueryCorrectness proves the join-based rewriting of a HAVING COUNT(*) op (C+1) correct extensionally: per group key, the sum of the annotations of the join query's rows is the fused predicate provenance. This file upgrades that to an intensional, multiset-level equality, the form needed to substitute the rewriting for the fused operator inside an arbitrary surrounding query.

The one obstruction to multiset-level equality is the failing groups: the fused operator emits a 𝟘-annotated row for a group that fails the comparison, while the join query emits no row at all. The rewriting is therefore padded: joinCountQueryPadded adds to the join query the self-difference keysQuery q ∖ keysQuery q – one 𝟘-annotated row per group key – and duplicate-eliminates the union, which merges everything into exactly one row per group key carrying the summed annotation. The result (joinCountQueryPadded_correct) is equal as a multiset of annotated tuples to the key projection of the fused HAVING output (proj_fused_eq_keyed), so the substitution is transparent to every surrounding operator – including annotation-sensitive ones like Diff and further HAVINGs, which are not congruences for the naive “equal up to 𝟘-rows” relation (a 𝟘-annotated row still changes the deterministic aggregate values of an enclosing group).

@[instance_reducible]

instance instMembershipAnnotatedTupleAnnotatedRelation {T K : Type} {n : ℕ} : Membership (AnnotatedTuple T K n) (AnnotatedRelation T K n)

AnnotatedRelation is an opaque def over Multiset, so instance search does not see the multiset membership through it; register it.

Equations

• instMembershipAnnotatedTupleAnnotatedRelation = { mem := instMembershipAnnotatedTupleAnnotatedRelation._aux_1 }

The padded join query

def keyIdx : Tuple (Fin 3) 1

The canonical key selector of the (key, value, identifier) base schema.

Equations

• keyIdx x✝ = ⟨0, keyIdx._proof_2⟩

def keyTerm : Tuple (Term ℕ 3) 1

The key column, as a projection term.

Equations

• keyTerm x✝ = #⟨0, keyIdx._proof_2⟩

def keyOf {K : Type} (p : AnnotatedTuple ℕ K 3) : Tuple ℕ 1

The group key of an annotated base row.

Equations

• keyOf p x✝ = p.1 ⟨0, keyIdx._proof_2⟩

def keysQuery (q : Query ℕ 3) : Query ℕ 1

One row per distinct group key, annotated by the ⊕-sum of the group's annotations.

Equations

• keysQuery q = ε (Π keyTerm q)

def zeroPadQuery (q : Query ℕ 3) : Query ℕ 1

One 𝟘-annotated row per distinct group key: the self-difference of the key query (α ⊖ α = 𝟘).

Equations

• zeroPadQuery q = (keysQuery q - keysQuery q)

def joinCountQueryPadded (q : Query ℕ 3) (op : CompOp) (C : ℕ) : Query ℕ 1

The padded join-based rewriting of HAVING COUNT(*) op (C + 1): the join query, padded with a 𝟘-annotated row per group key and duplicate-eliminated into one row per group key.

Equations

• joinCountQueryPadded q op C = ε (q.joinCountQuery op C ⊎ zeroPadQuery q)

theorem keysQuery_source (q : Query ℕ 3) (hq : q.source) : (keysQuery q).source

theorem zeroPadQuery_source (q : Query ℕ 3) (hq : q.source) : (zeroPadQuery q).source

theorem joinCountQueryPadded_source (q : Query ℕ 3) (hq : q.source) (op : CompOp) (C : ℕ) : (joinCountQueryPadded q op C).source

Key bookkeeping

theorem joinChain_key_mem {K : Type} [CommSemiringWithMonus K] [DecidableEq K] (q : Query ℕ 3) (hq : q.source) (d : AnnotatedDatabase ℕ K) (C : ℕ) (x : AnnotatedTuple ℕ K (3 * C + 3)) : x ∈ (joinChain q C).evaluateAnnotated ⋯ d → ∃ p ∈ q.evaluateAnnotated hq d, x.1 ⟨0, ⋯⟩ = p.1 ⟨0, ⋯⟩

Every row of the join chain carries the key of some base row in its key coordinate.

theorem keyed_fst {K : Type} [CommSemiringWithMonus K] [DecidableEq K] (q : Query ℕ 3) (hq : q.source) (d : AnnotatedDatabase ℕ K) : Multiset.map Prod.fst ((Π keyTerm q).evaluateAnnotated hq d) = Multiset.map keyOf (q.evaluateAnnotated hq d)

The key multiset of the base query, through the key projection.

theorem joinChainQuery_key_mem {K : Type} [CommSemiringWithMonus K] [DecidableEq K] (q : Query ℕ 3) (hq : q.source) (d : AnnotatedDatabase ℕ K) (C : ℕ) (x : AnnotatedTuple ℕ K 1) (hx : x ∈ (joinChainQuery q C).evaluateAnnotated ⋯ d) : x.1 ∈ (Multiset.map keyOf (q.evaluateAnnotated hq d)).dedup

Every row of the chain-projected key query carries a key of the base query.

theorem diff_row_mem {K : Type} [CommSemiringWithMonus K] [DecidableEq K] (q₁ q₂ : Query ℕ 1) (h₁ : q₁.source) (hd : (q₁ - q₂).source) (d : AnnotatedDatabase ℕ K) (y : AnnotatedTuple ℕ K 1) (hy : y ∈ (q₁ - q₂).evaluateAnnotated hd d) : ∃ z ∈ q₁.evaluateAnnotated h₁ d, y.1 = z.1

Rows of a difference keep the data parts of its left argument.

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

Every row of the join-based query, for any comparison operator, carries a key of the base query.

Evaluation of the padding

theorem keysQuery_eval {K : Type} [CommSemiringWithMonus K] [DecidableEq K] (q : Query ℕ 3) (hq : q.source) (d : AnnotatedDatabase ℕ K) : (keysQuery q).evaluateAnnotated ⋯ d = Multiset.map (fun (u : Tuple ℕ 1) => (u, (Multiset.map Prod.snd (Multiset.filter (fun (p : AnnotatedTuple ℕ K 1) => p.1 = u) ((Π keyTerm q).evaluateAnnotated hq d))).sum)) (Multiset.map keyOf (q.evaluateAnnotated hq d)).dedup

The key query evaluates to one row per distinct key with the summed annotation.

theorem zeroPadQuery_eval {K : Type} [CommSemiringWithMonus K] [DecidableEq K] (q : Query ℕ 3) (hq : q.source) (d : AnnotatedDatabase ℕ K) : (zeroPadQuery q).evaluateAnnotated ⋯ d = Multiset.map (fun (u : Tuple ℕ 1) => (u, 0)) (Multiset.map keyOf (q.evaluateAnnotated hq d)).dedup

The padding query evaluates to one 𝟘-annotated row per distinct key.

Site correctness: the padded rewriting, row for row

theorem joinCountQueryPadded_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 : ℕ) : (joinCountQueryPadded q op C).evaluateAnnotated ⋯ d = Multiset.map (fun (g : Tuple ℕ 1) => (g, Having.havingProv (Having.havingGroup keyIdx (q.evaluateAnnotated hq d) g) (ts 0) SeqAggFunc.count op (C + 1))) (Multiset.map keyOf (q.evaluateAnnotated hq d)).dedup

Multiset-level correctness of the padded JOIN rewriting. In an absorptive commutative m-semiring whose ⊗ distributes over ⊖, the padded join-based query evaluates to exactly – row for row, annotation for annotation – one row per group key of the base query, annotated with the fused COUNT(*) op (C + 1) predicate provenance. The sole hypothesis is the injective per-group occurrence identifiers (global row-distinctness of the base query's output).

theorem fused_key_proj {K : Type} [CommSemiringWithMonus K] [DecidableEq K] [HasAltLinearOrder K] (qg : AggQuery ℕ 3 (ColKind.allReg 3)) (q : Query ℕ 3) (hq : q.source) (d : AnnotatedDatabase ℕ K) (hin : qg.evaluateAnnotated d = q.evaluateAnnotated hq d) (ts' : Tuple (Term ℕ 3) 1) (op : CompOp) (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.count) op 0 (Term.const (C + 1)) qg).evaluateAnnotated d) = Multiset.map (fun (g : Tuple ℕ 1) => (g, Having.havingProv (Having.havingGroup keyIdx (q.evaluateAnnotated hq d) g) (ts' 0) SeqAggFunc.count op (C + 1))) (Multiset.map keyOf (q.evaluateAnnotated hq d)).dedup

The key-projected fused output. Projecting the fused HAVING COUNT(*) op (C + 1) site output to its group key yields the same one-row-per-key relation the padded join query evaluates to: combined with joinCountQueryPadded_correct, the padded rewriting can be substituted for the key-projected fused operator inside any surrounding query.

theorem countHaving_site_rewrite {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 : ℕ) : 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.count) op 0 (Term.const (C + 1)) (q.toAgg hq)).evaluateAnnotated d) = (joinCountQueryPadded q op C).evaluateAnnotated ⋯ d

Site substitution. The key-projected fused HAVING COUNT(*) op (C + 1) site over the embedded classical query and the padded join-based rewriting evaluate to the same multiset of annotated tuples: substituting one for the other inside any surrounding query preserves the annotated semantics verbatim.

Home · Documentation · Publications · Contributors · Source · Cite