Query-level counterexamples for the HAVING / JOIN correspondence

The correspondence between the possible-world semantics of HAVING comparisons on COUNT(*) and the JOIN-based rewriting holds in commutative m-semirings that are absorptive and whose ⊗ distributes over ⊖. This file witnesses, at the level of queries evaluated on concrete annotated databases (not merely of the underlying algebraic identities), that both hypotheses are needed. All facts are checked by decide.

The instances share the base relation R(g, v) of arity 2, grouped by the first column; on the fused side the query is the general HAVING site for COUNT(*) op C and on the join side the queries are

• Q₂^{≥1} = ε(Π_{#0}(R)),
• Q₂^{≥2} = ε(Π_{#0}(σ_{#0=#2 ∧ #1<#3}(R × R))), and
• Q₂^{=1} = Q₂^{≥1} - Q₂^{≥2},

the tie-broken comparison of the general construction degenerating to the plain < because the second attributes of the instances are pairwise distinct. The fused operator's output carries the group key and the aggregate value while the join queries return the key only, so the comparison is on the multisets of annotations.

• Distributivity is needed (HavingQueryCounterexamples.ChainFive.query_counterexample): in the five-element chain semiring – absorptive, hence idempotent, but not ⊗-over-⊖ distributive (ChainFive.not_mul_sub_left_distributive) – with annotations (mid, hi, hi) on one group, COUNT(*) = 1 yields annotation hi on the fused side but 𝟘 on the join side.

• Absorptivity is needed (HavingQueryCounterexamples.TropicalZ.query_counterexample): in the tropical semiring over ℤ ∪ {∞} – idempotent and distributive (TropicalZ.mul_sub_left_distributive) but not absorptive (TropicalZ.not_absorptive_witness) – with two occurrences annotated trop (-1) in one group, COUNT(*) ≥ 1 yields annotation trop (-2) on the fused side but trop (-1) on the join side.

def HavingQueryCounterexamples.qR : Query ℕ 2

The two-column base relation R(g, v).

Equations

• HavingQueryCounterexamples.qR = Query.Rel 2 "R"

def HavingQueryCounterexamples.qgR : AggQuery ℕ 2 (ColKind.allReg 2)

The same base relation as a general query, for the HAVING site.

Equations

• HavingQueryCounterexamples.qgR = AggQuery.Rel 2 "R"

def HavingQueryCounterexamples.q2ge1 : Query ℕ 1

Q₂^{≥1} = ε(Π_{#0}(R)).

Equations

• HavingQueryCounterexamples.q2ge1 = ε (Π ![#0] HavingQueryCounterexamples.qR)

def HavingQueryCounterexamples.q2ge2 : Query ℕ 1

Q₂^{≥2} = ε(Π_{#0}(σ_{#0=#2 ∧ #1<#3}(R × R))).

Equations

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

def HavingQueryCounterexamples.q2eq1 : Query ℕ 1

Q₂^{=1} = Q₂^{≥1} - Q₂^{≥2}.

Equations

• HavingQueryCounterexamples.q2eq1 = (HavingQueryCounterexamples.q2ge1 - HavingQueryCounterexamples.q2ge2)

Distributivity is needed: the ChainFive instance

def HavingQueryCounterexamples.dC : AnnotatedDatabase ℕ ChainFive

One group with key 0, values 1, 2, 3, annotations mid, hi, hi.

Equations

• HavingQueryCounterexamples.dC = [("R", ⟨2, {(![0, 1], ChainFive.mid), (![0, 2], ChainFive.hi), (![0, 3], ChainFive.hi)}⟩)]

theorem HavingQueryCounterexamples.chainFive_fused : Multiset.map (fun (p : AnnotatedTuple ℕ ChainFive (Nat.succ 0 + Nat.succ 0)) => p.2) ((AggQuery.havingSite ![0] ![#1] ![SeqAggFunc.count] CompOp.eq 0 (Term.const 1) qgR).evaluateAnnotated dC) = {ChainFive.hi}

Fused side: COUNT(*) = 1 has predicate provenance hi (each singleton world contributes its own annotation, the factored discarded-occurrence factor 𝟙 ⊖ hi being 𝟙 in the chain).

theorem HavingQueryCounterexamples.chainFive_join : Multiset.map (fun (p : AnnotatedTuple ℕ ChainFive 1) => p.2) (q2eq1.evaluateAnnotated ⋯ dC) = {0}

Join side: Q₂^{=1} has annotation 𝟘 (hi ⊖ hi).

theorem HavingQueryCounterexamples.ChainFive.query_counterexample : Multiset.map (fun (p : AnnotatedTuple ℕ ChainFive (Nat.succ 0 + Nat.succ 0)) => p.2) ((AggQuery.havingSite ![0] ![#1] ![SeqAggFunc.count] CompOp.eq 0 (Term.const 1) qgR).evaluateAnnotated dC) ≠ Multiset.map (fun (p : AnnotatedTuple ℕ ChainFive 1) => p.2) (q2eq1.evaluateAnnotated ⋯ dC)

Query-level part of the distributivity necessity: in the absorptive but non-distributive ChainFive, the fused COUNT(*) = 1 query and its join-based rewriting disagree on a concrete instance.

Absorptivity is needed: the tropical instance over ℤ ∪ {∞}

theorem HavingQueryCounterexamples.TropicalZ.not_absorptive_witness : 1 + Tropical.trop ↑(-1) ≠ 1

The tropical semiring over ℤ ∪ {∞} is not absorptive: 𝟙 ⊕ trop (-1) = trop (-1) ≠ 𝟙.

theorem HavingQueryCounterexamples.TropicalZ.mul_sub_left_distributive : _root_.mul_sub_left_distributive (Tropical (WithTop ℤ))

The tropical semiring over ℤ ∪ {∞} is ⊗-over-⊖ distributive.

noncomputable def HavingQueryCounterexamples.dZ : AnnotatedDatabase ℕ (Tropical (WithTop ℤ))

One group with key 0, values 1, 2, both annotated trop (-1).

Equations

• HavingQueryCounterexamples.dZ = [("R", ⟨2, {(![0, 1], Tropical.trop ↑(-1)), (![0, 2], Tropical.trop ↑(-1))}⟩)]

theorem HavingQueryCounterexamples.tropicalZ_fused : Multiset.map (fun (p : AnnotatedTuple ℕ (Tropical (WithTop ℤ)) (Nat.succ 0 + Nat.succ 0)) => p.2) ((AggQuery.havingSite ![0] ![#1] ![SeqAggFunc.count] CompOp.ge 0 (Term.const 1) qgR).evaluateAnnotated dZ) = {Tropical.trop ↑(-2)}

Fused side: COUNT(*) ≥ 1 has predicate provenance trop (-2): the two singleton worlds have annotation trop (-1) ⊗ (𝟙 ⊖ trop (-1)) = 𝟘, and only the full world trop (-1) ⊗ trop (-1) = trop (-2) survives.

theorem HavingQueryCounterexamples.tropicalZ_join : Multiset.map (fun (p : AnnotatedTuple ℕ (Tropical (WithTop ℤ)) 1) => p.2) (q2ge1.evaluateAnnotated ⋯ dZ) = {Tropical.trop ↑(-1)}

Join side: Q₂^{≥1} has annotation trop (-1) ⊕ trop (-1) = trop (-1).

theorem HavingQueryCounterexamples.TropicalZ.query_counterexample : Multiset.map (fun (p : AnnotatedTuple ℕ (Tropical (WithTop ℤ)) (Nat.succ 0 + Nat.succ 0)) => p.2) ((AggQuery.havingSite ![0] ![#1] ![SeqAggFunc.count] CompOp.ge 0 (Term.const 1) qgR).evaluateAnnotated dZ) ≠ Multiset.map (fun (p : AnnotatedTuple ℕ (Tropical (WithTop ℤ)) 1) => p.2) (q2ge1.evaluateAnnotated ⋯ dZ)

Query-level part of the absorptivity necessity: in the idempotent and distributive but non-absorptive tropical semiring over ℤ ∪ {∞}, the fused COUNT(*) ≥ 1 query and its join-based rewriting disagree on a concrete instance. Same phenomenon as the algebra-level TropicalR.F_ne_S, here at the level of evaluated queries.

Home · Documentation · Publications · Contributors · Source · Cite