 |
ProvSQL C/C++ API
Adding support for provenance and uncertainty management to PostgreSQL databases
|
|
ProvSQL C/C++ API
Adding support for provenance and uncertainty management to PostgreSQL databases
|
Exact closed-form HAVING COUNT(*) op C probability over safe-join lineage – the recursive marginal-vector engine of the Ré-Suciu HAVING trichotomy (see doc/source/dev/probability-evaluation.rst).
More...
#include "GenericCircuit.h"
Go to the source code of this file.
Namespaces | |
| namespace | provsql |
Functions | |
| unsigned | provsql::runAggMarginalEvaluator (GenericCircuit &gc) |
Run the safe-join aggregate marginal-vector pre-pass over gc. | |
Exact closed-form HAVING COUNT(*) op C probability over safe-join lineage – the recursive marginal-vector engine of the Ré-Suciu HAVING trichotomy (see doc/source/dev/probability-evaluation.rst).
CountCmpEvaluator (the flat Poisson-binomial pre-pass) is exact only when the gate_agg children are pairwise leaf-disjoint, i.e. flat single-table COUNT. A join makes two aggregate-input rows share a base tuple (fan-out, e.g. R(k,a),S(a,b) with several b per a), so the contributors stop being independent Bernoulli trials and CountCmpEvaluator bails to provsql_having's exponential enumeration.
This pass generalises the flat case to any hierarchical (laminar) join: each contributor is a product (conjunction) of gate_input leaves (nested gate_times from SPJ subqueries / views is flattened, since times is AND on the probability path, so detection is invariant to join order and subquery nesting), and the count distribution is computed recursively down the hierarchy. At each level the contributors partition into independent blocks (by shared leaf); a block factors out the leaves common to every member (this level's shared "root" event) and the block count is the disjoint mixture \((1-p_{\text{root}})\,\delta_0 + p_{\text{root}}\,m_{\text{inner}}\) (the ⊥ combinator), where \(m_{\text{inner}}\) is the same construction applied to the per-member residual leaf sets one level deeper; independent blocks combine by convolution (the ⊛^+ combinator). Single-level fan-out (R(k,a),S(a,b)) is the case where every residual is one leaf and \(m_{\text{inner}}\) is a Poisson-binomial; deeper nesting (orders→items under a user) recurses further. The answer is \(\sum_{c\ge 1,\;c\,\theta\,C} m[c]\) over the resulting count PMF m, with the empty group (c = 0) excluded exactly as in CountCmpEvaluator / SQL HAVING semantics.
A multi-member block with no common leaf is the join (Cartesian product) node R(a),S(a,b),T(a,c): the contributors are the complete product of per-factor parts, so count is the product of the per-factor counts. A SUM whose value lives on one factor is \(S_f\cdot M\) (that factor's weighted sum times the others' count product); a branch-spanning value that is additively separable across factors (e.g. sum(b+c)) is \(\sum_f S_f\cdot\prod_{g\ne f} N_g\), folded exactly from the per-factor joint (sum,count) distributions (sumCountPMF); a multiplicatively separable value (e.g. sum(b*c)) is \(\prod_f S_f\), the product of the per-factor weighted sums (mulSeparableSumPMF). A value that is neither (e.g. sum(b*c+b+c)) couples the factors and self-gates back to enumeration.
Soundness is circuit-only and self-gating. No planner-time skeleton certificate is consulted: the recursion is exact iff at every level each multi-member block has a leaf common to all its members (and every involved leaf is private to the cmp subtree). A non-laminar shape – e.g. the triangle R(x,y),S(y,z),T(z,x) – produces a multi-member block with no common leaf at some level, which clears the soundness flag and falls the cmp through to exact enumeration. This circuit-only recursion covers the tuple-independent hierarchical class at any depth.
**BID blocks (COUNT / SUM / AVG / MIN / MAX).** A repair_key block surfaces in the circuit as a set of gate_mulinput contributors sharing a block-key child, mutually exclusive with per-alternative probabilities. Such a contributor is recognised and the block handled as a categorical (at most one alternative present, the null arm Σp_i<1 contributing 0), independent of the TID part and of other blocks: COUNT / SUM / AVG convolve the block's count / weighted-sum distribution, and MIN / MAX fold a per-block factor (1-Σ_{pred} p_alt) into each pAllAbsent over a value-thresholded subset. No planner certificate is needed, since the block is visible in the circuit. The residual genuinely certificate-only case is a declared key on a plain TID table (mutual exclusion in block_key metadata only, no mulinput): that would need a planner CERT_SAFE_AGG_PLAN.
Non-read-once UNION / EXCEPT contributors. A UNION / EXCEPT over a join that re-uses a base tuple gives a contributor that is a gate_plus / gate_monus repeating the shared leaf – (r∧s)∨(r∧t) or (r∧s)∖(r∧t) – which contributorProb (read-once only) rejects. When the contributor's footprint is private (so it is independent of every other contributor), contributorExactMarginal computes its exact marginal by brute force over its private leaves (the internal sharing resolved exactly) and the contributor is modelled as a one-alternative BID block – an independent event – reusing the categorical machinery above. A base tuple shared across contributors of the same group is genuinely \(\#P\)-hard and bails.
Runs as a probability-side pre-pass in probability_evaluate.cpp, after runCountCmpEvaluator (so the cheap flat path still wins where it applies; this pass only ever sees the join-shaped cmps the flat pass left behind), gated by the same provsql.cmp_probability_evaluation GUC and sharing its sound-only contract (replace the gate_cmp by a Bernoulli gate_input, meaningless to symbolic semirings).
Definition in file AggMarginalEvaluator.h.