 |
ProvSQL SQL API
Adding support for provenance and uncertainty management to PostgreSQL databases
|
|
ProvSQL SQL API
Adding support for provenance and uncertainty management to PostgreSQL databases
|
Functions for computing probabilities, expected values, and game-theoretic contribution measures (Shapley/Banzhaf values) from provenance circuits. More...
Functions | |
| DOUBLE PRECISION | provsql.probability_evaluate (UUID token, TEXT method=NULL, TEXT arguments=NULL) |
| Compute the probability of a provenance token. | |
| DOUBLE PRECISION | provsql.probability (UUID token, TEXT method=NULL, TEXT arguments=NULL) |
| Short alias of probability_evaluate. | |
| DOUBLE PRECISION | provsql.probability (BOOLEAN predicate, TEXT method=NULL, TEXT arguments=NULL) |
| Probability of a Boolean event over random variables. | |
| VOID | provsql.probability_bounds (UUID token, OUT DOUBLE PRECISION lower, OUT DOUBLE PRECISION upper) |
| Cheap certified probability interval of a DNF-shaped circuit. | |
| DOUBLE PRECISION | provsql.expected (ANYELEMENT input, UUID prov=gate_one(), TEXT method=NULL, TEXT arguments=NULL) |
| Compute the expected value of a probabilistic scalar. | |
| DOUBLE PRECISION | provsql.rv_moment (UUID token, INTEGER k, BOOLEAN central, UUID prov=gate_one()) |
| Internal: shared C entry point for variance / moment / central_moment. | |
| DOUBLE PRECISION | provsql.agg_avg_moment_exact (UUID token, INTEGER k) |
Exact E[AVG^k | COUNT >= 1] over independent rows (the joint (sum, count) fold); NULL when the shape is out of scope (shared leaves, compound contributors), signalling agg_raw_moment's avg arm to fall back to the Monte-Carlo scalar path. | |
| DOUBLE PRECISION | provsql.agg_collapsed_moment (UUID token, INTEGER k) |
| Collapsed (Rao-Blackwellised) raw moment E[C^k] of a correlated COUNT / SUM whose per-row selection events are coupled through a single shared continuous latent: 1-D quadrature over the latent, closed-form per-row CDF given it (O(G·n), exact up to the grid). | |
| DOUBLE_PRECISION[] | provsql.agg_collapsed_moments (UUID token) |
| Both collapsed raw moments {E[C], E[C^2]} of a correlated COUNT / SUM from a single circuit load and plan build; NULL when the shared-latent pattern does not match. | |
| UUID | provsql.agg_defined_event (UUID token) |
| Boolean event "this aggregate-carrying gate's value is defined
(non-NULL) in the world". | |
| DOUBLE PRECISION | provsql.agg_raw_moment (AGG_TOKEN token, INTEGER k, UUID prov=gate_one(), TEXT method=NULL, TEXT arguments=NULL) |
| Compute the raw moment E[X^k | prov] of an AGG_TOKEN aggregate. | |
| DOUBLE PRECISION | provsql.variance (ANYELEMENT input, UUID prov=gate_one(), TEXT method=NULL, TEXT arguments=NULL) |
| Compute the variance Var[X | prov] of a probabilistic scalar. | |
| DOUBLE PRECISION | provsql.moment (ANYELEMENT input, INTEGER k, UUID prov=gate_one(), TEXT method=NULL, TEXT arguments=NULL) |
| Compute the raw moment E[X^k | prov] of a probabilistic scalar. | |
| DOUBLE PRECISION | provsql.rv_quantile (UUID token, DOUBLE PRECISION p, UUID prov=gate_one()) |
| Internal: rv-side quantile computation. | |
| DOUBLE PRECISION | provsql.quantile (ANYELEMENT input, DOUBLE PRECISION p, UUID prov=gate_one(), TEXT method=NULL, TEXT arguments=NULL) |
| Compute the p-quantile (inverse CDF) of a probabilistic scalar. | |
| VOID | provsql.rv_support (UUID token, UUID prov=gate_one(), float8 &lo, float8 &hi) |
| Internal: rv-side support computation. | |
| VOID | provsql.support (ANYELEMENT input, UUID prov=gate_one(), TEXT method=NULL, TEXT arguments=NULL, float8 &lo, float8 &hi) |
Compute the support interval | |
| DOUBLE PRECISION | provsql.central_moment (ANYELEMENT input, INTEGER k, UUID prov=gate_one(), TEXT method=NULL, TEXT arguments=NULL) |
| Compute the central moment E[(X - E[X|prov])^k | prov]. | |
| DOUBLE PRECISION | provsql.rv_covariance (UUID x, UUID y, UUID prov) |
| C entry point behind covariance (UUID-level binding). | |
| DOUBLE PRECISION | provsql.covariance (random_variable x, random_variable y, UUID prov=gate_one()) |
| Covariance Cov(X, Y) = E[XY] − E[X]·E[Y] of two random variables. | |
| DOUBLE PRECISION | provsql.stddev (random_variable x, UUID prov=gate_one()) |
| Standard deviation σ(X) = √Var(X) of a random variable. | |
| DOUBLE PRECISION | provsql.rv_correlation (UUID x, UUID y, UUID prov) |
| C entry point behind correlation (UUID-level binding). | |
| DOUBLE PRECISION | provsql.correlation (random_variable x, random_variable y, UUID prov=gate_one()) |
| Pearson correlation ρ(X, Y) = Cov(X, Y) / (σ(X)·σ(Y)). | |
| DOUBLE PRECISION | provsql.rv_entropy (UUID token, UUID prov) |
| C entry point behind entropy (UUID-level binding). | |
| DOUBLE PRECISION | provsql.entropy (random_variable x, UUID prov=gate_one()) |
| Entropy H(X) of a random variable, in nats. | |
| DOUBLE PRECISION | provsql.rv_kl (UUID p, UUID q) |
| C entry point behind kl (UUID-level binding). | |
| DOUBLE PRECISION | provsql.kl (random_variable p, random_variable q) |
| Kullback-Leibler divergence KL(P || Q), in nats. | |
| DOUBLE PRECISION | provsql.rv_mutual_information (UUID x, UUID y) |
| C entry point behind mutual_information (UUID-level binding). | |
| DOUBLE PRECISION | provsql.mutual_information (random_variable x, random_variable y) |
| Mutual information I(X; Y), in nats. | |
| DOUBLE PRECISION | provsql.shapley (UUID token, UUID variable, TEXT method=NULL, TEXT arguments=NULL, BOOLEAN banzhaf='f') |
| Compute the Shapley value of an input variable. | |
| SETOF RECORD | provsql.shapley_all_vars (UUID token, TEXT method=NULL, TEXT arguments=NULL, BOOLEAN banzhaf='f', OUT UUID variable, OUT DOUBLE PRECISIONvalue) |
| Compute Shapley values for all input variables at once. | |
| DOUBLE PRECISION | provsql.banzhaf (UUID token, UUID variable, TEXT method=NULL, TEXT arguments=NULL) |
| Compute the Banzhaf power index of an input variable. | |
| SETOF RECORD | provsql.banzhaf_all_vars (UUID token, TEXT method=NULL, TEXT arguments=NULL, OUT UUID variable, OUT DOUBLE PRECISIONvalue) |
| Compute Banzhaf power indices for all input variables at once. | |
| DOUBLE PRECISION | provsql.reachability_evaluate (INT[] sources, INT[] destinations, UUID[] tokens, DOUBLE_PRECISION[] probabilities, INT source, INT target, BOOLEAN directed) |
| Exact reachability probability over bounded-treewidth data (columnar form). | |
| VOID | provsql.reachability_compile_stats (INT[] sources, INT[] destinations, UUID[] tokens, DOUBLE_PRECISION[] probabilities, INT source, INT target, BOOLEAN directed, OUT DOUBLE PRECISIONprobability, OUT INT data_treewidth, OUT BIGINT nb_bags, OUT BIGINT max_states, OUT BIGINT nb_gates, OUT BIGINT nb_variables) |
| Reachability probability plus compilation statistics (columnar form). | |
| VOID | provsql.ucq_joint_compile_stats (INT[] disjunct_nvars, INT[] atom_disjunct, INT[] atom_rel, INT[] atom_vars, INT[] atom_arity, INT[] fact_rel, INT[] fact_elems, INT[] fact_arity, UUID[] fact_tokens, DOUBLE_PRECISION[] fact_probs, OUT DOUBLE PRECISIONprobability, OUT INT joint_treewidth, OUT INT data_treewidth_lb, OUT INT circuit_treewidth_lb, OUT BIGINT n_bags, OUT BIGINT max_states, OUT BIGINT dd_size, OUT INT n_enumerating) |
| Boolean UCQ probability plus compilation statistics (columnar form, internal). | |
| VOID | provsql.ucq_joint_compile_stats (JSONB query, INT[] fact_rel, INT[] fact_elems, INT[] fact_arity, UUID[] fact_tokens, DOUBLE_PRECISION[] fact_probs, OUT DOUBLE PRECISIONprobability, OUT INT joint_treewidth, OUT INT data_treewidth_lb, OUT INT circuit_treewidth_lb, OUT BIGINT n_bags, OUT BIGINT max_states, OUT BIGINT dd_size, OUT INT n_enumerating) |
| Boolean UCQ probability plus statistics from a JSON specification. | |
| VOID | provsql.ucq_joint_compile_stats_tracked (INT[] disjunct_nvars, INT[] atom_disjunct, INT[] atom_rel, INT[] atom_vars, INT[] atom_arity, INT[] fact_rel, INT[] fact_elems, INT[] fact_arity, UUID[] fact_tokens, OUT DOUBLE PRECISIONprobability, OUT INT joint_treewidth, OUT INT data_treewidth_lb, OUT INT circuit_treewidth_lb, OUT BIGINT n_bags, OUT BIGINT max_states, OUT BIGINT dd_size, OUT INT n_enumerating) |
| Correlated Boolean UCQ probability plus compilation statistics (columnar form, internal). | |
| VOID | provsql.ucq_joint_compile_stats_tracked (JSONB query, INT[] fact_rel, INT[] fact_elems, INT[] fact_arity, UUID[] fact_tokens, OUT DOUBLE PRECISIONprobability, OUT INT joint_treewidth, OUT INT data_treewidth_lb, OUT INT circuit_treewidth_lb, OUT BIGINT n_bags, OUT BIGINT max_states, OUT BIGINT dd_size, OUT INT n_enumerating) |
| Correlated Boolean UCQ probability plus statistics from a JSON spec. | |
| UUID | provsql.ucq_joint_materialize_tracked (INT[] disjunct_nvars, INT[] atom_disjunct, INT[] atom_rel, INT[] atom_vars, INT[] atom_arity, INT[] fact_rel, INT[] fact_elems, INT[] fact_arity, UUID[] fact_tokens) |
| Compile a correlated UCQ and materialise its certified d-D, returning the root provenance token (columnar form, internal). | |
| UUID | provsql.ucq_joint_materialize_tracked (JSONB query, INT[] fact_rel, INT[] fact_elems, INT[] fact_arity, UUID[] fact_tokens) |
| Compile a correlated UCQ and materialise its certified d-D from a JSON spec, returning the root provenance token. | |
| UUID | provsql.ucq_joint_provenance (JSONB descriptor, UUID fallback=NULL) |
| Compile a UCQ over named relations into a materialised certified d-D, gathering the facts from the store – the descriptor-driven engine. | |
| UUID | provsql.ucq_mobius_materialize_tracked (INT[] disjunct_nvars, INT[] atom_disjunct, INT[] atom_rel, INT[] atom_vars, INT[] atom_arity, INT[] fact_rel, INT[] fact_elems, INT[] fact_arity, UUID[] fact_tokens, UUID lineage=NULL) |
| =========================================================================== Safe-UCQ Möbius-inversion route (mobius_evaluate.cpp). | |
| VOID | provsql.ucq_mobius_compile_stats (INT[] disjunct_nvars, INT[] atom_disjunct, INT[] atom_rel, INT[] atom_vars, INT[] atom_arity, INT[] fact_rel, INT[] fact_elems, INT[] fact_arity, UUID[] fact_tokens, OUT DOUBLE PRECISIONprobability, OUT INT n_components, OUT INT n_cnf_conjuncts, OUT INT lattice_size, OUT INT n_nonzero, OUT INT n_cancelled, OUT BOOLEAN cancelled_hard, OUT BIGINT dd_size, OUT BIGINT memo_hits) |
| Compile the Möbius circuit and return the lattice statistics plus the probability (the demonstrability surface). | |
| UUID | provsql.mobius_or_null (UUID tok) |
Pass a token through iff it is a gate_mobius, else return NULL. | |
| UUID | provsql.ucq_mobius_provenance (JSONB descriptor, UUID fallback=NULL) |
| Möbius-route provenance from a descriptor (the planner-substituted entry point, and the manual one). | |
| RECORD | provsql.mobius_compile_stats (JSONB descriptor, OUT DOUBLE PRECISIONprobability, OUT INT n_components, OUT INT n_cnf_conjuncts, OUT INT lattice_size, OUT INT n_nonzero, OUT INT n_cancelled, OUT BOOLEAN cancelled_hard, OUT BIGINT dd_size, OUT BIGINT memo_hits) |
| Möbius lattice statistics + probability from a descriptor: the demonstrability SRF. | |
| VOID | provsql.ucq_joint_gather (JSONB descriptor, INT[] &disjunct_nvars, INT[] &atom_disjunct, INT[] &atom_rel, INT[] &atom_vars, INT[] &atom_arity, INT[] &fact_rel, INT[] &fact_elems, INT[] &fact_arity, UUID[] &fact_tokens, TEXT[] &val_by_id) |
Internal gather for the per-answer joint route: parse descriptor into the columnar UCQ arrays and gather every fact (relation index, dense element ids, provenance token) with the value dictionary. | |
| UUID | provsql.ucq_joint_provenance_answer (JSONB descriptor, INT[] head_vars, TEXT[] head_vals, UUID fallback=NULL) |
| Per-answer joint-width provenance via the TOP-DOWN single DP (planner-substituted, C). | |
| UUID | provsql.ucq_mobius_provenance_answer (JSONB descriptor, INT[] head_vars, TEXT[] head_vals, UUID fallback=NULL) |
| Per-answer safe-UCQ Möbius provenance (planner-substituted): one head-pinned Möbius circuit per output group. | |
| SETOF RECORD | provsql.reachability_materialize (INT[] sources, INT[] destinations, UUID[] tokens, DOUBLE_PRECISION[] probabilities, UUID[] block_keys, INT[] block_indices, INT[] source_vertices, UUID[] source_tokens, DOUBLE_PRECISION[] source_probabilities, BOOLEAN directed, OUT INT vertex, OUT UUID token) |
| Compile and materialise the reachability provenance of every vertex (columnar form, internal). | |
| SETOF RECORD | provsql.reachability_materialize_hops (INT[] sources, INT[] destinations, UUID[] tokens, DOUBLE_PRECISION[] probabilities, UUID[] block_keys, INT[] block_indices, INT[] source_vertices, UUID[] source_tokens, DOUBLE_PRECISION[] source_probabilities, BOOLEAN directed, INT hop_bound, INT hop_seed, OUT INT vertex, OUT INT hops, OUT UUID token) |
Bounded-hop variant of reachability_materialize() (internal). | |
| SETOF RECORD | provsql.reachability_materialize_any (INT[] sources, INT[] destinations, UUID[] tokens, DOUBLE_PRECISION[] probabilities, UUID[] block_keys, INT[] block_indices, INT[] source_vertices, UUID[] source_tokens, DOUBLE_PRECISION[] source_probabilities, BOOLEAN directed, INT[] group_ids, INT[] member_vertices, OUT INT group_id, OUT UUID token) |
| Per-group "some member reachable" compilation (columnar form, internal). | |
| UUID | provsql.reachability_materialize_cover (INT[] sources, INT[] destinations, UUID[] tokens, DOUBLE_PRECISION[] probabilities, UUID[] block_keys, INT[] block_indices, INT[] source_vertices, UUID[] source_tokens, DOUBLE_PRECISION[] source_probabilities, BOOLEAN directed, INT[] member_vertices) |
| Compile and materialise the "every member vertex reachable" (k-terminal / coverage) circuit (columnar form, internal). | |
| VOID | provsql.plant_reach_any_groups (TEXT work_name, TEXT node_attribute, REGCLASS member_rel, TEXT member_attribute, TEXT group_attribute, REGCLASS edge_rel, TEXT source_attribute, TEXT destination_attribute, TEXT source_value, BOOLEAN directed, TEXT edge_quals=NULL, REGCLASS source_rel=NULL, TEXT source_rel_attribute=NULL, TEXT edge_sql=NULL, TEXT member_quals=NULL) |
| Plant certified any-member-reachable gates for a grouped reachability aggregation (internal). | |
| VOID | provsql.plant_reach_cover (TEXT work_name, TEXT node_attribute, REGCLASS edge_rel, TEXT source_attribute, TEXT destination_attribute, TEXT source_value, BOOLEAN directed, TEXT[] node_values, TEXT edge_quals=NULL, REGCLASS source_rel=NULL, TEXT source_rel_attribute=NULL, TEXT edge_sql=NULL) |
| Plant the certified all-members-reachable gate for a reachability self-join conjunction (internal). | |
| UUID[] | provsql.token_conjunctive_leaves (UUID token) |
| Input leaves of a conjunction-shaped provenance token (internal). | |
| VOID | provsql.gather_reachability_edges (REGCLASS rel, TEXT source_attribute, TEXT destination_attribute, TEXT[] extra_vertices, TEXT edge_quals=NULL, TEXT rel_sql=NULL, INT[] &sources, INT[] &destinations, UUID[] &tokens, DOUBLE_PRECISION[] &probabilities, UUID[] &block_keys, INT[] &block_indices, INT[] &extra_ids, TEXT[] &vertices) |
| Gather the edges of a tracked relation in the columnar form expected by reachability_evaluate (internal). | |
| VOID | provsql.gather_reachability_sources (REGCLASS rel, TEXT source_attribute, TEXT[] &source_values, UUID[] &source_tokens, DOUBLE_PRECISION[] &source_probabilities) |
| Gather a source relation's vertices, tokens and probabilities (internal). | |
| VOID | provsql.eval_reachability (REGCLASS edge_rel, TEXT source_attribute, TEXT destination_attribute, TEXT source_value, BOOLEAN directed, TEXT work_name, TEXT colnames, TEXT coldef, TEXT coltype, TEXT body_sql, TEXT edge_quals=NULL, REGCLASS source_rel=NULL, TEXT source_rel_attribute=NULL, TEXT edge_sql=NULL, INT hop_bound=NULL, INT hop_seed=NULL, INT hops_position=NULL) |
| Fixpoint driver for the recursive reachability shape: decomposition-aligned compilation with fallback to eval_recursive. | |
Functions for computing probabilities, expected values, and game-theoretic contribution measures (Shapley/Banzhaf values) from provenance circuits.
| DOUBLE PRECISION provsql.agg_avg_moment_exact | ( | UUID | token, |
| INTEGER | k ) |
Exact E[AVG^k | COUNT >= 1] over independent rows (the joint (sum, count) fold); NULL when the shape is out of scope (shared leaves, compound contributors), signalling agg_raw_moment's avg arm to fall back to the Monte-Carlo scalar path.
| DOUBLE PRECISION provsql.agg_collapsed_moment | ( | UUID | token, |
| INTEGER | k ) |
Collapsed (Rao-Blackwellised) raw moment E[C^k] of a correlated COUNT / SUM whose per-row selection events are coupled through a single shared continuous latent: 1-D quadrature over the latent, closed-form per-row CDF given it (O(G·n), exact up to the grid).
NULL when the circuit does not match the shared-latent pattern (caller falls back to the exact n^k enumeration). k in {1, 2}.
| DOUBLE_PRECISION[] provsql.agg_collapsed_moments | ( | UUID | token | ) |
Both collapsed raw moments {E[C], E[C^2]} of a correlated COUNT / SUM from a single circuit load and plan build; NULL when the shared-latent pattern does not match.
variance() uses this so a mean+variance readout traverses the circuit once rather than calling agg_collapsed_moment twice (the load and O(n) plan build dominate once the grid loop is arithmetic).
| UUID provsql.agg_defined_event | ( | UUID | token | ) |
Boolean event "this aggregate-carrying gate's value is defined (non-NULL) in the world".
Backs the conditional-on-defined convention of the aggregate moment readouts: sum / count (and constants) have a value in every world – the empty group is the real value 0 – so their defined event is gate_one(); min / max / avg (and any other aggregate) are NULL on an empty group, so their defined event is "some contributing row is present", the OR of the semimod children's row tokens; a case gate's value is defined iff its first-match selected branch's value is (the same region walk as the moment evaluator, conjoined per branch). Anything else (an arith composite, whose AGG_TOKEN running value is total) counts as always defined.
| DOUBLE PRECISION provsql.agg_raw_moment | ( | AGG_TOKEN | token, |
| INTEGER | k, | ||
| UUID | prov = gate_one(), | ||
| TEXT | method = NULL, | ||
| TEXT | arguments = NULL ) |
Compute the raw moment E[X^k | prov] of an AGG_TOKEN aggregate.
Sister of expected() for the AGG_TOKEN side of the polymorphic moment / variance / central_moment dispatch. Supports the same aggregation functions as expected: SUM (which COUNT normalises to at the gate level via Aggregation.cpp:322), MIN, MAX, and AVG (exact over independent / laminar rows via the joint (sum, count) distribution, Monte-Carlo scalar fallback otherwise). MIN / MAX / AVG are NULL on an empty group, so their moments are CONDITIONAL on the aggregate being defined – NULL only when it never is; SUM / COUNT treat the empty world as the real value 0.
Strategy:
prov when conditioning), and evaluate the probability via probability_evaluate.v with v^k in the rank-based enumeration that expected already uses; MAX is handled by sign-flipping per the existing trick (negate vs. rerank), with the outer multiplier becoming \((-1)^k\) instead of just \(-1\).Cost: SUM is \(O(n^k)\) probability evaluations – tractable for small k or small n; for larger sizes, prefer reaching for the sampler. MIN / MAX stay linear in n.
| DOUBLE PRECISION provsql.banzhaf | ( | UUID | token, |
| UUID | variable, | ||
| TEXT | method = NULL, | ||
| TEXT | arguments = NULL ) |
Compute the Banzhaf power index of an input variable.
| SETOF RECORD provsql.banzhaf_all_vars | ( | UUID | token, |
| TEXT | method = NULL, | ||
| TEXT | arguments = NULL, | ||
| OUT UUID | variable, | ||
| OUT DOUBLE PRECISION | value ) |
Compute Banzhaf power indices for all input variables at once.
| DOUBLE PRECISION provsql.central_moment | ( | ANYELEMENT | input, |
| INTEGER | k, | ||
| UUID | prov = gate_one(), | ||
| TEXT | method = NULL, | ||
| TEXT | arguments = NULL ) |
Compute the central moment E[(X - E[X|prov])^k | prov].
k = 0 returns 1; k = 1 returns 0; k = 2 is equivalent to variance(input, prov, ...). Polymorphic dispatcher: routes random_variable through rv_moment, and AGG_TOKEN through the binomial expansion \(E[(X-\mu)^k|A] = \sum_{i=0}^{k} \binom{k}{i} (-\mu)^{k-i} E[X^i|A]\) with \(\mu = E[X|A]\), where each \(E[X^i|A]\) comes from agg_raw_moment.
| DOUBLE PRECISION provsql.correlation | ( | random_variable | x, |
| random_variable | y, | ||
| UUID | prov = gate_one() ) |
Pearson correlation ρ(X, Y) = Cov(X, Y) / (σ(X)·σ(Y)).
Same exact tiers as covariance; on the Monte-Carlo path the covariance and BOTH standard deviations are read off the same coupled pass, instead of stacking five independent estimates (three for the covariance, one per standard deviation). Returns NULL when either standard deviation is 0 (a degenerate / constant variable, for which correlation is undefined) rather than raising a division-by-zero.
| x | the first random variable. |
| y | the second random variable. |
| prov | optional conditioning event; default gate_one() (unconditional). |
| DOUBLE PRECISION provsql.covariance | ( | random_variable | x, |
| random_variable | y, | ||
| UUID | prov = gate_one() ) |
Covariance Cov(X, Y) = E[XY] − E[X]·E[Y] of two random variables.
The bivariate readout complementing the univariate moment surface (expected / variance / moment / central_moment). Exact tiers: an exact 0 when the two arguments' stochastic-leaf footprints are structurally independent (given prov), a variance readout when the two arguments coincide, and the closed-form E[XY] − E[X]·E[Y] whenever every factor decomposes analytically. When some factor has no closed form, a SINGLE coupled Monte-Carlo pass over the joint circuit draws (x, y) pairs (shared leaves produce one draw both observe) and returns the sample covariance – the estimator's noise then scales with the covariance signal itself, not with the product of the means as the naive three-run E[XY] − E[X]·E[Y] subtraction would.
| x | the first random variable. |
| y | the second random variable. |
| prov | optional conditioning event (a provenance UUID); the default gate_one() is the unconditional covariance. Conditioning is applied jointly: the Monte-Carlo pass rejection-samples the pair on prov, giving Cov(X, Y | prov). |
| DOUBLE PRECISION provsql.entropy | ( | random_variable | x, |
| UUID | prov = gate_one() ) |
Entropy H(X) of a random variable, in nats.
Shannon entropy for a discrete distribution (a categorical / discrete count / constant – a point mass has entropy 0), differential entropy for a continuous one (quadrature of -f ln f over the family's integration range; also exact through independent-arm Bernoulli mixture trees such as gmm's). Shapes with no closed density (arithmetic composites) and the conditional form fall back to a Monte Carlo histogram plug-in estimate at the provsql.rv_mc_samples budget.
| x | the random variable. |
| prov | optional conditioning event; default gate_one() (unconditional). |
| VOID provsql.eval_reachability | ( | REGCLASS | edge_rel, |
| TEXT | source_attribute, | ||
| TEXT | destination_attribute, | ||
| TEXT | source_value, | ||
| BOOLEAN | directed, | ||
| TEXT | work_name, | ||
| TEXT | colnames, | ||
| TEXT | coldef, | ||
| TEXT | coltype, | ||
| TEXT | body_sql, | ||
| TEXT | edge_quals = NULL, | ||
| REGCLASS | source_rel = NULL, | ||
| TEXT | source_rel_attribute = NULL, | ||
| TEXT | edge_sql = NULL, | ||
| INT | hop_bound = NULL, | ||
| INT | hop_seed = NULL, | ||
| INT | hops_position = NULL ) |
Fixpoint driver for the recursive reachability shape: decomposition-aligned compilation with fallback to eval_recursive.
Called (at plan time, over SPI) by the recursive-CTE lowering when the provenance class is 'absorptive' or 'BOOLEAN' (provsql.provenance) and the CTE matches the linear reachability shape over a tracked base edge relation. Attempts the decomposition-aligned route – gather the edges, compile every reachable vertex's certified provenance circuit along a tree decomposition of the data graph, materialise them, and fill the working table with one tokenised row per reachable vertex. On any failure (data treewidth above the cap, per-node state bound, edges that are not independent base tuples...), falls back to the generic eval_recursive() fixpoint, preserving its behaviour exactly.
| edge_rel | the provenance-tracked edge relation |
| source_attribute | name of the source-vertex column |
| destination_attribute | name of the destination-vertex column |
| source_value | the base arm's constant, as TEXT |
| directed | if false, each edge can be traversed both ways |
| work_name | name of the working temp table (the CTE name) |
| colnames | comma-separated user column names (for the fallback) |
| coldef | column definitions of the working table |
| coltype | type of the CTE's single column |
| body_sql | deparsed CTE body (for the fallback) |
| edge_quals | optional deterministic filter over edge columns (deparsed from the recursive arm's WHERE clause) |
| source_rel | source relation of a multi-source base arm (SELECT col FROM sources), NULL for the constant form; tracked sources form a probabilistic source set, untracked ones are certain |
| source_rel_attribute | the source relation's vertex column |
| edge_sql | deparsed edge subquery when the recursive arm joins a derived (join-defined) edge relation instead of a base one; NULL for the REGCLASS form |
| hop_bound | maximum number of recursive steps for the hop-counting CTE shape (NULL for plain reachability) |
| hop_seed | the base arm's hop constant (hop-counting shape) |
| hops_position | 1-based position of the hop column among the CTE's two columns (hop-counting shape) |
| DOUBLE PRECISION provsql.expected | ( | ANYELEMENT | input, |
| UUID | prov = gate_one(), | ||
| TEXT | method = NULL, | ||
| TEXT | arguments = NULL ) |
Compute the expected value of a probabilistic scalar.
Computes E[input | prov] for either an AGG_TOKEN (discrete SUM/MIN/MAX aggregation over Boolean-input gate_agg circuits, with prov as the Boolean conditioning event) or a random_variable (continuous distribution, traversed by the analytical / MC evaluator from Expectation.cpp).
Implementation: thin wrapper over moment(input, 1, prov, method,
arguments). Both branches converge on the same machinery; the AGG_TOKEN side computes E[X] as the \(k=1\) instance of the \(n^k\)-tuple enumeration in agg_raw_moment, the random_variable side calls compute_expectation through rv_moment.
| input | aggregate expression or random variable to compute E[·] of |
| prov | provenance condition (defaults to gate_one(), i.e., unconditional) |
| method | knowledge compilation method (AGG_TOKEN path only) |
| arguments | additional arguments for the method (AGG_TOKEN path only) |
| VOID provsql.gather_reachability_edges | ( | REGCLASS | rel, |
| TEXT | source_attribute, | ||
| TEXT | destination_attribute, | ||
| TEXT[] | extra_vertices, | ||
| TEXT | edge_quals = NULL, | ||
| TEXT | rel_sql = NULL, | ||
| INT[] & | sources, | ||
| INT[] & | destinations, | ||
| UUID[] & | tokens, | ||
| DOUBLE_PRECISION[] & | probabilities, | ||
| UUID[] & | block_keys, | ||
| INT[] & | block_indices, | ||
| INT[] & | extra_ids, | ||
| TEXT[] & | vertices ) |
Gather the edges of a tracked relation in the columnar form expected by reachability_evaluate (internal).
Materializes the edge relation with its provenance tokens and probabilities, maps arbitrary vertex values (compared as TEXT) onto dense INTEGER IDs, and checks that every edge tuple carries a base input token (independent tuples): reachability compilation along the data is only correct when the edges are independent events, so views or query results with derived provenance are rejected.
| rel | the provenance-tracked edge relation |
| source_attribute | name of the source-vertex column |
| destination_attribute | name of the destination-vertex column |
| extra_vertices | vertex values (as TEXT) that must be part of the dense ID space even when they touch no edge – the source set in particular; their IDs come back in extra_ids (aligned with the input) |
| edge_quals | optional deterministic filter over the edge relation's columns (SQL TEXT, deparsed by the rewriter from the recursive arm's WHERE clause), restricting which edges participate |
| rel_sql | deparsed edge subquery to gather from instead of rel (join-defined edges); the tokens are then conjunctions of base tuples, validated for shape and disjoint supports |
The vertices output maps the dense IDs back to the original vertex values (as TEXT, 1-indexed), for callers that need to label per-vertex results.
| [out] | sources | source vertex (dense ID) of each gathered edge |
| [out] | destinations | destination vertex (dense ID) of each edge |
| [out] | tokens | provenance token of each edge tuple |
| [out] | probabilities | probability of each edge tuple |
| [out] | block_keys | per-edge BID key variable (nil UUID = independent) |
| [out] | block_indices | per-edge outcome index within its block |
| [out] | extra_ids | dense IDs assigned to the extra_vertices |
| [out] | vertices | dense-ID-to-original-value map (TEXT, 1-indexed) |
| VOID provsql.gather_reachability_sources | ( | REGCLASS | rel, |
| TEXT | source_attribute, | ||
| TEXT[] & | source_values, | ||
| UUID[] & | source_tokens, | ||
| DOUBLE_PRECISION[] & | source_probabilities ) |
Gather a source relation's vertices, tokens and probabilities (internal).
For a provenance-tracked source relation, every tuple must carry a base input token (a probabilistic source set); for an untracked relation the sources are certain and the tokens come back as the nil UUID. Vertex values are returned as TEXT, for the shared dense-ID mapping of gather_reachability_edges().
| rel | the source relation | |
| source_attribute | name of the vertex column | |
| [out] | source_values | vertex value of each source tuple (as TEXT) |
| [out] | source_tokens | per-source base input token (nil UUID = certain) |
| [out] | source_probabilities | per-source probability |
| DOUBLE PRECISION provsql.kl | ( | random_variable | p, |
| random_variable | q ) |
Kullback-Leibler divergence KL(P || Q), in nats.
Exact: the defining sum for two discrete distributions (matching outcomes by value) and the defining integral (quadrature over P's integration window) for two continuous ones, including independent-arm mixture trees. Returns Infinity when P is not absolutely continuous with respect to Q – an outcome of P that Q gives zero mass, mismatched kinds (discrete vs continuous), or a region of P's support where Q's density (under)flows to zero. Both arguments must resolve to closed-form densities; arithmetic composites and conditioned variables raise.
| RECORD provsql.mobius_compile_stats | ( | JSONB | descriptor, |
| OUT DOUBLE PRECISION | probability, | ||
| OUT INT | n_components, | ||
| OUT INT | n_cnf_conjuncts, | ||
| OUT INT | lattice_size, | ||
| OUT INT | n_nonzero, | ||
| OUT INT | n_cancelled, | ||
| OUT BOOLEAN | cancelled_hard, | ||
| OUT BIGINT | dd_size, | ||
| OUT BIGINT | memo_hits ) |
Möbius lattice statistics + probability from a descriptor: the demonstrability SRF.
Gathers the same TID facts as ucq_mobius_provenance, then runs the columnar ucq_mobius_compile_stats.
| UUID provsql.mobius_or_null | ( | UUID | tok | ) |
Pass a token through iff it is a gate_mobius, else return NULL.
The Möbius-precedence dispatch (see make_provenance_expression) wraps the Möbius call in this and then COALESCE\ s it before the joint-width call: a Möbius success always roots a gate_mobius (the compiler wraps even a thin selector around the lineage), so it short-circuits and the joint-width compiler never runs; a Möbius decline returns the literal lineage (never a gate_mobius), so this yields NULL and COALESCE falls through to joint-width. The lineage token is a plain plus/times/input, so the test is unambiguous.
| DOUBLE PRECISION provsql.moment | ( | ANYELEMENT | input, |
| INTEGER | k, | ||
| UUID | prov = gate_one(), | ||
| TEXT | method = NULL, | ||
| TEXT | arguments = NULL ) |
Compute the raw moment E[X^k | prov] of a probabilistic scalar.
k must be a non-negative INTEGER. k = 0 returns 1; k = 1 is equivalent to expected(input). Polymorphic dispatcher: routes random_variable through rv_moment (analytical / MC) and AGG_TOKEN through agg_raw_moment (SUM via tuple enumeration, MIN / MAX via rank enumeration, AVG via the joint (sum, count) distribution over independent / laminar rows with a Monte-Carlo fallback).
| DOUBLE PRECISION provsql.mutual_information | ( | random_variable | x, |
| random_variable | y ) |
Mutual information I(X; Y), in nats.
Exactly 0 for structurally independent variables (disjoint stochastic-leaf footprints, the same test the moment evaluators use); H(X) for a discrete variable paired with itself and Infinity for a continuous one (I(X;X) diverges). A genuinely correlated pair (shared leaves) is estimated by a 2-D histogram plug-in over coupled joint Monte Carlo draws – both roots evaluated against the same per-iteration cache, so shared leaves keep their joint law – at the provsql.rv_mc_samples budget.
| VOID provsql.plant_reach_any_groups | ( | TEXT | work_name, |
| TEXT | node_attribute, | ||
| REGCLASS | member_rel, | ||
| TEXT | member_attribute, | ||
| TEXT | group_attribute, | ||
| REGCLASS | edge_rel, | ||
| TEXT | source_attribute, | ||
| TEXT | destination_attribute, | ||
| TEXT | source_value, | ||
| BOOLEAN | directed, | ||
| TEXT | edge_quals = NULL, | ||
| REGCLASS | source_rel = NULL, | ||
| TEXT | source_rel_attribute = NULL, | ||
| TEXT | edge_sql = NULL, | ||
| TEXT | member_quals = NULL ) |
Plant certified any-member-reachable gates for a grouped reachability aggregation (internal).
Called (at plan time, over SPI) by the recursive-CTE lowering when the outer query aggregates a reachability working table by a column of a joined, untracked member relation: GROUP BY collapses each group's per-vertex reach tokens with provenance_plus, whose disjuncts are correlated (they share edges) and would otherwise leave the certified route. For each multi-member group this pre-creates, at the canonical address of the group's token multiset, a certified single-child plus over the group's native any-member-reachable circuit (reachability_materialize_any), so the natural aggregation stays on the linear evaluation route. Best-effort: any failure leaves the generic path untouched (notice under verbosity 10).
| work_name | the lowered CTE's working table |
| node_attribute | its vertex column |
| member_rel | the joined member relation (must be untracked) |
| member_attribute | the member relation's join column |
| group_attribute | the member relation's grouping column |
| edge_rel | the tracked edge relation (as for eval_reachability) |
| source_attribute | name of the source-vertex column |
| destination_attribute | name of the destination-vertex column |
| source_value | the base arm's constant, as TEXT |
| directed | if false, each edge can be traversed both ways |
| edge_quals | optional deterministic filter over edge columns |
| source_rel | source relation of a multi-source base arm |
| source_rel_attribute | the source relation's vertex column |
| edge_sql | deparsed edge subquery (join-defined edges) |
| member_quals | optional deterministic filter over the member relation's columns (table-qualified as t.column), restricting which members participate in each group |
| VOID provsql.plant_reach_cover | ( | TEXT | work_name, |
| TEXT | node_attribute, | ||
| REGCLASS | edge_rel, | ||
| TEXT | source_attribute, | ||
| TEXT | destination_attribute, | ||
| TEXT | source_value, | ||
| BOOLEAN | directed, | ||
| TEXT[] | node_values, | ||
| TEXT | edge_quals = NULL, | ||
| REGCLASS | source_rel = NULL, | ||
| TEXT | source_rel_attribute = NULL, | ||
| TEXT | edge_sql = NULL ) |
Plant the certified all-members-reachable gate for a reachability self-join conjunction (internal).
Called (at plan time, over SPI) by the recursive-CTE lowering when the outer query self-joins a reachability working table with one constant node binding per reference – "are these k vertices all
reachable" – whose row provenance provenance_times() computes as the product of correlated per-vertex reach tokens (they share edges). This pre-creates, at the times-canonical address of that token multiset, a certified single-child times over the native all-members-reachable circuit (reachability_materialize_cover), so the natural conjunction stays on the linear certified route – with the joint-worlds semantics: probability evaluation gives the k-terminal reliability, and nonnegative min-plus the cost of the cheapest covering subgraph (directed Steiner cost), shared edges paid once where the raw product would pay them once per factor. Best-effort: any failure leaves the generic path untouched (notice under verbosity 10).
| work_name | the lowered CTE's working table |
| node_attribute | its vertex column |
| edge_rel | the tracked edge relation (as for eval_reachability) |
| source_attribute | name of the source-vertex column |
| destination_attribute | name of the destination-vertex column |
| source_value | the base arm's constant, as TEXT |
| directed | if false, each edge can be traversed both ways |
| node_values | the constant node bindings, as TEXT (multiset: one per self-join reference) |
| edge_quals | optional deterministic filter over edge columns |
| source_rel | source relation of a multi-source base arm |
| source_rel_attribute | the source relation's vertex column |
| edge_sql | deparsed edge subquery (join-defined edges) |
| DOUBLE PRECISION provsql.probability | ( | BOOLEAN | predicate, |
| TEXT | method = NULL, | ||
| TEXT | arguments = NULL ) |
Probability of a Boolean event over random variables.
The (BOOLEAN) overload of probability lets a query ask for the probability of an event with the natural infix grammar, e.g. probability(x > y AND x < z). When the argument carries a probabilistic (random_variable / aggregate) comparison, the planner hook intercepts the call and rewrites it into probability_evaluate over the argument's event token (a gate_cmp / Boolean combination); the body below is then never reached.
When the argument is a purely deterministic Boolean (no probabilistic comparison) the hook leaves the call alone and the body runs, so the probability of a definite event is simply 1 when it holds and 0 when it does not (NULL propagates). This makes probability total over Booleans – probability(1 > 0) is 1, probability(region = 'north') is a per-row 0/1 – and it works even with provsql.active off. NOT strict so a default-NULL method does not short-circuit the cast.
The predicate surface deliberately lives only on the short probability name, not on probability_evaluate: a Boolean overload of the latter would make probability_evaluate('<UUID-as-TEXT>') ambiguous (an unknown literal matches both the UUID and the BOOLEAN overload), breaking existing string-literal callers. probability is new, so it carries the predicate overload without that hazard.
| DOUBLE PRECISION provsql.probability | ( | UUID | token, |
| TEXT | method = NULL, | ||
| TEXT | arguments = NULL ) |
Short alias of probability_evaluate.
Bound to the same C symbol as probability_evaluate, so probability(token) is exactly probability_evaluate(token). Provided to match the concise polymorphic surface of expected, variance, and support: callers are not forced to spell out probability_evaluate.
| token | provenance token to evaluate |
| method | knowledge compilation method (NULL for default) |
| arguments | additional arguments for the method |
| VOID provsql.probability_bounds | ( | UUID | token, |
| OUT DOUBLE PRECISION | lower, | ||
| OUT DOUBLE PRECISION | upper ) |
Cheap certified probability interval of a DNF-shaped circuit.
Returns [lower,upper] with lower <= probability_evaluate(token) <= upper, computed without compiling the circuit (the Olteanu-Huang d-tree leaf bound). Errors when token is not a monotone DNF over input leaves.
| DOUBLE PRECISION provsql.probability_evaluate | ( | UUID | token, |
| TEXT | method = NULL, | ||
| TEXT | arguments = NULL ) |
Compute the probability of a provenance token.
Compiles the provenance circuit to d-DNNF and evaluates the probability. The compilation method can be selected explicitly.
probability is a shorter alias bound to the same C symbol, so probability(token) is exactly probability_evaluate(token); it is usually preferable, and additionally carries a (BOOLEAN) predicate overload (e.g. probability(x > y)).
| token | provenance token to evaluate |
| method | knowledge compilation method (NULL for default) |
| arguments | additional arguments for the method |
| DOUBLE PRECISION provsql.quantile | ( | ANYELEMENT | input, |
| DOUBLE PRECISION | p, | ||
| UUID | prov = gate_one(), | ||
| TEXT | method = NULL, | ||
| TEXT | arguments = NULL ) |
Compute the p-quantile (inverse CDF) of a probabilistic scalar.
\(F^{-1}(p) = \min\{x : P(X \le x) \ge p\}\) for \(p \in [0,1]\): medians (p = 0.5), percentiles, Value-at-Risk, and credible intervals. p = 0 / p = 1 return the (possibly infinite) support edges. Polymorphic dispatcher mirroring expected / moment: random_variable routes through rv_quantile (analytical inverse CDF / MC), plain numerics are their own quantile (a Dirac's inverse CDF is constant), and the optional prov argument conditions on a provenance event, e.g. quantile(x | (x > 0), 0.5) for the median of a truncated distribution.
| VOID provsql.reachability_compile_stats | ( | INT[] | sources, |
| INT[] | destinations, | ||
| UUID[] | tokens, | ||
| DOUBLE_PRECISION[] | probabilities, | ||
| INT | source, | ||
| INT | target, | ||
| BOOLEAN | directed, | ||
| OUT DOUBLE PRECISION | probability, | ||
| OUT INT | data_treewidth, | ||
| OUT BIGINT | nb_bags, | ||
| OUT BIGINT | max_states, | ||
| OUT BIGINT | nb_gates, | ||
| OUT BIGINT | nb_variables ) |
Reachability probability plus compilation statistics (columnar form).
Same compilation as reachability_evaluate(), returning the probability together with the structural statistics that substantiate the bounded-treewidth guarantee: the treewidth of the min-fill decomposition of the data graph, its number of bags, the maximum number of dynamic-programming states at any decomposition node, and the size of the emitted d-DNNF (linear in the number of edges for fixed data treewidth).
| sources | source vertex of each edge (dense INTEGER IDs) | |
| destinations | destination vertex of each edge | |
| tokens | provenance token of each edge tuple | |
| probabilities | probability of each edge tuple | |
| source | the vertex reachability starts from | |
| target | the vertex whose reachability is evaluated | |
| directed | if false, each edge can be traversed both ways | |
| [out] | probability | the reachability probability |
| [out] | data_treewidth | treewidth of the min-fill decomposition of the data graph |
| [out] | nb_bags | number of bags in the decomposition |
| [out] | max_states | maximum number of dynamic-programming states at any decomposition node |
| [out] | nb_gates | number of gates in the emitted d-DNNF |
| [out] | nb_variables | number of variables in the emitted d-DNNF |
| DOUBLE PRECISION provsql.reachability_evaluate | ( | INT[] | sources, |
| INT[] | destinations, | ||
| UUID[] | tokens, | ||
| DOUBLE_PRECISION[] | probabilities, | ||
| INT | source, | ||
| INT | target, | ||
| BOOLEAN | directed ) |
Exact reachability probability over bounded-treewidth data (columnar form).
Computes the probability that target is reachable from source in the probabilistic graph given by the parallel edge arrays (two-terminal network reliability). Unlike probability_evaluate(), which compiles the provenance circuit built along the relational query plan, this compiles the query along a tree decomposition of the data graph (in the spirit of the provenance refinement of Courcelle's theorem), producing a d-DNNF whose size is linear in the number of edges for data of bounded treewidth. Exact, and linear-time, on cyclic data as well – where the recursive-query fixpoint cannot terminate structurally.
Edges are independent events. Two array positions may share a token only if they are mutual reverses (the natural encoding of an undirected edge in a directed edge relation); they are then treated as a single bidirectional edge. This is an internal/testing surface: the user-facing route is a plain WITH RECURSIVE reachability query under the 'absorptive' (or 'BOOLEAN') provenance class, which the query rewriter compiles through eval_reachability() / reachability_materialize().
| sources | source vertex of each edge (dense INTEGER IDs) |
| destinations | destination vertex of each edge |
| tokens | provenance token of each edge tuple |
| probabilities | probability of each edge tuple |
| source | the vertex reachability starts from |
| target | the vertex whose reachability is evaluated |
| directed | if false, each edge can be traversed both ways |
| SETOF RECORD provsql.reachability_materialize | ( | INT[] | sources, |
| INT[] | destinations, | ||
| UUID[] | tokens, | ||
| DOUBLE_PRECISION[] | probabilities, | ||
| UUID[] | block_keys, | ||
| INT[] | block_indices, | ||
| INT[] | source_vertices, | ||
| UUID[] | source_tokens, | ||
| DOUBLE_PRECISION[] | source_probabilities, | ||
| BOOLEAN | directed, | ||
| OUT INT | vertex, | ||
| OUT UUID | token ) |
Compile and materialise the reachability provenance of every vertex (columnar form, internal).
All-targets variant of reachability_evaluate(): compiles, along a tree decomposition of the data graph, one certified provenance circuit per vertex reachable from some source in the all-edges-present world, materialises the (shared, linear-size) circuits in the provenance store – plus / times gates carrying the d-DNNF certificate, negated edges as monus(one, edge) – and returns one (vertex, token) row per such vertex. Sources form a possibly probabilistic source set: each source arc is gated by the source tuple's token, the nil UUID marking a certain (always present) source. This is the engine behind the rewriter's recursive-reachability route; the returned tokens are ordinary provenance tokens usable with the whole evaluation surface, wrapped in the 'absorptive' assumption marker (the compiled circuit is the exact Boolean lineage but only the absorptive quotient of the infinite recursive semiring provenance: probability and absorptive semiring evaluations – e.g. nonnegative min-plus – are exact, counting and why-provenance refuse).
| sources | source vertex of each edge (dense INTEGER IDs) | |
| destinations | destination vertex of each edge | |
| tokens | provenance token of each edge tuple | |
| probabilities | probability of each edge tuple | |
| block_keys | per-edge BID key variable (nil UUID = independent tuple; alternatives sharing a key are mutually exclusive, e.g. from repair_key) | |
| block_indices | per-edge outcome index within its block | |
| source_vertices | the source vertices | |
| source_tokens | per-source provenance token (nil UUID = certain) | |
| source_probabilities | per-source probability | |
| directed | if false, each edge can be traversed both ways | |
| [out] | vertex | a vertex reachable from some source |
| [out] | token | the materialised reachability provenance token of vertex |
| SETOF RECORD provsql.reachability_materialize_any | ( | INT[] | sources, |
| INT[] | destinations, | ||
| UUID[] | tokens, | ||
| DOUBLE_PRECISION[] | probabilities, | ||
| UUID[] | block_keys, | ||
| INT[] | block_indices, | ||
| INT[] | source_vertices, | ||
| UUID[] | source_tokens, | ||
| DOUBLE_PRECISION[] | source_probabilities, | ||
| BOOLEAN | directed, | ||
| INT[] | group_ids, | ||
| INT[] | member_vertices, | ||
| OUT INT | group_id, | ||
| OUT UUID | token ) |
Per-group "some member reachable" compilation (columnar form, internal).
For each distinct group in the parallel group_ids / member_vertices arrays, compiles the certified circuit of "some
member vertex is reachable from a present source" along the data decomposition – the disjunction over the group's correlated per-vertex reachability events, deterministic by construction through the set-reachability state bit – materialises it, and returns one (group_id, token) row per group. Engine behind the rewriter's cross-vertex aggregation planting.
| sources | source vertex of each edge (dense INTEGER IDs) | |
| destinations | destination vertex of each edge | |
| tokens | provenance token of each edge tuple | |
| probabilities | probability of each edge tuple | |
| block_keys | per-edge BID key variable (nil UUID = independent) | |
| block_indices | per-edge outcome index within its block | |
| source_vertices | the source vertices | |
| source_tokens | per-source provenance token (nil UUID = certain) | |
| source_probabilities | per-source probability | |
| directed | if false, each edge can be traversed both ways | |
| group_ids | group identifier of each member row | |
| member_vertices | member vertex of each member row | |
| [out] | group_id | a group whose every member is reachable |
| [out] | token | the materialised all-members-reachable provenance token of group_id |
| UUID provsql.reachability_materialize_cover | ( | INT[] | sources, |
| INT[] | destinations, | ||
| UUID[] | tokens, | ||
| DOUBLE_PRECISION[] | probabilities, | ||
| UUID[] | block_keys, | ||
| INT[] | block_indices, | ||
| INT[] | source_vertices, | ||
| UUID[] | source_tokens, | ||
| DOUBLE_PRECISION[] | source_probabilities, | ||
| BOOLEAN | directed, | ||
| INT[] | member_vertices ) |
Compile and materialise the "every member vertex reachable" (k-terminal / coverage) circuit (columnar form, internal).
Arguments as reachability_materialize_any() with a single member set: compiles the certified circuit of "every member vertex is
reachable from a present source" – the conjunction over the members' correlated per-vertex events, deterministic by construction through the pending rescuer-set congruence – materialises it, and returns its token, wrapped in the 'absorptive' assumption marker. Probability evaluation gives the k-terminal reliability; nonnegative min-plus the cost of the cheapest covering subgraph (directed Steiner cost), shared edges paid once. A member vertex absent from the graph is unreachable: the circuit is then constant false.
| sources | source vertex of each edge (dense INTEGER IDs) |
| destinations | destination vertex of each edge |
| tokens | provenance token of each edge tuple |
| probabilities | probability of each edge tuple |
| block_keys | per-edge BID key variable (nil UUID = independent) |
| block_indices | per-edge outcome index within its block |
| source_vertices | the source vertices |
| source_tokens | per-source provenance token (nil UUID = certain) |
| source_probabilities | per-source probability |
| directed | if false, each edge can be traversed both ways |
| member_vertices | the member vertices (dense IDs) |
| SETOF RECORD provsql.reachability_materialize_hops | ( | INT[] | sources, |
| INT[] | destinations, | ||
| UUID[] | tokens, | ||
| DOUBLE_PRECISION[] | probabilities, | ||
| UUID[] | block_keys, | ||
| INT[] | block_indices, | ||
| INT[] | source_vertices, | ||
| UUID[] | source_tokens, | ||
| DOUBLE_PRECISION[] | source_probabilities, | ||
| BOOLEAN | directed, | ||
| INT | hop_bound, | ||
| INT | hop_seed, | ||
| OUT INT | vertex, | ||
| OUT INT | hops, | ||
| OUT UUID | token ) |
Bounded-hop variant of reachability_materialize() (internal).
Compiles, along a tree decomposition of the data graph, one certified provenance circuit per (vertex, walk length) pair achievable within hop_bound edges – the rows a hop-counting recursive CTE derives, row (v,h) meaning "some *walk* of exactly @c h edges connects a
present source to @c v" – and returns them as (vertex, hops, token) with hop_seed added to the lengths (the CTE base arm's hop constant). Also pre-creates, per vertex, the certified gate that a hop-discarding query's deduplication will address, wired to the compilation's native within-bound root, so the natural "within k
hops" probability evaluates through the linear certified route.
| sources | source vertex of each edge (dense INTEGER IDs) | |
| destinations | destination vertex of each edge | |
| tokens | provenance token of each edge tuple | |
| probabilities | probability of each edge tuple | |
| block_keys | per-edge BID key variable (nil UUID = independent) | |
| block_indices | per-edge outcome index within its block | |
| source_vertices | the source vertices | |
| source_tokens | per-source provenance token (nil UUID = certain) | |
| source_probabilities | per-source probability | |
| directed | if false, each edge can be traversed both ways | |
| hop_bound | maximum walk length | |
| hop_seed | hop value of the base arm (added to reported lengths) | |
| [out] | vertex | a reachable vertex |
| [out] | hops | the walk length at which vertex is reached |
| [out] | token | the materialised provenance token of the |
| DOUBLE PRECISION provsql.rv_correlation | ( | UUID | x, |
| UUID | y, | ||
| UUID | prov ) |
C entry point behind correlation (UUID-level binding).
| DOUBLE PRECISION provsql.rv_covariance | ( | UUID | x, |
| UUID | y, | ||
| UUID | prov ) |
C entry point behind covariance (UUID-level binding).
| DOUBLE PRECISION provsql.rv_entropy | ( | UUID | token, |
| UUID | prov ) |
C entry point behind entropy (UUID-level binding).
| DOUBLE PRECISION provsql.rv_kl | ( | UUID | p, |
| UUID | q ) |
C entry point behind kl (UUID-level binding).
| DOUBLE PRECISION provsql.rv_moment | ( | UUID | token, |
| INTEGER | k, | ||
| BOOLEAN | central, | ||
| UUID | prov = gate_one() ) |
Internal: shared C entry point for variance / moment / central_moment.
The expected() SQL function reaches the Expectation evaluator through provenance_evaluate_compiled(..., 'expectation', ...). The variance / raw-moment / central-moment SQL functions need an extra k INTEGER argument that does not fit that dispatcher's signature, so they go through this dedicated entry point. Returns E[X^k] when central is FALSE, or E[(X - E[X])^k] when TRUE.
| DOUBLE PRECISION provsql.rv_mutual_information | ( | UUID | x, |
| UUID | y ) |
C entry point behind mutual_information (UUID-level binding).
| DOUBLE PRECISION provsql.rv_quantile | ( | UUID | token, |
| DOUBLE PRECISION | p, | ||
| UUID | prov = gate_one() ) |
Internal: rv-side quantile computation.
C entry point behind the polymorphic quantile dispatcher. Closed-form inverse CDF where the family has one (Normal via Beasley-Springer-Moro polished by Newton steps, Uniform and Exponential by algebraic inversion), generic monotone-CDF bisection otherwise (Erlang, Gamma), exact generalised inverse for categorical mixtures, and the empirical Monte Carlo quantile for compound scalar circuits. A non-trivial prov conditions (truncates) the distribution first, in closed form when the event reduces to an interval on a bare gate_rv.
| VOID provsql.rv_support | ( | UUID | token, |
| UUID | prov = gate_one(), | ||
| float8 & | lo, | ||
| float8 & | hi ) |
Internal: rv-side support computation.
Lifts provsql.compute_support out of RangeCheck.cpp – the same interval-arithmetic propagation runRangeCheck uses to decide gate_cmps. Returns [-Infinity, +Infinity] when the tightest bound is the conservative all-real interval (e.g. for a normal RV, or any sub-circuit that mixes a normal in).
| DOUBLE PRECISION provsql.shapley | ( | UUID | token, |
| UUID | variable, | ||
| TEXT | method = NULL, | ||
| TEXT | arguments = NULL, | ||
| BOOLEAN | banzhaf = 'f' ) |
Compute the Shapley value of an input variable.
Measures the contribution of a specific input variable to the truth of a provenance expression, using game-theoretic Shapley values.
| token | provenance token to evaluate |
| variable | UUID of the input variable |
| method | knowledge compilation method |
| arguments | additional arguments for the method |
| banzhaf | if true, compute the Banzhaf value instead |
| SETOF RECORD provsql.shapley_all_vars | ( | UUID | token, |
| TEXT | method = NULL, | ||
| TEXT | arguments = NULL, | ||
| BOOLEAN | banzhaf = 'f', | ||
| OUT UUID | variable, | ||
| OUT DOUBLE PRECISION | value ) |
Compute Shapley values for all input variables at once.
| DOUBLE PRECISION provsql.stddev | ( | random_variable | x, |
| UUID | prov = gate_one() ) |
Standard deviation σ(X) = √Var(X) of a random variable.
A thin NUMERIC readout over variance. The square root is taken on the scalar double result, so no RV-level sqrt is involved and this carries no dependency on RV function application (pow / sqrt). NULL propagates from a NULL input; the order-2 central moment is non-negative by construction, so the root is always real.
| x | the random variable. |
| prov | optional conditioning event; default gate_one() (unconditional). |
| VOID provsql.support | ( | ANYELEMENT | input, |
| UUID | prov = gate_one(), | ||
| TEXT | method = NULL, | ||
| TEXT | arguments = NULL, | ||
| float8 & | lo, | ||
| float8 & | hi ) |
Compute the support interval [lo, hi] of a probabilistic (or deterministic) scalar.
Polymorphic dispatcher mirroring expected / variance / moment / central_moment, with two extra "free" branches:
smallint / INTEGER / bigint / NUMERIC / real / double precision): degenerate point support \([c, c]\). Lets callers ask for the support of a literal without round-tripping through as_random.random_variable / bare UUID (any provenance gate token; the random_variable branch reinterprets the value via the binary-coercible random_variable -> UUID cast): routes to rv_support, which propagates distribution supports (uniform exact, exponential gate_arith via interval arithmetic. gate_value gives the same \([c, c]\) point support as the NUMERIC branch; any non-scalar gate (Boolean gates, aggregates, ...) safely falls back to the conservative all-real interval without raising. Conditioning on prov is not yet supported.AGG_TOKEN: closed-form per aggregation function:SUM : \([\sum_i \min(0,v_i), \sum_i \max(0,v_i)]\) (every row is independently in or out of the included set; the extreme SUMs are reached by including only positive or only negative-valued rows).MIN : \([\min_i v_i, \max_i v_i]\) in the non-empty subsets, plus +Infinity if the empty subset has positive probability under prov.MAX : symmetric – -Infinity if empty has positive probability under prov, otherwise min_i v_i; hi is always max_i v_i.Other aggregation functions raise.
Returns the composite RECORD (lo, hi) via the function's OUT parameters, with -Infinity / +Infinity marking unbounded ends.
| UUID[] provsql.token_conjunctive_leaves | ( | UUID | token | ) |
Input leaves of a conjunction-shaped provenance token (internal).
Descends a token's circuit through the conjunctive gate types (times, and the pass-through project / eq where-provenance wrappers) down to input leaves. Returns the distinct leaves, or NULL when the circuit contains any other gate type (a disjunctive or aggregate shape, which is not a conjunction of independent tuples). Used by the reachability gathering to accept join-defined edges: a derived edge whose token is a pure conjunction of base tuples.
| token | the provenance token |
| VOID provsql.ucq_joint_compile_stats | ( | INT[] | disjunct_nvars, |
| INT[] | atom_disjunct, | ||
| INT[] | atom_rel, | ||
| INT[] | atom_vars, | ||
| INT[] | atom_arity, | ||
| INT[] | fact_rel, | ||
| INT[] | fact_elems, | ||
| INT[] | fact_arity, | ||
| UUID[] | fact_tokens, | ||
| DOUBLE_PRECISION[] | fact_probs, | ||
| OUT DOUBLE PRECISION | probability, | ||
| OUT INT | joint_treewidth, | ||
| OUT INT | data_treewidth_lb, | ||
| OUT INT | circuit_treewidth_lb, | ||
| OUT BIGINT | n_bags, | ||
| OUT BIGINT | max_states, | ||
| OUT BIGINT | dd_size, | ||
| OUT INT | n_enumerating ) |
Boolean UCQ probability plus compilation statistics (columnar form, internal).
Same compilation as ucq_joint_compile_stats(query jsonb, ...), returning the probability together with the three width columns that substantiate thesis Prop. 4.2.11 empirically – the adversarial family has small data and circuit widths but large joint width – and the structural statistics.
| disjunct_nvars | number of query variables of each disjunct | |
| atom_disjunct | disjunct index of each atom (parallel to atom_rel) | |
| atom_rel | relation id of each atom | |
| atom_vars | query-variable indices of all atom columns, concatenated | |
| atom_arity | number of columns of each atom (slices atom_vars) | |
| fact_rel | relation id of each fact | |
| fact_elems | element ids of all fact columns, concatenated | |
| fact_arity | number of columns of each fact (slices fact_elems) | |
| fact_tokens | provenance token of each fact | |
| fact_probs | probability of each fact | |
| [out] | probability | the exact UCQ probability |
| [out] | joint_treewidth | width of the min-fill decomposition found |
| [out] | data_treewidth_lb | degeneracy lower bound of the data-only graph |
| [out] | circuit_treewidth_lb | degeneracy lower bound of the slice-only graph |
| [out] | n_bags | number of bags in the decomposition |
| [out] | max_states | peak number of DP states at any node |
| [out] | dd_size | number of gates in the emitted d-D |
| [out] | n_enumerating | maximum number of essential (enumerating) query variables over the disjuncts – the e of the \(2^{O(k^e)}\) bound, with variables functionally determined by others (via FDs mined from the data) removed |
| VOID provsql.ucq_joint_compile_stats | ( | JSONB | query, |
| INT[] | fact_rel, | ||
| INT[] | fact_elems, | ||
| INT[] | fact_arity, | ||
| UUID[] | fact_tokens, | ||
| DOUBLE_PRECISION[] | fact_probs, | ||
| OUT DOUBLE PRECISION | probability, | ||
| OUT INT | joint_treewidth, | ||
| OUT INT | data_treewidth_lb, | ||
| OUT INT | circuit_treewidth_lb, | ||
| OUT BIGINT | n_bags, | ||
| OUT BIGINT | max_states, | ||
| OUT BIGINT | dd_size, | ||
| OUT INT | n_enumerating ) |
Boolean UCQ probability plus statistics from a JSON specification.
JSON-spec wrapper over the columnar ucq_joint_compile_stats() (see ucq_joint_evaluate(query jsonb, ...) for the JSON format).
| VOID provsql.ucq_joint_compile_stats_tracked | ( | INT[] | disjunct_nvars, |
| INT[] | atom_disjunct, | ||
| INT[] | atom_rel, | ||
| INT[] | atom_vars, | ||
| INT[] | atom_arity, | ||
| INT[] | fact_rel, | ||
| INT[] | fact_elems, | ||
| INT[] | fact_arity, | ||
| UUID[] | fact_tokens, | ||
| OUT DOUBLE PRECISION | probability, | ||
| OUT INT | joint_treewidth, | ||
| OUT INT | data_treewidth_lb, | ||
| OUT INT | circuit_treewidth_lb, | ||
| OUT BIGINT | n_bags, | ||
| OUT BIGINT | max_states, | ||
| OUT BIGINT | dd_size, | ||
| OUT INT | n_enumerating ) |
Correlated Boolean UCQ probability plus compilation statistics (columnar form, internal).
Same compilation as ucq_joint_evaluate_tracked(); the three width columns substantiate thesis Prop. 4.2.11 on real correlated data (the data-only and circuit-only degeneracy bounds can be small while the joint width is large).
| VOID provsql.ucq_joint_compile_stats_tracked | ( | JSONB | query, |
| INT[] | fact_rel, | ||
| INT[] | fact_elems, | ||
| INT[] | fact_arity, | ||
| UUID[] | fact_tokens, | ||
| OUT DOUBLE PRECISION | probability, | ||
| OUT INT | joint_treewidth, | ||
| OUT INT | data_treewidth_lb, | ||
| OUT INT | circuit_treewidth_lb, | ||
| OUT BIGINT | n_bags, | ||
| OUT BIGINT | max_states, | ||
| OUT BIGINT | dd_size, | ||
| OUT INT | n_enumerating ) |
Correlated Boolean UCQ probability plus statistics from a JSON spec.
| VOID provsql.ucq_joint_gather | ( | JSONB | descriptor, |
| INT[] & | disjunct_nvars, | ||
| INT[] & | atom_disjunct, | ||
| INT[] & | atom_rel, | ||
| INT[] & | atom_vars, | ||
| INT[] & | atom_arity, | ||
| INT[] & | fact_rel, | ||
| INT[] & | fact_elems, | ||
| INT[] & | fact_arity, | ||
| UUID[] & | fact_tokens, | ||
| TEXT[] & | val_by_id ) |
Internal gather for the per-answer joint route: parse descriptor into the columnar UCQ arrays and gather every fact (relation index, dense element ids, provenance token) with the value dictionary.
Used only by the planner-substituted ucq_joint_provenance_answer (the C single-DP entry point), which calls it ONCE per query and then computes all answers in one sweep. No head pinning: the single DP discovers the answers. val_by_id maps a dense element id back to its TEXT value (so an answer's head ids can be matched to the GROUP BY head TEXT).
| UUID provsql.ucq_joint_materialize_tracked | ( | INT[] | disjunct_nvars, |
| INT[] | atom_disjunct, | ||
| INT[] | atom_rel, | ||
| INT[] | atom_vars, | ||
| INT[] | atom_arity, | ||
| INT[] | fact_rel, | ||
| INT[] | fact_elems, | ||
| INT[] | fact_arity, | ||
| UUID[] | fact_tokens ) |
Compile a correlated UCQ and materialise its certified d-D, returning the root provenance token (columnar form, internal).
The architecturally-primary route: the compiler builds the deterministic, decomposable circuit and materialises it as ordinary plus / times / monus provenance gates (carrying the d-DNNF certificate); the answer is then obtained through the standard entry points on the returned token – probability_evaluate(token), shapley(token, ...), expectation – so the joint-width path shares the one evaluation pipeline. The token is the exact Boolean provenance of the UCQ (no 'absorptive' marker).
| UUID provsql.ucq_joint_materialize_tracked | ( | JSONB | query, |
| INT[] | fact_rel, | ||
| INT[] | fact_elems, | ||
| INT[] | fact_arity, | ||
| UUID[] | fact_tokens ) |
Compile a correlated UCQ and materialise its certified d-D from a JSON spec, returning the root provenance token.
JSON-spec wrapper over ucq_joint_materialize_tracked(). Evaluate the answer with the standard surface, e.g. probability_evaluate(ucq_joint_materialize_tracked(query, ...)).
| UUID provsql.ucq_joint_provenance | ( | JSONB | descriptor, |
| UUID | fallback = NULL ) |
Compile a UCQ over named relations into a materialised certified d-D, gathering the facts from the store – the descriptor-driven engine.
The query-surface bridge for the joint-width compiler: instead of hand-built columnar arrays, a JSON descriptor names the relations and how their columns map to query variables, and this function gathers the facts itself (the provenance rewriting is disabled around the gather), builds the value-based element dictionary shared across the relations (so equal join values get the same dense id), compiles and materialises the certified d-D, and returns its provenance token. The answer is then any standard evaluation on that token – probability_evaluate(ucq_joint_provenance(...)), shapley(...), expectation. This is also the engine the planner-time query recogniser drives once it builds the descriptor from a query's abstract syntax.
Descriptor shape:
* { "disjuncts": [ { "n_vars": k,
* "atoms": [ {"rel": <relidx>, "vars": [..]}, ... ] }, ... ],
* "relations": [ "schema.r", "schema.s", ... ], -- relidx -> relation
* "elem_cols": [ ["x"], ["x","y"], ... ] } -- per relation: the
* element columns, in
* the atom's var order
* | descriptor | the UCQ + the relations and their element columns |
| fallback | token returned if the joint-width compiler declines |
| UUID provsql.ucq_joint_provenance_answer | ( | JSONB | descriptor, |
| INT[] | head_vars, | ||
| TEXT[] | head_vals, | ||
| UUID | fallback = NULL ) |
Per-answer joint-width provenance via the TOP-DOWN single DP (planner-substituted, C).
The transparent per-answer rewrite substitutes one call per output group. On the FIRST call of a query the function gathers the facts once (ucq_joint_gather), runs the single DP, and materialises EVERY answer's certified d-D into the store, caching head_vals -> token in fn_extra; each subsequent group call is an O(1) lookup – so the whole GROUP BY costs one gather + one decomposition + one sweep, not k of each. On any decline (joint width too large) the fallback token (the normal per-answer provenance) is returned, so the query never fails. The answer's marginal / Shapley / expectation is then the standard evaluation on the returned token – one pipeline for the whole system.
| VOID provsql.ucq_mobius_compile_stats | ( | INT[] | disjunct_nvars, |
| INT[] | atom_disjunct, | ||
| INT[] | atom_rel, | ||
| INT[] | atom_vars, | ||
| INT[] | atom_arity, | ||
| INT[] | fact_rel, | ||
| INT[] | fact_elems, | ||
| INT[] | fact_arity, | ||
| UUID[] | fact_tokens, | ||
| OUT DOUBLE PRECISION | probability, | ||
| OUT INT | n_components, | ||
| OUT INT | n_cnf_conjuncts, | ||
| OUT INT | lattice_size, | ||
| OUT INT | n_nonzero, | ||
| OUT INT | n_cancelled, | ||
| OUT BOOLEAN | cancelled_hard, | ||
| OUT BIGINT | dd_size, | ||
| OUT BIGINT | memo_hits ) |
Compile the Möbius circuit and return the lattice statistics plus the probability (the demonstrability surface).
cancelled_hard is the single number that makes the mechanism legible: for q9 the 1 cancelled element is #P-hard, so the query is easy only because its hard part cancels.
| UUID provsql.ucq_mobius_materialize_tracked | ( | INT[] | disjunct_nvars, |
| INT[] | atom_disjunct, | ||
| INT[] | atom_rel, | ||
| INT[] | atom_vars, | ||
| INT[] | atom_arity, | ||
| INT[] | fact_rel, | ||
| INT[] | fact_elems, | ||
| INT[] | fact_arity, | ||
| UUID[] | fact_tokens, | ||
| UUID | lineage = NULL ) |
=========================================================================== Safe-UCQ Möbius-inversion route (mobius_evaluate.cpp).
The last missing exact route of the Dalvi-Suciu dichotomy: UCQs that are safe only because the #P-hard terms of their inclusion-exclusion expansion carry a zero Möbius value on the CNF lattice and cancel (canonical witness: QW / q9). Same TID gather as ucq_joint, then the lattice-walking compiler materialises a gate_mobius-rooted circuit (a signed combination over certified-independent islands), answered in PTIME data complexity by the
Materialise the safe-UCQ Möbius circuit and return its root token. Columnar (TID) interface; see ucq_mobius_provenance for the gather.
| UUID provsql.ucq_mobius_provenance | ( | JSONB | descriptor, |
| UUID | fallback = NULL ) |
Möbius-route provenance from a descriptor (the planner-substituted entry point, and the manual one).
Same descriptor and TID gather as ucq_joint_provenance; on any decline (unsafe shape, cap, not TID) returns fallback, so a recognised query never fails.
| UUID provsql.ucq_mobius_provenance_answer | ( | JSONB | descriptor, |
| INT[] | head_vars, | ||
| TEXT[] | head_vals, | ||
| UUID | fallback = NULL ) |
Per-answer safe-UCQ Möbius provenance (planner-substituted): one head-pinned Möbius circuit per output group.
On the first call the facts are gathered once (ucq_joint_gather) and cached; each group pins head_vars to head_vals and compiles, caching head -> token. On any decline returns fallback. STABLE: it caches per fn-call context, so it is not re-evaluated within one scan.
| DOUBLE PRECISION provsql.variance | ( | ANYELEMENT | input, |
| UUID | prov = gate_one(), | ||
| TEXT | method = NULL, | ||
| TEXT | arguments = NULL ) |
Compute the variance Var[X | prov] of a probabilistic scalar.
Polymorphic dispatcher that mirrors expected: random_variable inputs go through the analytical / MC evaluator (rv_moment(UUID, 2, true)); AGG_TOKEN inputs go through the agg_raw_moment helper, computing \(\mathrm{Var}[X|A] = E[X^2|A] - E[X|A]^2\). Conditioning on prov is supported for AGG_TOKEN (matching expected) but not yet for random_variable.