Scan-computable HAVING provenance for MIN, MAX and PICKFIRST

For a HAVING predicate comparing an aggregate to a constant, the possible-world semantics sums the world annotations T_U(W) over the non-empty valid worlds W ⊆ U of a group, of which there are in general exponentially many. This file shows that for the aggregates MIN, MAX and PICKFIRST – those whose validity is decided occurrence by occurrence – that sum collapses, in an absorptive commutative m-semiring, to a closed form using O(|U|) semiring operations: the provenance is obtained by a single scan over the occurrences of the group, hence in polynomial time in data complexity.

The collapse

Everything rests on one identity, meet_family_eq: for H ⊆ G ⊆ U,

⊕_{W ⊆ G, W ∩ H ≠ ∅} T_U(W) = (𝟙 ⊖ ⊕_{x ∈ U \ G} α x) ⊗ (⊕_{i ∈ H} α i),

i.e., the provenance of “the world stays inside G and meets H” is the product of two running sums. Both hypotheses of the absorptive setting are used: ≤ follows from A_W ≤ α i ≤ ⊕_H α (absorptivity makes A decreasing under inclusion), and ≥ from upward_expansion in the universe G, transported to U by T_eq_T_of_subset and sum_monus.

Where the hypotheses are used

Absorptivity makes A decreasing under inclusion (A_le_of_subset_absorptive) and is used in both halves. mul_sub_left_distributive is used exactly twice: in the ≤ half, to pass from T_U(W) – defined in Provenance.Having as A_W ⊖ ⊕_x A_{W ∪ {x}} – to the factored form A_W ⊗ (𝟙 ⊖ ⊕_{U∖W} α) in which the possible-world semantics is stated; and in the ≥ half, to rewrite the right-hand side as ⊕_H α ⊖ (⊕_H α ⊗ ⊕_{U∖G} α), the shape sum_monus needs. The first use is not a proof convenience: in MaxMin TVL (absorptive but not mul_sub_left_distributive) the identity is false for T as defined here – U = {1,2}, G = H = {1} and α₁ = α₂ = unknown give 𝟘 on the left and unknown on the right – because that is precisely where the two forms of the world annotation part company.

The six comparison operators then instantiate this with the right pair (G, H); e.g., MIN(t) ≥ c keeps the worlds inside G = {i | t i ≥ c}, while MIN(t) ≤ c keeps the worlds meeting H = {i | t i ≤ c}, and MIN(t) = c uses both. PICKFIRST splits the worlds according to their first occurrence and applies the identity to each fiber.

Main results

• meet_family_eq – the collapse identity;
• prov_eq_of_pointwise – its reading as a selection predicate decided occurrence by occurrence;
• minScan / minScan_correct, maxScan / maxScan_correct, firstScan / firstScan_correct – the three scans and their correctness, for all six comparison operators.

Unlike the COUNT/SUM cases, no world enumeration is involved: the scans are closed forms, and the absorptivity hypothesis is what makes them exist (in ℕ[X], for instance, the same provenance is a product rather than a sum of annotations).

@[simp]

theorem CompOp.eval_coe_withTop {V : Type} [LinearOrder V] (op : CompOp) (a b : V) : op.eval ↑a ↑b ↔ op.eval a b

Comparisons are unchanged by the embedding of the value domain into WithTop (used to give the empty world an aggregate value).

@[simp]

theorem CompOp.eval_coe_withBot {V : Type} [LinearOrder V] (op : CompOp) (a b : V) : op.eval ↑a ↑b ↔ op.eval a b

Comparisons are unchanged by the embedding of the value domain into WithBot.

theorem Having.monus_mono_left {K : Type} [CommSemiringWithMonus K] {a a' c : K} (h : a ≤ a') : a - c ≤ a' - c

Monus is monotone in its first argument.

theorem Having.A_le_sum_of_meet {ι : Type} [DecidableEq ι] {K : Type} [CommSemiringWithMonus K] (h_abs : absorptive K) (α : ι → K) {W H : Finset ι} {i : ι} (hiW : i ∈ W) (hiH : i ∈ H) : A α W ≤ ∑ j ∈ H, α j

The annotation of a world meeting H is bounded by ⊕_{i ∈ H} α i.

theorem Having.meet_family_le {ι : Type} [DecidableEq ι] {K : Type} [CommSemiringWithMonus K] (h_abs : absorptive K) (h_distrib : mul_sub_left_distributive K) (α : ι → K) {U G H : Finset ι} : ∑ W ∈ G.powerset with (W ∩ H).Nonempty, T α U W ≤ (1 - ∑ x ∈ U \ G, α x) * ∑ i ∈ H, α i

Upper bound half of meet_family_eq.

theorem Having.meet_family_self_ge {ι : Type} [DecidableEq ι] {K : Type} [CommSemiringWithMonus K] (h_abs : absorptive K) (α : ι → K) {G H : Finset ι} (hHG : H ⊆ G) : ∑ i ∈ H, α i ≤ ∑ W ∈ G.powerset with (W ∩ H).Nonempty, T α G W

Lower bound half in the special case G = U: every α i, i ∈ H, is already reached by the worlds containing i.

theorem Having.T_eq_T_of_subset {ι : Type} [DecidableEq ι] {K : Type} [CommSemiringWithMonus K] (α : ι → K) {U G W : Finset ι} (hGU : G ⊆ U) (hWG : W ⊆ G) : T α U W = T α G W - A α W * ∑ x ∈ U \ G, α x

For a world W ⊆ G ⊆ U, passing from the universe G to the larger universe U subtracts the annotations of the occurrences of U \ G. Only monus_add and ordinary distributivity are used, not mul_sub_left_distributive.

theorem Having.meet_family_eq {ι : Type} [DecidableEq ι] {K : Type} [CommSemiringWithMonus K] (h_abs : absorptive K) (h_distrib : mul_sub_left_distributive K) (α : ι → K) {U G H : Finset ι} (hGU : G ⊆ U) (hHG : H ⊆ G) : ∑ W ∈ G.powerset with (W ∩ H).Nonempty, T α U W = (1 - ∑ x ∈ U \ G, α x) * ∑ i ∈ H, α i

Core collapse. In an absorptive m-semiring, the possible-world provenance of the family of worlds that stay inside G and meet H is (𝟙 ⊖ ⊕_{x ∈ U \ G} α x) ⊗ (⊕_{i ∈ H} α i): two running sums, hence a single scan over the occurrences of the group.

Possible-world provenance of a selection predicate

def Having.prov {ι : Type} [DecidableEq ι] {K : Type} [CommSemiringWithMonus K] (α : ι → K) (U : Finset ι) (P : Finset ι → Prop) [DecidablePred P] : K

The possible-world provenance, at one group, of a selection predicate P on worlds: the ⊕-sum of the world annotations T_U(W) over the non-empty worlds satisfying P, in the possible-world semantics of HAVING predicates.

Equations

• Having.prov α U P = ∑ W ∈ U.powerset with W.Nonempty ∧ P W, Having.T α U W

theorem Having.prov_congr {ι : Type} [DecidableEq ι] {K : Type} [CommSemiringWithMonus K] (α : ι → K) (U : Finset ι) {P Q : Finset ι → Prop} [DecidablePred P] [DecidablePred Q] (h : ∀ W ⊆ U, P W ↔ Q W) : prov α U P = prov α U Q

Two predicates that agree on the worlds of U have the same provenance.

theorem Having.prov_or {ι : Type} [DecidableEq ι] {K : Type} [CommSemiringWithMonus K] (α : ι → K) (U : Finset ι) {P Q : Finset ι → Prop} [DecidablePred P] [DecidablePred Q] (hdisj : ∀ (W : Finset ι), P W → Q W → False) : (prov α U fun (W : Finset ι) => P W ∨ Q W) = prov α U P + prov α U Q

The provenance of a disjunction of two mutually exclusive predicates is the ⊕-sum of the two provenances.

theorem Having.prov_fiber {ι : Type} [DecidableEq ι] {K : Type} [CommSemiringWithMonus K] (α : ι → K) (U P : Finset ι) (Q : ι → Finset ι → Prop) [(i : ι) → DecidablePred (Q i)] {R : Finset ι → Prop} [DecidablePred R] (hR : ∀ W ⊆ U, W.Nonempty ∧ R W ↔ ∃ i ∈ P, W.Nonempty ∧ Q i W) (hdisj : ∀ (W : Finset ι), ∀ i ∈ P, ∀ j ∈ P, Q i W → Q j W → i = j) : prov α U R = ∑ i ∈ P, prov α U (Q i)

Provenance of a predicate that splits into fibers indexed by a finite set: if every non-empty world satisfying R satisfies Q i for exactly one i ∈ P, the provenance of R is the ⊕-sum of the provenances of the Q i.

theorem Having.prov_of_forall_not {ι : Type} [DecidableEq ι] {K : Type} [CommSemiringWithMonus K] (α : ι → K) (U : Finset ι) {P : Finset ι → Prop} [DecidablePred P] (hP : ∀ W ⊆ U, W.Nonempty → ¬P W) : prov α U P = 0

Unsatisfiable predicates have provenance 𝟘. This is the algebraic content of the range-check short-circuit of the enumeration algorithms: when no world can satisfy the predicate, the possible-world ⊕-sum is empty. No hypothesis on the m-semiring is needed.

theorem Having.prov_of_forall {ι : Type} [DecidableEq ι] {K : Type} [CommSemiringWithMonus K] (h_abs : absorptive K) (α : ι → K) (U : Finset ι) {P : Finset ι → Prop} [DecidablePred P] (hP : ∀ W ⊆ U, W.Nonempty → P W) : prov α U P = ∑ i ∈ U, α i

Necessarily-true predicates have provenance ⊕_{i ∈ U} α i. This is the algebraic content of the complementary range-check short-circuit: when every non-empty world satisfies the predicate, the possible-world provenance is F_1(U), which in an absorptive m-semiring collapses (by F_eq_S at C = 1) to the ⊕-sum of the annotations of the group.

theorem Having.prov_eq_of_pointwise {ι : Type} [DecidableEq ι] {K : Type} [CommSemiringWithMonus K] (h_abs : absorptive K) (h_distrib : mul_sub_left_distributive K) (α : ι → K) (U : Finset ι) (p q r : ι → Prop) [DecidablePred p] [DecidablePred q] [DecidablePred r] (hqp : ∀ i ∈ U, q i → p i) (hr : ∀ i ∈ U, r i ↔ ¬p i) {P : Finset ι → Prop} [DecidablePred P] (hP : ∀ W ⊆ U, W.Nonempty ∧ P W ↔ (∀ i ∈ W, p i) ∧ ∃ i ∈ W, q i) : prov α U P = (1 - ∑ x ∈ U with r x, α x) * ∑ i ∈ U with q i, α i

Occurrence-wise selection predicates are scan-computable. If a non-empty world satisfies P exactly when all its occurrences satisfy p and at least one of them satisfies q, then the provenance of P is (𝟙 ⊖ ⊕_{¬p} α) ⊗ (⊕_{q} α).

This is the algebraic content of the tractability of the MIN, MAX and PICKFIRST comparisons: all of them have this shape, so their provenance is obtained from two running sums over the occurrences of the group.

theorem Having.prov_eq_of_exists {ι : Type} [DecidableEq ι] {K : Type} [CommSemiringWithMonus K] (h_abs : absorptive K) (h_distrib : mul_sub_left_distributive K) (α : ι → K) (U : Finset ι) (q : ι → Prop) [DecidablePred q] {P : Finset ι → Prop} [DecidablePred P] (hP : ∀ W ⊆ U, W.Nonempty ∧ P W ↔ ∃ i ∈ W, q i) : prov α U P = ∑ i ∈ U with q i, α i

Special case of prov_eq_of_pointwise with no constraint on the excluded occurrences: the provenance of “some occurrence of the world satisfies q” is ⊕_{q} α.

The MIN and MAX aggregates

def Having.minAgg {ι V : Type} [LinearOrder V] (t : ι → V) (W : Finset ι) : WithTop V

MIN(t) over a world, as an element of WithTop V: the empty world has aggregate value ⊤ (it is excluded from the possible-world sum anyway).

Equations

• Having.minAgg t W = W.inf fun (i : ι) => ↑(t i)

def Having.maxAgg {ι V : Type} [LinearOrder V] (t : ι → V) (W : Finset ι) : WithBot V

MAX(t) over a world, as an element of WithBot V.

Equations

• Having.maxAgg t W = W.sup fun (i : ι) => ↑(t i)

def Having.minScan {ι K : Type} [CommSemiringWithMonus K] {V : Type} [LinearOrder V] (α : ι → K) (U : Finset ι) (t : ι → V) (op : CompOp) (c : V) : K

The MIN scan. Closed form for the provenance of MIN(t) op c: for each operator, at most two running ⊕-sums over the occurrences of the group, combined by one ⊖ and one ⊗. Computing it takes O(|U|) semiring operations, hence polynomial time in data complexity; minScan_correct proves it correct.

Equations

• Having.minScan α U t CompOp.lt c = ∑ i ∈ U with t i < c, α i
• Having.minScan α U t CompOp.le c = ∑ i ∈ U with t i ≤ c, α i
• Having.minScan α U t CompOp.ge c = (1 - ∑ x ∈ U with t x < c, α x) * ∑ i ∈ U with c ≤ t i, α i
• Having.minScan α U t CompOp.gt c = (1 - ∑ x ∈ U with t x ≤ c, α x) * ∑ i ∈ U with c < t i, α i
• Having.minScan α U t CompOp.eq c = (1 - ∑ x ∈ U with t x < c, α x) * ∑ i ∈ U with t i = c, α i
• Having.minScan α U t CompOp.ne c = ∑ i ∈ U with t i < c, α i + (1 - ∑ x ∈ U with t x ≤ c, α x) * ∑ i ∈ U with c < t i, α i

def Having.maxScan {ι K : Type} [CommSemiringWithMonus K] {V : Type} [LinearOrder V] (α : ι → K) (U : Finset ι) (t : ι → V) (op : CompOp) (c : V) : K

The MAX scan, the mirror image of minScan; see maxScan_correct.

Equations

• Having.maxScan α U t CompOp.gt c = ∑ i ∈ U with c < t i, α i
• Having.maxScan α U t CompOp.ge c = ∑ i ∈ U with c ≤ t i, α i
• Having.maxScan α U t CompOp.le c = (1 - ∑ x ∈ U with c < t x, α x) * ∑ i ∈ U with t i ≤ c, α i
• Having.maxScan α U t CompOp.lt c = (1 - ∑ x ∈ U with c ≤ t x, α x) * ∑ i ∈ U with t i < c, α i
• Having.maxScan α U t CompOp.eq c = (1 - ∑ x ∈ U with c < t x, α x) * ∑ i ∈ U with t i = c, α i
• Having.maxScan α U t CompOp.ne c = ∑ i ∈ U with c < t i, α i + (1 - ∑ x ∈ U with c ≤ t x, α x) * ∑ i ∈ U with t i < c, α i

@[simp]

theorem Having.le_minAgg_iff {ι : Type} [DecidableEq ι] {V : Type} [LinearOrder V] (t : ι → V) (W : Finset ι) (c : V) : ↑c ≤ minAgg t W ↔ ∀ i ∈ W, c ≤ t i

@[simp]

theorem Having.lt_minAgg_iff {ι : Type} [DecidableEq ι] {V : Type} [LinearOrder V] (t : ι → V) (W : Finset ι) (c : V) : ↑c < minAgg t W ↔ ∀ i ∈ W, c < t i

@[simp]

theorem Having.minAgg_lt_iff {ι : Type} [DecidableEq ι] {V : Type} [LinearOrder V] (t : ι → V) (W : Finset ι) (c : V) : minAgg t W < ↑c ↔ ∃ i ∈ W, t i < c

@[simp]

theorem Having.minAgg_le_iff {ι : Type} [DecidableEq ι] {V : Type} [LinearOrder V] (t : ι → V) (W : Finset ι) (c : V) : minAgg t W ≤ ↑c ↔ ∃ i ∈ W, t i ≤ c

theorem Having.minAgg_eq_iff {ι : Type} [DecidableEq ι] {V : Type} [LinearOrder V] (t : ι → V) (W : Finset ι) (c : V) : minAgg t W = ↑c ↔ (∀ i ∈ W, c ≤ t i) ∧ ∃ i ∈ W, t i = c

@[simp]

theorem Having.maxAgg_le_iff {ι : Type} [DecidableEq ι] {V : Type} [LinearOrder V] (t : ι → V) (W : Finset ι) (c : V) : maxAgg t W ≤ ↑c ↔ ∀ i ∈ W, t i ≤ c

@[simp]

theorem Having.maxAgg_lt_iff {ι : Type} [DecidableEq ι] {V : Type} [LinearOrder V] (t : ι → V) (W : Finset ι) (c : V) : maxAgg t W < ↑c ↔ ∀ i ∈ W, t i < c

@[simp]

theorem Having.lt_maxAgg_iff {ι : Type} [DecidableEq ι] {V : Type} [LinearOrder V] (t : ι → V) (W : Finset ι) (c : V) : ↑c < maxAgg t W ↔ ∃ i ∈ W, c < t i

@[simp]

theorem Having.le_maxAgg_iff {ι : Type} [DecidableEq ι] {V : Type} [LinearOrder V] (t : ι → V) (W : Finset ι) (c : V) : ↑c ≤ maxAgg t W ↔ ∃ i ∈ W, c ≤ t i

theorem Having.maxAgg_eq_iff {ι : Type} [DecidableEq ι] {V : Type} [LinearOrder V] (t : ι → V) (W : Finset ι) (c : V) : maxAgg t W = ↑c ↔ (∀ i ∈ W, t i ≤ c) ∧ ∃ i ∈ W, t i = c

Provenance of the six MIN(t) op c predicates

theorem Having.prov_min_lt {ι : Type} [DecidableEq ι] {K : Type} [CommSemiringWithMonus K] {V : Type} [LinearOrder V] (h_abs : absorptive K) (h_distrib : mul_sub_left_distributive K) (α : ι → K) (U : Finset ι) (t : ι → V) (c : V) : (prov α U fun (W : Finset ι) => minAgg t W < ↑c) = ∑ i ∈ U with t i < c, α i

MIN(t) < c: some occurrence of the world has value < c.

theorem Having.prov_min_le {ι : Type} [DecidableEq ι] {K : Type} [CommSemiringWithMonus K] {V : Type} [LinearOrder V] (h_abs : absorptive K) (h_distrib : mul_sub_left_distributive K) (α : ι → K) (U : Finset ι) (t : ι → V) (c : V) : (prov α U fun (W : Finset ι) => minAgg t W ≤ ↑c) = ∑ i ∈ U with t i ≤ c, α i

MIN(t) ≤ c: some occurrence of the world has value ≤ c.

theorem Having.prov_min_ge {ι : Type} [DecidableEq ι] {K : Type} [CommSemiringWithMonus K] {V : Type} [LinearOrder V] (h_abs : absorptive K) (h_distrib : mul_sub_left_distributive K) (α : ι → K) (U : Finset ι) (t : ι → V) (c : V) : (prov α U fun (W : Finset ι) => ↑c ≤ minAgg t W) = (1 - ∑ x ∈ U with t x < c, α x) * ∑ i ∈ U with c ≤ t i, α i

MIN(t) ≥ c: the world avoids every occurrence of value < c and is non-empty.

theorem Having.prov_min_gt {ι : Type} [DecidableEq ι] {K : Type} [CommSemiringWithMonus K] {V : Type} [LinearOrder V] (h_abs : absorptive K) (h_distrib : mul_sub_left_distributive K) (α : ι → K) (U : Finset ι) (t : ι → V) (c : V) : (prov α U fun (W : Finset ι) => ↑c < minAgg t W) = (1 - ∑ x ∈ U with t x ≤ c, α x) * ∑ i ∈ U with c < t i, α i

MIN(t) > c: the world avoids every occurrence of value ≤ c and is non-empty.

theorem Having.prov_min_eq {ι : Type} [DecidableEq ι] {K : Type} [CommSemiringWithMonus K] {V : Type} [LinearOrder V] (h_abs : absorptive K) (h_distrib : mul_sub_left_distributive K) (α : ι → K) (U : Finset ι) (t : ι → V) (c : V) : (prov α U fun (W : Finset ι) => minAgg t W = ↑c) = (1 - ∑ x ∈ U with t x < c, α x) * ∑ i ∈ U with t i = c, α i

MIN(t) = c: the world avoids every occurrence of value < c and contains one of value c.

theorem Having.prov_min_ne {ι : Type} [DecidableEq ι] {K : Type} [CommSemiringWithMonus K] {V : Type} [LinearOrder V] (h_abs : absorptive K) (h_distrib : mul_sub_left_distributive K) (α : ι → K) (U : Finset ι) (t : ι → V) (c : V) : (prov α U fun (W : Finset ι) => minAgg t W ≠ ↑c) = ∑ i ∈ U with t i < c, α i + (1 - ∑ x ∈ U with t x ≤ c, α x) * ∑ i ∈ U with c < t i, α i

MIN(t) ≠ c: the two disjoint cases MIN(t) < c and MIN(t) > c.

Provenance of the six MAX(t) op c predicates

theorem Having.prov_max_gt {ι : Type} [DecidableEq ι] {K : Type} [CommSemiringWithMonus K] {V : Type} [LinearOrder V] (h_abs : absorptive K) (h_distrib : mul_sub_left_distributive K) (α : ι → K) (U : Finset ι) (t : ι → V) (c : V) : (prov α U fun (W : Finset ι) => ↑c < maxAgg t W) = ∑ i ∈ U with c < t i, α i

MAX(t) > c: some occurrence of the world has value > c.

theorem Having.prov_max_ge {ι : Type} [DecidableEq ι] {K : Type} [CommSemiringWithMonus K] {V : Type} [LinearOrder V] (h_abs : absorptive K) (h_distrib : mul_sub_left_distributive K) (α : ι → K) (U : Finset ι) (t : ι → V) (c : V) : (prov α U fun (W : Finset ι) => ↑c ≤ maxAgg t W) = ∑ i ∈ U with c ≤ t i, α i

MAX(t) ≥ c: some occurrence of the world has value ≥ c.

theorem Having.prov_max_le {ι : Type} [DecidableEq ι] {K : Type} [CommSemiringWithMonus K] {V : Type} [LinearOrder V] (h_abs : absorptive K) (h_distrib : mul_sub_left_distributive K) (α : ι → K) (U : Finset ι) (t : ι → V) (c : V) : (prov α U fun (W : Finset ι) => maxAgg t W ≤ ↑c) = (1 - ∑ x ∈ U with c < t x, α x) * ∑ i ∈ U with t i ≤ c, α i

MAX(t) ≤ c: the world avoids every occurrence of value > c and is non-empty.

theorem Having.prov_max_lt {ι : Type} [DecidableEq ι] {K : Type} [CommSemiringWithMonus K] {V : Type} [LinearOrder V] (h_abs : absorptive K) (h_distrib : mul_sub_left_distributive K) (α : ι → K) (U : Finset ι) (t : ι → V) (c : V) : (prov α U fun (W : Finset ι) => maxAgg t W < ↑c) = (1 - ∑ x ∈ U with c ≤ t x, α x) * ∑ i ∈ U with t i < c, α i

MAX(t) < c: the world avoids every occurrence of value ≥ c and is non-empty.

theorem Having.prov_max_eq {ι : Type} [DecidableEq ι] {K : Type} [CommSemiringWithMonus K] {V : Type} [LinearOrder V] (h_abs : absorptive K) (h_distrib : mul_sub_left_distributive K) (α : ι → K) (U : Finset ι) (t : ι → V) (c : V) : (prov α U fun (W : Finset ι) => maxAgg t W = ↑c) = (1 - ∑ x ∈ U with c < t x, α x) * ∑ i ∈ U with t i = c, α i

MAX(t) = c: the world avoids every occurrence of value > c and contains one of value c.

theorem Having.prov_max_ne {ι : Type} [DecidableEq ι] {K : Type} [CommSemiringWithMonus K] {V : Type} [LinearOrder V] (h_abs : absorptive K) (h_distrib : mul_sub_left_distributive K) (α : ι → K) (U : Finset ι) (t : ι → V) (c : V) : (prov α U fun (W : Finset ι) => maxAgg t W ≠ ↑c) = ∑ i ∈ U with c < t i, α i + (1 - ∑ x ∈ U with c ≤ t x, α x) * ∑ i ∈ U with t i < c, α i

MAX(t) ≠ c: the two disjoint cases MAX(t) > c and MAX(t) < c.

The two scans are correct

theorem Having.minScan_correct {ι : Type} [DecidableEq ι] {K : Type} [CommSemiringWithMonus K] {V : Type} [LinearOrder V] (h_abs : absorptive K) (h_distrib : mul_sub_left_distributive K) (α : ι → K) (U : Finset ι) (t : ι → V) (c : V) (op : CompOp) : (prov α U fun (W : Finset ι) => op.eval (minAgg t W) ↑c) = minScan α U t op c

Correctness of the MIN scan. For every comparison operator, the possible-world provenance of the HAVING MIN(t) op c predicate is computed by the scan minScan.

theorem Having.maxScan_correct {ι : Type} [DecidableEq ι] {K : Type} [CommSemiringWithMonus K] {V : Type} [LinearOrder V] (h_abs : absorptive K) (h_distrib : mul_sub_left_distributive K) (α : ι → K) (U : Finset ι) (t : ι → V) (c : V) (op : CompOp) : (prov α U fun (W : Finset ι) => op.eval (maxAgg t W) ↑c) = maxScan α U t op c

Correctness of the MAX scan.

The PICKFIRST aggregate

PICKFIRST is the non-commutative aggregate returning the value of the first occurrence of its input sequence. Here the occurrences are ordered by a linear order ≼ on ι (the order along which the group is enumerated), so the first occurrence of a world is its ≼-minimum.

def Having.firstAgg {ι V : Type} [LinearOrder ι] (t : ι → V) (W : Finset ι) : WithTop V

PICKFIRST(t) over a world: the value of its ≼-first occurrence, with ⊤ for the empty world.

Equations

• Having.firstAgg t W = WithTop.map t W.min

theorem Having.firstAgg_eq {ι : Type} [DecidableEq ι] {V : Type} [LinearOrder V] [LinearOrder ι] (t : ι → V) {W : Finset ι} {i : ι} (hiW : i ∈ W) (hmin : ∀ j ∈ W, i ≤ j) : firstAgg t W = ↑(t i)

The value of PICKFIRST on a world whose ≼-minimum is i.

def Having.firstScan {ι K : Type} [CommSemiringWithMonus K] {V : Type} [LinearOrder V] [LinearOrder ι] (α : ι → K) (U : Finset ι) (t : ι → V) (op : CompOp) (c : V) : K

The PICKFIRST scan. Closed form for the provenance of PICKFIRST(t) op c: one term per satisfying occurrence, each combining the annotation of that occurrence with the running sum of the annotations of the occurrences that precede it.

Equations

• Having.firstScan α U t op c = ∑ i ∈ U with op.eval (t i) c, (1 - ∑ x ∈ U with x < i, α x) * α i

theorem Having.prov_first_fiber {ι : Type} [DecidableEq ι] {K : Type} [CommSemiringWithMonus K] [LinearOrder ι] (h_abs : absorptive K) (h_distrib : mul_sub_left_distributive K) (α : ι → K) (U : Finset ι) {i : ι} (hiU : i ∈ U) : (prov α U fun (W : Finset ι) => i ∈ W ∧ ∀ j ∈ W, i ≤ j) = (1 - ∑ x ∈ U with x < i, α x) * α i

Provenance of the worlds whose ≼-first occurrence is a given i: the world contains i and none of the occurrences preceding i.

theorem Having.firstScan_correct {ι : Type} [DecidableEq ι] {K : Type} [CommSemiringWithMonus K] {V : Type} [LinearOrder V] [LinearOrder ι] (h_abs : absorptive K) (h_distrib : mul_sub_left_distributive K) (α : ι → K) (U : Finset ι) (t : ι → V) (c : V) (op : CompOp) : (prov α U fun (W : Finset ι) => op.eval (firstAgg t W) ↑c) = firstScan α U t op c

Correctness of the PICKFIRST scan. The possible-world provenance of the HAVING PICKFIRST(t) op c predicate is computed by the scan firstScan: the worlds are partitioned according to their first occurrence.

Home · Documentation · Publications · Contributors · Source · Cite