PaperlayerView exact revision on arXiv

Source-linked AI summary

Provenance of HAVING Queries in Semirings with Monus

Aryak Sen, Pratik Karmakar, Silviu Maniu, Angelo Saadeh, Pierre Senellart

arXiv:2609.31246v1cs.DB

TL;DR

HAVING comparisons over aggregate values have lacked an implementable provenance semantics across probabilistic-query semirings and aggregate functions. This paper defines one for commutative m-semirings and derives algorithms for it. For COUNT(*) comparisons, it agrees with the aggregation-free self-join rewriting under stated semiring conditions, and its ProvSQL implementation is viable on a real-world dataset.

  • Problem

    Prior formal comparison expressions may remain unresolved in semirings needed for probabilistic query evaluation, and the approach is restricted to commutative monoid aggregates.

    Source: §1 · p. 2

  • Method

    The paper defines HAVING provenance through possible-world semantics in arbitrary commutative m-semirings, without requiring a semimodule structure or restricting aggregate functions to commutative monoid operations.

    Source: §1 · p. 2

  • Results

    For COUNT(*) comparisons, the semantics agrees with aggregation-free self-join rewriting in absorptive m-semirings where ⊗ distributes over ⊖.

    Source: §1 · p. 2

  • Takeaways & Limitations

    Algorithms implemented in ProvSQL show the approach is viable on a real-world database, including for probabilistic query evaluation.

    Source: §1 · p. 3

    Grouping or ordering over aggregate values is rejected, and scalar aggregation is outside the formal treatment despite being implemented.

    Source: §3 · p. 9

Abstract

from arXiv · show

The semiring framework and its extensions form the basis of a rich collection of theoretical results and implementations for provenance tracking of database queries. Many real-world queries use aggregation and conditions on the aggregate values. Support for such queries has been proposed by introducing semimodule elements as aggregate values and formal comparisons between aggregate values as tuple annotations, which takes the approach outside the standard semiring framework. In this work, we show how to introduce a semantics for the provenance of such queries in arbitrary commutative semirings with monus (or m-semirings), without the need for additional operators. This semantics is shown to agree with the standard provenance of the aggregation-free self-join rewriting of HAVING COUNT(*) queries in semirings that are absorptive and where times distributes over monus. We derive algorithms for this semantics and implement them within the ProvSQL system, with viable performance on a real-world dataset for probabilistic query evaluation.

1 Introduction

HAVING queries need a provenance semantics for comparisons over aggregate values, which prior approaches could leave as abstract expressions or restrict to particular aggregates. This paper defines such semantics in commutative m-semirings and provides algorithms and a ProvSQL implementation.

1 Introduction

  • The prior comparison-expression approach can remain unresolved for probabilistic-query semirings and is restricted to commutative monoid aggregates.Existing provenance systems either offered partial aggregation support or stopped at abstract comparison formulas without concrete semiring elements.Source: §1 · p. 2
  • The paper gives an implementable semantics for HAVING comparisons in arbitrary commutative m-semirings and for any aggregate function.The aggregate function need not be commutative or monoid-based.Source: §1 · p. 2
  • The paper systematically accounts for commutative m-semirings and supplies machine-checked Lean proofs of their definitions and properties.The formalized account corrects erroneous claims in prior work [17, 5].Source: §1 · p. 2
  • For COUNT(*) comparisons, the semantics agrees with the aggregation-free self-join rewriting when the m-semiring is absorptive and ⊗ distributes over ⊖.The stated result applies in particular to the Boolean-function semiring used for probability evaluation.Source: §1 · p. 2
  • The paper gives possible-world enumeration generally and polynomial-time algorithms for COUNT, SUM, MIN, and MAX in identified cases, especially absorptive m-semirings.The algorithms are implemented in ProvSQL and shown viable on a real-world database, including for probabilistic query evaluation.Source: §1 · pp. 2–3

2 Preliminaries

The preliminaries establish the commutative m-semiring setting, annotated multiset relations, and the representation of aggregate values used to define query semantics. They distinguish ordinary selection from HAVING comparisons over aggregates.

2 Preliminaries

  • An m-semiring is a naturally ordered semiring equipped with monus satisfying the residuation law.The paper focuses on commutative semirings and catalogs properties including absorptivity and distribution of ⊗ over ⊖.Source: §2 · pp. 3–4
  • Table 1 summarizes common m-semirings' idempotence, absorptivity, ⊗-over-⊖ distributivity, and characteristic 0.The paper reports that its table and Lean proofs correct errors in prior claims about tropical monus and distributivity in N[X] and Why[X] [17, Example 4] [5].Source: §2 · p. 4, Table 1 · p. 4
  • Annotated relations use multiset semantics, allowing repeated tuple occurrences with distinct annotations so aggregation can preserve multiplicity.Merging such occurrences can change COUNT(*) under SQL bag semantics.Source: §2 · p. 5
  • Grouping records aggregate values as formal objects derived from the ordered occurrences in each group, while the group key receives a δ-based existence annotation.The ordering matters for non-commutative aggregates, and is irrelevant for commutative ones.Source: §2 · p. 6
  • HAVING comparisons extend selection to predicates over aggregate values, while regular-value selections retain the earlier semantics.The paper changes only selection semantics; other algebra operators retain their prior semantics, and terminal aggregation alone excludes HAVING.Source: §2 · p. 6

3 A Possible-World Semantics for Aggregate Comparisons

The paper evaluates aggregate comparisons by splitting each group into possible worlds, testing the aggregate predicate in each world, and combining annotations for worlds that satisfy it. This gives comparisons K-valued provenance without relying on a semimodule structure.

3 A Possible-World Semantics for Aggregate Comparisons

  • Possible-world semantics supports aggregate comparisons in arbitrary commutative m-semirings and accepts any function on sequences of values.Unlike the semimodule-based approach, it includes non-associative functions such as AVG and non-commutative functions such as ARRAY_AGG.Source: §3 · p. 7
  • The provenance of an aggregate predicate is the ⊕-sum of annotations for non-empty worlds that satisfy the comparison.The world aggregate is tested as an ordinary value, and summing only non-empty satisfying worlds enforces group existence.Source: §3 · pp. 7–8
  • A world is a subsequence of a group's occurrences; its annotation records kept and discarded occurrences using ⊗ and monus.Each occurrence contributes separately, including repeated tuples.Source: §3 · p. 7
  • In absorptive B[X], COUNT(*) ≥ 2 over three annotated occurrences yields the Boolean function that at least two variables hold.Discarded-occurrence negations cancel, leaving the three minimal satisfying pairs; this simplification fails in non-absorptive semirings.Source: §3 · p. 8
  • Aggregate values may pass through projection, joins, unions, and further selections before comparison, with the originating group's worlds retained.The implementation materializes the aggregate value as a provenance-circuit gate and evaluates the comparison downstream.Source: §3 · p. 9
  • Grouping or ordering over aggregate values is rejected; scalar aggregation is implemented but left outside the paper's formal treatment.The formal definitions assume at least one grouping index, while the implementation follows SQL's single-group convention for scalar aggregation.Source: §3 · p. 9

4 Main Results

The paper defines provenance semantics for HAVING queries in commutative m-semirings and establishes when COUNT(*) provenance matches its aggregation-free self-join rewriting. It also proves compatibility with homomorphisms, gives a probabilistic interpretation, and identifies tractable and intractable cases.

4 Main Results

  • Absorptive m-semirings where ⊗ distributes over ⊖ give the same provenance for COUNT(*) comparisons and their aggregation-free self-join rewritings.The theorem treats ⩽, =, and ⩾ comparisons; the result extends to the six comparison operators.Source: §4 · pp. 9–10
  • The two hypotheses are separately necessary for the stated general equivalence: counterexamples arise without distributivity or without absorptivity.The paper also notes that outside Boolean provenance, results can depend on query writing, so it adopts its semantics as an implementable choice for other m-semirings.Source: §4 · p. 10
  • For monotone HAVING conditions rewritable as positive aggregate-free queries, absorptivity suffices without ⊗-over-⊖ distributivity.COUNT(*) ⩾ C is one such condition.Source: §4 · p. 10
  • HAVING provenance commutes with m-semiring homomorphisms, preserving the compile-once, evaluate-many specialization principle.The paper identifies tropical, Viterbi, and Łukasiewicz m-semirings as examples covered by a proper generalization beyond Boolean-function provenance.Source: §4 · pp. 10–11
  • For tuple-independent probabilistic databases, the semantics computes Boolean query probability from the Boolean-function provenance of the query.The annotations use independent variables carrying the corresponding tuple probabilities.Source: §4 · p. 11
  • For B[X] and N[X], deciding whether HAVING provenance is nonzero is NP-complete for a fixed query with distinct-variable annotations.For B[X], deciding nonzero provenance for a fixed HAVING query is in NP.Source: §4 · p. 11

5 Algorithms

The paper gives general possible-world enumeration and specialized procedures for common aggregate comparisons. It identifies conditions for polynomial-time symbolic provenance and gives polynomial-time probability evaluation when group contributors are independent.

5 Algorithms

  • ValidSum incrementally builds worlds by their sums, ValidCount enumerates subsets by size, and other aggregates or comparisons between multiple aggregates use brute-force world enumeration.The algorithms return precisely the index sets of valid worlds, whose annotations are combined by ⊕.Source: §5 · pp. 11–12
  • Polynomial-time symbolic provenance is available for several aggregate comparisons, with the required semiring assumptions depending on the aggregate and comparison.The procedures compute provenance by combining the annotations of valid non-empty worlds.Source: §5 · p. 12
  • MIN, MAX, and PICKFIRST comparisons take polynomial time in absorptive m-semirings where ⊗ distributes over ⊖, using a single scan.The scan decides world validity occurrence by occurrence.Source: §5 · p. 12
  • COUNT(*) ⩾ k or > k and SUM(a) ⩾ c or > c are tractable in absorptive m-semirings when SUM values meet the stated fixed-threshold bound.Their upward-closed valid-world families reduce to minimal worlds of bounded size, yielding O(|U|^(k+1)) candidates.Source: §5 · p. 12
  • COUNT(*) = k, ⩽ k, or < k is tractable in arbitrary m-semirings for fixed k; the corresponding SUM cases require all values to meet the threshold condition.The valid worlds have cardinality at most the fixed threshold, so only polynomially many need enumeration.Source: §5 · pp. 12–13
  • With independent group contributors, aggregate-comparison probabilities are computable in polynomial time; MIN and MAX comparisons take O(N).For SUM(t) θ C, the stated bound is O(N · min(C, S)), where S is the sum of the input weights.Source: §5 · p. 13

6 Implementation and Experiments

The section implements HAVING provenance algorithms in ProvSQL and evaluates them on a probabilistic image-retrieval database. As k grows, the self-join rewriting becomes much slower, while the proposed semantics remains comparatively stable.

6 Implementation and Experiments

  • The implementation uses closed forms for MIN, MAX, and PICKFIRST, brute-force enumeration otherwise, and justified pruning for absorptive m-semirings.For nonnegative integer sums, ValidSum uses dynamic programming bounded by the comparison constant; negative values and tables beyond 107 entries fall back to enumeration.Source: §6 · p. 13
  • The probabilistic retrieval database contains 239,377 images and 1,570,565 detected-object annotations, treated as independent probabilistic facts.The evaluation queried refrigerator objects for COUNT(*) >= k and COUNT(*) <= k, with k from 0 to 15; no image had more than 13 objects.Source: §6 · pp. 13–14
  • At k=15, self-join provenance tracking was 106x slower for COUNT(*) >= k and 108x for <= k; probability-evaluation ratios reached 83x and 115x, respectively.Figure 1 compares planning plus execution time; for provenance tracking, the rewriting was faster at smaller k before its cost grew with the number of joins.Source: Figure 1 · p. 14, §6 · p. 15
  • The probability pipeline chooses the cheapest estimated applicable exact method per provenance circuit; the experiment reports means from three runs with one-standard-deviation error bars.The genetic query optimizer was disabled because its join orders made self-joins with k >= 12 exceed a five-minute timeout; exhaustive planning kept execution around three seconds but planning grew quickly.Source: §6 · p. 14
  • For probability evaluation, our semantics took 0.2–0.5 seconds across k, and Poisson-binomial optimization brought no measurable gain on this dataset.Groups contained at most 13 objects, leaving valid-world DNFs small enough for world enumeration or inclusion–exclusion.Source: §6 · p. 15

7 Related Work

Prior work had introduced formal comparisons for aggregate provenance, but had not assigned them concrete values across commutative m-semirings. Related research also addresses negation, provenance systems, probabilistic aggregation, and compact representations.

Aggregation in the provenance semiring framework

  • The present work gives values in every commutative m-semiring to the formal aggregate-comparison expressions introduced by [6] and stored as strings by [32].The cited approaches did not consider evaluation of those expressions or probability computation.Source: §7 · p. 15

Negation in the provenance semiring framework

  • The monus extension [17] supports provenance for negation, but some m-semirings lack expected axioms such as multiplication distributing over monus [5].The framework has also supported SPARQL provenance [18], a semiring generalization of Codd’s theorem [8], and ProvSQL’s EXCEPT operator [34].Source: §7 · p. 15

Provenance systems

  • ProvSQL previously stored aggregate comparisons as unevaluated formal expressions [34], while GProM [7] treated HAVING as a plain selection without recording comparison-dependent provenance.That omission precludes probabilistic use of GProM’s HAVING handling.Source: §7 · p. 15

Aggregation in probabilistic databases

  • Prior probabilistic HAVING work was restricted in scope: [16] used Boolean provenance and commutative-monoid aggregates, while ProbLog [15, 14] supports no other m-semiring and does not scale to realistic database sizes [34].Factorized aggregation work [10] omits provenance and is deterministic.Source: §7 · p. 16

8 Conclusion

The paper gives HAVING queries a provenance semantics for any commutative m-semiring, with equivalence to self-join rewriting under stated conditions. Its algorithms and experiments support feasibility, while the conclusion identifies provenance circuits for safe plans as a next step.

8 Conclusion

  • The semantics applies to any commutative m-semiring and gives values to the formal comparison expressions of [6].For COUNT(*) comparisons it agrees with self-join rewriting when the m-semiring is absorptive and multiplication distributes over monus; elsewhere, query formulation can change provenance.Source: §8 · p. 16
  • Algorithms for specific aggregates and comparisons, together with experiments, show feasibility and yield the first end-to-end provenance-aware implementation of selection on aggregate values.The system implementation extends ProvSQL.Source: §8 · p. 16
  • A proposed next step is lifting safe plans to provenance circuits while keeping probabilistic evaluation of safe HAVING queries over joins polynomial.The conclusion notes that Proposition 19 restates the base case of those safe plans.Source: §8 · p. 16

A.1 Corrections to the Literature

This appendix corrects published claims about distributivity over monus and the existence of monus in tropical semirings. It shows counterexamples for two provenance semirings and explains that the tropical claim confused the usual order with the semiring’s natural order.

A.1 Corrections to the Literature

  • The tropical semiring over R does admit monus: its natural order reverses the usual real order, so the residuation condition holds.The same construction applies over Q, Z, and N; the mistaken contrary claim in [17] used the usual order to assess whether a least element exists.Source: §A.1 · p. 20
  • The distributivity claim for N[X] in [5] fails: coefficient-wise truncated subtraction gives different results for (a ⊗ b) ⊖ (a ⊗ c) and a ⊗ (b ⊖ c).The example uses a = x + 1, b = x, and c = 1; the results differ in the coefficient of x.Source: §A.1 · pp. 20–21
  • Why[X] also fails the claimed distributivity axiom A13 from [5], as a one-variable example with set difference monus demonstrates.In the example, b ⊖ c is nonempty, but multiplying a by b and c gives the same result.Source: §A.1 · p. 21

A.2 Proofs of the Useful Results on M-Semirings

The appendix establishes useful algebraic properties of m-semirings and recalls the semantics of relational algebra with aggregation. It characterizes when addition is a join and when monus distributes over addition, and specifies the operators and annotation structures used for aggregate queries.

A.2 Proofs of the Useful Results on M-Semirings

  • In an m-semiring, idempotence is equivalent to right-distributivity of monus over addition; when idempotent, addition is the join under the natural order.The proof establishes that a ⊕ b is the least upper bound of a and b.Source: §A.2 · p. 21
  • The proof derives idempotent addition from a ⊖ a = 0 using residuation and antisymmetry of the natural order.It concludes that a ⊕ a = a for every a.Source: §A.2 · p. 21
  • Monus is bounded by its minuend, and increasing the subtrahend can only decrease the result in the natural order.These properties follow from the residuation law.Source: §A.2 · p. 22

A.3 Relational Algebra with Aggregation and its Semantics

  • The relational-algebra multiset difference models SQL NOT IN rather than EXCEPT ALL; the usual truncated-count difference makes provenance computation intractable.Under set semantics, ε(q1 − q2) matches EXCEPT.Source: §A.3 · p. 22
  • Annotated query semantics require a semiring, an m-semiring for multiset difference, and a δ-semiring for aggregation.The appendix also recalls the corresponding ordinary-relation operators and their aggregation semantics.Source: §A.3 · p. 23

B Material for Section 3 (A Possible-World Semantics for Aggregate Comparisons)

The appendix formalizes aggregate comparisons using possible worlds and extends the earlier semantics beyond comparisons applied directly to groupings. It also gives a gate-based rewriting for ProvSQL and establishes its correctness relative to the comparison and indicator gates.

B Material for Section 3 (A Possible-World Semantics for Aggregate Comparisons)

  • The general semantics tracks regular, aggregate-token, and provenance columns, with query-scope restrictions expressed as typing conditions.Aggregate tokens pair an aggregate function with the ordered occurrence sequence of the group that produced them.Source: B Material for Section 3 (A… · p. 24
  • Aggregate groups retain pending existence factors until comparison; a possible-world sum subsumes the factor when the predicate entails group existence, avoiding double counting in nonidempotent m-semirings.Predicates that can hold for an empty group do not subsume the factor.Source: B Material for Section 3 (A… · p. 24
  • The general semantics agrees with the earlier definition on direct comparison sites, and results for grouping comparisons extend to corresponding sites in arbitrary queries.At a site, the output carries group keys and aggregate values annotated by the predicate provenance.Source: B Material for Section 3 (A… · pp. 24–25
  • ProvSQL’s rewriting compiles aggregate predicates into comparison and indicator gates, combining Boolean connectives with semiring operations and retaining a group-existence guard when needed.The rewritten site computes the annotation assigned by the general semantics relative to those gates.Source: B Material for Section 3 (A… · p. 25

C.1 Proof of Theorem 12

The section proves the HAVING COUNT(*) provenance equivalence with a self-join rewriting by establishing a bounded-count identity and matching recurrences, and uses counterexamples to isolate the roles of absorptivity and distributivity of times over monus. It also notes that absorptivity alone suffices for positive rewritings of monotone conditions.

C.1 Proof of Theorem 12

  • Lemma 26 factors TU(W) as AW ⊗ (1 ⊖ EW) before applying distributivity, avoiding a monus bound that would move in the wrong direction.Absorptivity ensures products only decrease as factors are added, supporting the bound on each world’s contribution.Source: §C.1 · p. 30
  • For arity-2 aggregate-free queries with occurrence identifiers, HAVING COUNT(*) and the self-join rewriting agree for ⩽, =, and ⩾ under absorptivity and distributivity of ⊗ over ⊖.The theorem also gives an absorptive m-semiring counterexample without distributivity for = at C=1, and an idempotent, distributive but non-absorptive m-semiring counterexample for ⩾ at C=1.Source: §C.1 · p. 30

Proof of (i)

  • The proof matches possible-world annotations with self-join annotations: identifier ordering selects each C-element occurrence set once, and duplicate elimination sums its products.The proof then uses matching FC and SC recurrences and induction on the number of occurrences to establish their equality.Source: Proof of (i) · p. 32
  • For COUNT(*) = C, the proof combines Lemma 26’s per-world upper bound with right-distributivity of ⊖ over ⊕ to establish the exact-count equality.Lemma 26 bounds each world W with j ⩽ |W| ⩽ C by Sj(U) ⊖ SC+1(U), assuming absorptivity and that ⊗ distributes over ⊖.Source: §C.1 · p. 29, Proof of (i) · p. 33
  • For COUNT(*) ≤ C, the provenance is S1(U) ⊖ S_C+1(U), equal to the sum of annotations of worlds whose sizes lie between 1 and C.The proof bounds each qualifying world’s contribution and uses absorptivity to show larger worlds are removed by monus.Source: Proof of (i) · pp. 33–34

Proof of (ii)

  • In an absorptive five-element chain that is not ⊗/⊖-distributive, a group with three occurrences annotated e2, e3, and e3 has only singleton possible worlds satisfying HAVING COUNT(*) = 1.For each occurrence i, the product of the other annotations is e3, and 1 ⊖ e3 = 1.Source: Proof of (ii) · p. 34

Proof of (iii)

  • In tropical K2, which is idempotent and ⊗-over-⊖ distributive but not absorptive, two tuples annotated −1 produce provenance −2.This supplies a counterexample isolating the need for absorptivity even when distributivity holds.Source: Proof of (iii) · pp. 34–35

C.2 Monotone Conditions: Absorptivity Suffices

  • For idempotent m-semirings, monus cancels from possible-world sums over superset-closed families, and absorptivity reduces the sum to minimal worlds.The proposition applies to nonempty worlds; it does not require absorptivity or ⊗-over-⊖ distributivity for its cancellation result.Source: §C.2 · p. 35
  • For absorptive m-semirings, Theorem 29 drops ⊗/⊖ distributivity for positive aggregate-free rewritings of COUNT thresholds and specified monotone MIN/MAX conditions.The monotone conditions include COUNT(*) ≥ C or > C, MIN(t) ≤ c or < c, and MAX(t) ≥ c or > c; they may be combined using conjunction and disjunction.Source: §C.2 · p. 36

C.3 Specialization, Probabilistic Evaluation, and Complexity

The section establishes preservation of HAVING-query provenance under m-semiring homomorphisms and its agreement with classical possible-world probability evaluation. It also proves a fixed-query NP-completeness result for Boolean and natural-number polynomial semirings.

Specialization

  • HAVING-query provenance is preserved by every m-semiring homomorphism, even when aggregate comparisons occur far from their grouping.Comparisons may pass through projections, joins, unions, and further selections before evaluation.Source: §C.3 · pp. 37, 39

Probabilistic Evaluation

  • Pr(I |= Q) equals the probability of the provenance of Q over the corresponding B[X]-instance.The proof shows the Boolean provenance is true under a valuation exactly when Q holds on the associated possible world.Source: §C.3 · pp. 39–40

Complexity

  • For K in {B[X], N[X]}, nonzero provenance of a fixed Boolean HAVING query is NP-complete for a suitable fixed query.For B[X], deciding nonzero provenance for any fixed Boolean HAVING query is in NP.Source: §C.3 · p. 40
  • The hardness reduction encodes subset-sum in the data while using the fixed query HAVING SUM(v) = b.Distinct tuple variables ensure possible worlds correspond to sub-multisets; nonzero provenance holds exactly when a nonempty sub-multiset sums to the target.Source: §C.3 · pp. 40–41

D Material for Section 5 (Algorithms)

This section presents algorithms for computing HAVING-query provenance, including ValidSum and ValidCount procedures that enumerate non-empty worlds satisfying aggregate comparisons. It also establishes polynomial-time data-complexity results under specified semiring conditions and probability-evaluation bounds for comparisons with independent contributors.

D Material for Section 5 (Algorithms)

  • ValidSum and ValidCount return exactly the non-empty worlds whose SUM(t) or COUNT(*) satisfies the chosen comparison with C.For ValidCount, t is the constant 1; ValidSum permits a term taking values in N on the group-member occurrences.Source: D Material for Section 5 (Algorithms) · p. 41

Proof. Correctness of ValidSum

  • ValidSum’s dynamic program tracks worlds by total sum, then selects the totals satisfying the comparison and omits the empty world.The proof handles zero-valued occurrences by limiting updates to worlds present before appending new ones.Source: Proof. Correctness of ValidSum · p. 46

Correctness of ValidCount

  • ValidCount’s recursive Combinations procedure partitions extensions by whether they include the current occurrence, enumerating each desired world exactly once.AddExact produces the non-empty worlds of a specified cardinality, and the final comparison cases select the required cardinalities.Source: Correctness of ValidCount · pp. 47–48
  • MIN, MAX, and PICKFIRST comparisons have polynomial data complexity in absorptive m-semirings where multiplication distributes over monus; fixed-threshold COUNT(*) ≥ k and > k do as well.The proposition also lists SUM(a) ≥ c and > c for a natural-number-valued attribute, with an additional condition whose text is incomplete in the supplied passage.Source: Correctness of ValidCount · pp. 48–49
  • For fixed k, COUNT(*) = k, COUNT(*) <= k, and COUNT(*) < k have polynomial-time provenance in arbitrary m-semirings.Their satisfying worlds have sizes k, 1 through k, and 1 through k − 1, respectively.Source: Correctness of ValidCount · pp. 49–50
  • SUM(a) = c, SUM(a) <= c, and SUM(a) < c have polynomial-time provenance in arbitrary m-semirings when all values are nonzero and c <= k · a.The valid worlds are among those of size at most k, so they can be enumerated in polynomially many cases for fixed k.Source: Correctness of ValidCount · pp. 49–50
  • MIN, MAX, and PICKFIRST comparisons admit single-scan closed forms in absorptive m-semirings where times distributes over monus; monus-free MIN forms require absorptivity alone.The scan takes O(|U|) semiring operations; the four forms with a monus factor require both hypotheses.Source: Correctness of ValidCount · p. 49
  • For fixed thresholds, COUNT(*) >= k and COUNT(*) > k have polynomial-time provenance in absorptive m-semirings, using minimal satisfying worlds of sizes k and k + 1, respectively.Absorptivity collapses the sum over each upward-closed family of satisfying worlds to its minimal worlds.Source: Correctness of ValidCount · p. 50
  • For fixed k, SUM(a) >= c and SUM(a) > c have polynomial-time provenance in absorptive m-semirings, with minimal satisfying worlds bounded in size by k and k + 1, respectively.The bound assumes nonnegative values satisfying c <= k · a; strict comparisons allow one additional nonzero occurrence.Source: Correctness of ValidCount · p. 50
  • For independent contributors, SUM(t) comparisons cost O(N · min(C, S)) and MIN/MAX comparisons cost O(N); COUNT comparisons use Poisson-binomial CDF queries.The SUM bound assumes integer weights and S = Σ_i t(u_i); the COUNT procedure evaluates the relevant tails of the contributor-count distribution.Source: Correctness of ValidCount · p. 51

E Material for Section 6 (Implementation and Experiments)

The implementation material gives ProvSQL SQL templates for HAVING COUNT(*) bounds and equivalent self-join rewritings, including a difference-based form for upper bounds.

HAVING-based templates

  • The HAVING template groups matching rows by image and filters groups with COUNT(*) >= k or COUNT(*) <= k.The template projects provenance and removes rows whose provenance is zero.Source: E Material for Section 6… · p. 52

Probability evaluation

  • For probability evaluation, the templates replace sr_formula with probability_evaluate and filter out images with zero probability.Under the HAVING semantics, those images have no possible world in which the aggregate comparison holds.Source: E Material for Section 6… · pp. 52–53

Self-join rewritings

F Dependency Graph of the Results

Figure 2 summarizes dependencies among the paper’s results by indicating which proofs use earlier results.

Dependency graph

Related papers

Loading 2609.31246v1…