Possible-world semantics of the fused Having operator

This file gives the K-annotated semantics of the fused HAVING operator Query.Having – a grouping γ^≼ whose output is filtered by a comparison between an aggregate value and a regular term – in an arbitrary commutative m-semiring, together with the bridge between its possible worlds and the Finset-of-positions representation on which the algebraic development of Provenance.Having and Provenance.HavingMinMax is built.

Possible worlds

The occurrences of a group are extracted as a sequence U (a list of annotated tuples, ordered by the canonical lexicographic order – the ordering ≼ along which non-commutative aggregates read their input, with an arbitrary fixed tie-break on the annotations). A possible world of U is a subsequence W ⊑ U; its annotation is, in factored form,

ann_U(W) = (⊗_{(u,α) ∈ W} α) ⊗ (𝟙 ⊖ ⊕_{(u,α) ∈ U∖W} α).

The bridge

Formally, worlds are represented as sets of positions W : Finset (Fin U.length); seqOf U W is the subsequence of U they select. This representation is faithful: seqOf U W is always a sublist of U (seqOf_sublist), every sublist arises this way (sublist_eq_seqOf), and when the occurrences of U are pairwise distinct the correspondence is a bijection (seqOf_injective). Because annotations and aggregate values factor through positions, the possible-world ⊕-sum below is taken over Finset (Fin U.length) – which is exactly the index representation used by Provenance.Having – and the whole algebraic development attaches to the semantics through worldAnn_eq_T and havingProv_eq_prov.

The semantics

For a group with occurrence sequence U and an atomic aggregate comparison f(t) op s, the predicate provenance is

⊕_{∅ ≠ W ⊑ U} ann_U(W) ⊗ χ_op(agg_{t,f}(W), s(g)),

where agg_{t,f}(W) applies the sequence aggregate f to the t-values of the occurrences of W (in order) and χ_op sends a true comparison to 𝟙 and a false one to 𝟘. The sum ranges over non-empty worlds only, so it already enforces group existence. The general evaluator's HAVING site (AggQuery.havingSite, in Provenance.AggQueryBridges) has exactly this closed form: one row per group of the inner query, whose data part carries the group key and the (whole-group) aggregate values, and whose annotation is the predicate provenance of its group. Boolean combinations of aggregate comparisons are interpreted by HavingPred.prov: ∧ ↦ ⊗, ∨ ↦ ⊕, and ¬ is pushed to the atoms by De Morgan duality, complementing the comparison operator of an atom (as in ProvSQL's implementation).

Positions and subsequences: the bridge

def Having.seqOf {β : Type} (U : List β) : Finset (Fin U.length) → List β

The subsequence of U selected by a set of positions, in order.

Equations

• Having.seqOf [] x_2 = []
• Having.seqOf (a :: U) W = (if 0 ∈ W then [a] else []) ++ Having.seqOf U {i : Fin U.length | i.succ ∈ W}

theorem Having.seqOf_sublist {β : Type} (U : List β) (W : Finset (Fin U.length)) : (seqOf U W).Sublist U

A set of positions selects a sublist.

theorem Having.sublist_eq_seqOf {β : Type} {U L : List β} (h : L.Sublist U) : ∃ (W : Finset (Fin U.length)), seqOf U W = L

Every sublist is selected by some set of positions.

theorem Having.seqOf_length {β : Type} (U : List β) (W : Finset (Fin U.length)) : (seqOf U W).length = W.card

The length of the selected subsequence is the number of selected positions: Finset.card is the COUNT aggregate of the bridge.

theorem Having.seqOf_injective {β : Type} {U : List β} : U.Nodup → Function.Injective (seqOf U)

Under occurrence-uniqueness (U.Nodup), the position representation is faithful: distinct sets of positions select distinct subsequences.

The world annotation, in factored form

def Having.worldAnn {K : Type} [CommSemiringWithMonus K] {N : ℕ} (α : Fin N → K) (W : Finset (Fin N)) : K

The K-annotation of a possible world, in the factored form of the possible-world semantics: the product of the annotations of the kept occurrences times 𝟙 ⊖ the sum of the annotations of the discarded ones. worldAnn_eq_T normalizes it into the Having.T form used by the algebraic development.

Equations

• Having.worldAnn α W = (∏ i ∈ W, α i) * (1 - ∑ i ∈ Wᶜ, α i)

theorem Having.worldAnn_eq_T {K : Type} [CommSemiringWithMonus K] (h_distrib : mul_sub_left_distributive K) {N : ℕ} (α : Fin N → K) (W : Finset (Fin N)) : worldAnn α W = T α Finset.univ W

In an m-semiring where ⊗ left-distributes over ⊖, the factored world annotation coincides with the exactly-W contribution Having.T over the full universe of positions. This is the only place the distributivity hypothesis enters the correspondence between the semantics and the query-free algebra; cf. ChainFive, where the two forms differ.

Group extraction and aggregate values

theorem Having.foldr_sortedInsert_coe {α' : Type} [LinearOrder α'] (s : Multiset α') : ↑↑(Multiset.foldr sortedInsert ⟨[], ⋯⟩ s) = s

Folding sortedInsert over a multiset sorts it without changing its elements: the underlying multiset of the resulting list is the original multiset. (Multiset.sort would serve the same purpose but is defined by well-founded recursion and does not reduce in the kernel.)

def Having.havingGroup {T : Type} [ValueType T] {K : Type} {m n₁ : ℕ} [HasAltLinearOrder K] (is : Tuple (Fin m) n₁) (r : AnnotatedRelation T K m) (g : Tuple T n₁) : List (AnnotatedTuple T K m)

The occurrence sequence U^≼ of the group of key g: the annotated tuples of r whose grouping columns match g, as a list sorted by the lexicographic order on annotated tuples – by the canonical order on the value part first (the ordering ≼ along which the group sequence is read), then by the alternative order of HasAltLinearOrder on the annotation, an arbitrary fixed tie-break, matching the possible-world semantics where occurrences with equal value parts are ordered arbitrarily.

Equations

• Having.havingGroup is r g = ↑(Multiset.foldr sortedInsert ⟨[], ⋯⟩ (Multiset.filter (fun (p : AnnotatedTuple T K m) => ∀ (k' : Fin n₁), p.1 (is k') = g k') r))

theorem Having.havingGroup_coe {T : Type} [ValueType T] {K : Type} {m n₁ : ℕ} [HasAltLinearOrder K] (is : Tuple (Fin m) n₁) (r : AnnotatedRelation T K m) (g : Tuple T n₁) : ↑(havingGroup is r g) = Multiset.filter (fun (p : AnnotatedTuple T K m) => ∀ (k' : Fin n₁), p.1 (is k') = g k') r

The group sequence is a permutation of the group multiset: as a multiset, havingGroup is r g is the sub-multiset of r matching the key g.

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

The group sequence is sorted: on consecutive occurrences, the tuple part is strictly increasing or equal (ties on the tuple part being broken by the alternative order on the annotations).

def Having.aggValOn {T : Type} [ValueType T] {K : Type} {m : ℕ} (U : List (AnnotatedTuple T K m)) (t : Term T m) (f : SeqAggFunc T) (W : Finset (Fin U.length)) : T

The aggregate value of f over the term t in the world W: f applied to the sequence of t-values of the kept occurrences, in order. No algebraic structure on f is required.

Equations

• Having.aggValOn U t f W = f (List.map (fun (p : AnnotatedTuple T K m) => t.eval p.1) (Having.seqOf U W))

Predicate provenance

def Having.chi {T : Type} [ValueType T] {K : Type} [CommSemiringWithMonus K] (op : CompOp) (a b : T) : K

χ_op: the characteristic value of a comparison, 𝟙 if it holds and 𝟘 otherwise.

Equations

• Having.chi op a b = if op.eval a b then 1 else 0

def Having.havingProv {T : Type} [ValueType T] {K : Type} [CommSemiringWithMonus K] {m : ℕ} (U : List (AnnotatedTuple T K m)) (t : Term T m) (f : SeqAggFunc T) (op : CompOp) (c : T) : K

Predicate provenance of an atomic aggregate comparison on the occurrence sequence U of one group: the ⊕-sum, over the non-empty possible worlds of U, of the world annotation times the characteristic value of the comparison between the aggregate value in the world and the regular value c. The sum ranges over non-empty worlds only: it thereby already enforces group existence, which is why the fused selection semantics drops the annotation of the grouped row itself.

Equations

• Having.havingProv U t f op c = ∑ W : Finset (Fin U.length) with W.Nonempty, Having.worldAnn (fun (i : Fin U.length) => (U.get i).2) W * Having.chi op (Having.aggValOn U t f W) c

theorem Having.havingProv_eq_prov {T : Type} [ValueType T] {K : Type} [CommSemiringWithMonus K] {m : ℕ} (h_distrib : mul_sub_left_distributive K) (U : List (AnnotatedTuple T K m)) (t : Term T m) (f : SeqAggFunc T) (op : CompOp) (c : T) : havingProv U t f op c = prov (fun (i : Fin U.length) => (U.get i).2) Finset.univ fun (W : Finset (Fin U.length)) => op.eval (aggValOn U t f W) c

Attachment of the algebra to the semantics. In an m-semiring where ⊗ left-distributes over ⊖, the predicate provenance is exactly the possible-world provenance Having.prov of the predicate “f(t) op c holds in the world”, over the universe of positions of U annotated by the occurrence annotations. All the collapse results of Provenance.Having and Provenance.HavingMinMax (F_eq_S, G_eq_S_monus_S, collapse_to_minimal, minScan_correct …) thereby apply to the fused operator's semantics.

theorem Having.aggValOn_count {K : Type} {m : ℕ} (U : List (AnnotatedTuple ℕ K m)) (t : Term ℕ m) (W : Finset (Fin U.length)) : aggValOn U t SeqAggFunc.count W = W.card

The COUNT(*) specialization: on the world W, the sequence aggregate List.length computes |W|, so a COUNT comparison depends on the world only through its cardinality. Together with havingProv_eq_prov this attaches the Having.F/Having.G algebra to the fused semantics.

theorem Having.havingProv_count_ge {K : Type} [CommSemiringWithMonus K] {m : ℕ} (h_abs : absorptive K) (h_distrib : mul_sub_left_distributive K) (U : List (AnnotatedTuple ℕ K m)) (t : Term ℕ m) (C : ℕ) : havingProv U t SeqAggFunc.count CompOp.ge (C + 1) = S (fun (i : Fin U.length) => (U.get i).2) Finset.univ (C + 1)

COUNT(*) ≥ C case of the fused semantics. In an absorptive m-semiring with ⊗ distributive over ⊖, the predicate provenance of COUNT(*) ≥ C + 1 on the group sequence U is the possible-world provenance Having.F – hence, by Having.F_eq_S, the join-side Having.S, the ⊕-sum of the monomials of the worlds of size exactly C + 1.

theorem Having.havingProv_count_eq {K : Type} [CommSemiringWithMonus K] {m : ℕ} (h_distrib : mul_sub_left_distributive K) (U : List (AnnotatedTuple ℕ K m)) (t : Term ℕ m) (C : ℕ) : havingProv U t SeqAggFunc.count CompOp.eq (C + 1) = G (fun (i : Fin U.length) => (U.get i).2) Finset.univ (C + 1)

COUNT(*) = C case of the fused semantics. The predicate provenance of COUNT(*) = C + 1 is Having.G – hence, by Having.G_eq_S_monus_S, the join-side difference S_{C+1} ⊖ S_{C+2}.

theorem Having.havingProv_count_le {K : Type} [CommSemiringWithMonus K] {m : ℕ} (h_distrib : mul_sub_left_distributive K) (U : List (AnnotatedTuple ℕ K m)) (t : Term ℕ m) (C : ℕ) : havingProv U t SeqAggFunc.count CompOp.le C = ∑ W ∈ Finset.univ.powerset with 1 ≤ W.card ∧ W.card ≤ C, T (fun (i : Fin U.length) => (U.get i).2) Finset.univ W

COUNT(*) ≤ C case of the fused semantics. The predicate provenance of COUNT(*) ≤ C is the ⊕-sum of world annotations over the worlds of size between 1 and C – hence, by Having.atMost_eq_S_monus_S, the join-side difference S_1 ⊖ S_{C+1}.

theorem Having.havingProv_count_gt {K : Type} [CommSemiringWithMonus K] {m : ℕ} (U : List (AnnotatedTuple ℕ K m)) (t : Term ℕ m) (c : ℕ) : havingProv U t SeqAggFunc.count CompOp.gt c = havingProv U t SeqAggFunc.count CompOp.ge (c + 1)

COUNT(*) > c is COUNT(*) ≥ c + 1.

theorem Having.havingProv_count_lt {K : Type} [CommSemiringWithMonus K] {m : ℕ} (U : List (AnnotatedTuple ℕ K m)) (t : Term ℕ m) (c : ℕ) : havingProv U t SeqAggFunc.count CompOp.lt (c + 1) = havingProv U t SeqAggFunc.count CompOp.le c

COUNT(*) < c + 1 is COUNT(*) ≤ c.

theorem Having.havingProv_ne_split {T : Type} [ValueType T] {K : Type} [CommSemiringWithMonus K] {m : ℕ} (U : List (AnnotatedTuple T K m)) (t : Term T m) (f : SeqAggFunc T) (c : T) : havingProv U t f CompOp.ne c = havingProv U t f CompOp.lt c + havingProv U t f CompOp.gt c

The ≠ comparison splits. For any aggregate and any m-semiring, the predicate provenance of f(t) ≠ c is the ⊕-sum of those of f(t) < c and f(t) > c: the characteristic values agree world by world, by trichotomy of the linear order on the value domain.

theorem Having.havingProv_count_ge_one {K : Type} [CommSemiringWithMonus K] {m : ℕ} (h_abs : absorptive K) (h_distrib : mul_sub_left_distributive K) (U : List (AnnotatedTuple ℕ K m)) (t : Term ℕ m) : havingProv U t SeqAggFunc.count CompOp.ge 1 = (List.map (fun (p : AnnotatedTuple ℕ K m) => p.2) U).sum

COUNT(*) ≥ 1 collapses to the group annotation sum. In an absorptive m-semiring with ⊗ distributive over ⊖, the fused COUNT(*) ≥ 1 predicate provenance of a group sequence is the ⊕-sum of the annotations of its occurrences (the C = 1 instance of the join correspondence: S_1 is the sum of the singleton monomials).

Boolean combinations of aggregate comparisons

inductive HavingPred (T : Type) (m n₁ : ℕ) : Type

Boolean combinations of fused aggregate comparisons: atoms compare a sequence aggregate of a term over the group to a regular term over the group key; combinations are negation, conjunction and disjunction.

• cmp {T : Type} {m n₁ : ℕ} : Term T m → SeqAggFunc T → CompOp → Term T n₁ → HavingPred T m n₁
• not {T : Type} {m n₁ : ℕ} : HavingPred T m n₁ → HavingPred T m n₁
• and {T : Type} {m n₁ : ℕ} : HavingPred T m n₁ → HavingPred T m n₁ → HavingPred T m n₁
• or {T : Type} {m n₁ : ℕ} : HavingPred T m n₁ → HavingPred T m n₁ → HavingPred T m n₁

def HavingPred.provAux {T : Type} [ValueType T] {K : Type} [CommSemiringWithMonus K] {m n₁ : ℕ} (U : List (AnnotatedTuple T K m)) (g : Tuple T n₁) (negated : Bool) : HavingPred T m n₁ → K

Worker for HavingPred.prov, carrying the polarity of the enclosing negations (mirroring ProvSQL's rewriting of HAVING predicates, which pushes NOT through Boolean combinations by De Morgan duality and complements the comparison operator at the leaves). Under negated, conjunction becomes ⊕, disjunction becomes ⊗, and an atom's operator is complemented; since χ_op is {𝟘, 𝟙}-valued, complementing the operator is the same as interpreting ¬ world-wise inside the possible-world sum, which keeps the nonempty-world guard (an outer 𝟙 ⊖ · interpretation would instead hold on worlds where the group is empty, although the grouping outputs no row there).

Equations

• One or more equations did not get rendered due to their size.
• HavingPred.provAux U g negated (HavingPred.cmp t f op s) = Having.havingProv U t f (if negated = true then op.negate else op) (s.eval g)
• HavingPred.provAux U g negated ψ.not = HavingPred.provAux U g (!negated) ψ

def HavingPred.prov {T : Type} [ValueType T] {K : Type} [CommSemiringWithMonus K] {m n₁ : ℕ} (U : List (AnnotatedTuple T K m)) (g : Tuple T n₁) (ψ : HavingPred T m n₁) : K

Predicate provenance of a Boolean combination of aggregate comparisons, on the occurrence sequence U of the group of key g: conjunction is interpreted by ⊗, disjunction by ⊕, and negation by pushing it to the atoms (De Morgan duality, complementing the comparison operator of an atom), as ProvSQL does.

Equations

• HavingPred.prov U g ψ = HavingPred.provAux U g false ψ

def HavingPred.holdsOnSeq {T : Type} [ValueType T] {m n₁ : ℕ} (L : List (Tuple T m)) (g : Tuple T n₁) : HavingPred T m n₁ → Prop

Classical satisfaction of a Boolean combination of aggregate comparisons on a plain occurrence sequence L (the tuples of one group, in ≼-order) with group key g: an atom applies the sequence aggregate to the t-values of L and compares with the regular term evaluated on the key; ∧, ∨ and ¬ are classical. This is the reading of the HAVING predicate on one possible world.

Equations

• HavingPred.holdsOnSeq L g (HavingPred.cmp t f op s) = op.eval (f (List.map t.eval L)) (s.eval g)
• HavingPred.holdsOnSeq L g ψ.not = ¬HavingPred.holdsOnSeq L g ψ
• HavingPred.holdsOnSeq L g (ψ₁.and ψ₂) = (HavingPred.holdsOnSeq L g ψ₁ ∧ HavingPred.holdsOnSeq L g ψ₂)
• HavingPred.holdsOnSeq L g (ψ₁.or ψ₂) = (HavingPred.holdsOnSeq L g ψ₁ ∨ HavingPred.holdsOnSeq L g ψ₂)

@[instance_reducible]

instance HavingPred.decidableHoldsOnSeq {T : Type} [ValueType T] {m n₁ : ℕ} (L : List (Tuple T m)) (g : Tuple T n₁) (ψ : HavingPred T m n₁) : Decidable (holdsOnSeq L g ψ)

Equations

• HavingPred.decidableHoldsOnSeq L g (HavingPred.cmp t f op s) = HavingPred.decidableHoldsOnSeq._aux_1 L g t f op s
• HavingPred.decidableHoldsOnSeq L g ψ.not = HavingPred.decidableHoldsOnSeq._aux_3 L g ψ (HavingPred.decidableHoldsOnSeq L g ψ)
• HavingPred.decidableHoldsOnSeq L g (ψ₁.and ψ₂) = HavingPred.decidableHoldsOnSeq._aux_5 L g ψ₁ ψ₂ (HavingPred.decidableHoldsOnSeq L g ψ₁) (HavingPred.decidableHoldsOnSeq L g ψ₂)
• HavingPred.decidableHoldsOnSeq L g (ψ₁.or ψ₂) = HavingPred.decidableHoldsOnSeq._aux_7 L g ψ₁ ψ₂ (HavingPred.decidableHoldsOnSeq L g ψ₁) (HavingPred.decidableHoldsOnSeq L g ψ₂)

def HavingPred.modelsBoolean {T : Type} [ValueType T] {m n₁ : ℕ} (d : Database T) (q : Query T m) (is : Tuple (Fin m) n₁) (ψ : HavingPred T m n₁) : Prop

Plain possible-world satisfaction of a Boolean HAVING query: the query grouping the output of q by the columns is and keeping the groups satisfying ψ holds on the database d iff some realized group key satisfies ψ – equivalently, iff its output is non-empty.

Equations

• HavingPred.modelsBoolean d q is ψ = ∃ g ∈ Multiset.map (fun (u : Tuple T m) (k : Fin n₁) => u (is k)) (q.evaluate d), HavingPred.holdsOnSeq (Relation.groupSeq is (q.evaluate d) g) g ψ

@[instance_reducible]

instance HavingPred.decidableModelsBoolean {T : Type} [ValueType T] {m n₁ : ℕ} (d : Database T) (q : Query T m) (is : Tuple (Fin m) n₁) (ψ : HavingPred T m n₁) : Decidable (modelsBoolean d q is ψ)

Equations

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

def HavingPred.booleanProv {T : Type} [ValueType T] {K : Type} [CommSemiringWithMonus K] [DecidableEq K] {m n₁ : ℕ} [HasAltLinearOrder K] (q : Query T m) (hq : q.source) (d : AnnotatedDatabase T K) (is : Tuple (Fin m) n₁) (ψ : HavingPred T m n₁) : K

Boolean provenance of a Boolean HAVING query – the ⊕-sum of the annotations of the output rows of σ_ψ(γ^≼(q)): one summand per distinct group key of the inner query, carrying the predicate provenance of its group.

Equations

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

Home · Documentation · Publications · Contributors · Source · Cite