 |
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
|
Create a δ-semiring gate wrapping a provenance token. More...
Topics | |
| Provenance output | |
| Compute the probability of a provenance token. | |
Functions | |
| DOUBLE PRECISION | probability_evaluate (UUID token, TEXT method=NULL, TEXT arguments=NULL) |
| Compute the probability of a provenance token. | |
| VOID | probability_bounds (UUID token, OUT DOUBLE PRECISION lower, OUT DOUBLE PRECISION upper) |
| Cheap certified probability interval of a DNF-shaped circuit. | |
| DOUBLE PRECISION | expected (ANYELEMENT input, UUID prov=gate_one(), TEXT method=NULL, TEXT arguments=NULL) |
| Compute the expected value of a probabilistic scalar. | |
| DOUBLE PRECISION | rv_moment (UUID token, INTEGER k, BOOLEAN central, UUID prov=gate_one()) |
| Internal: shared C entry point for variance / moment / central_moment. | |
| DOUBLE PRECISION | 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 | 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 | 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. | |
| VOID | rv_support (UUID token, UUID prov=gate_one(), float8 &lo, float8 &hi) |
| Internal: rv-side support computation. | |
| VOID | support (ANYELEMENT input, UUID prov=gate_one(), TEXT method=NULL, TEXT arguments=NULL, float8 &lo, float8 &hi) |
Compute the support interval | |
| DOUBLE PRECISION | 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 | shapley (UUID token, UUID variable, TEXT method=NULL, TEXT arguments=NULL, BOOLEAN banzhaf='f') |
| Compute the Shapley value of an input variable. | |
| SETOF RECORD | 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 | banzhaf (UUID token, UUID variable, TEXT method=NULL, TEXT arguments=NULL) |
| Compute the Banzhaf power index of an input variable. | |
| SETOF RECORD | 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 | 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 | 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). | |
| VOID | 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). | |
| VOID | 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. | |
| VOID | 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). | |
| VOID | 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. | |
| UUID | 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 | 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 | 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 | 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 | 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). | |
| UUID | mobius_or_null (UUID tok) |
Pass a token through iff it is a gate_mobius, else return NULL. | |
| UUID | 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 | 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. | |
| VOID | 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 | 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 | 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 | 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 | 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 | 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 | 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 | 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 | 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[] | token_conjunctive_leaves (UUID token) |
| Input leaves of a conjunction-shaped provenance token (internal). | |
| VOID | 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 | 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 | 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. | |
Create a δ-semiring gate wrapping a provenance token.
Functions for computing probabilities, expected values, and game-theoretic contribution measures (Shapley/Banzhaf values) from provenance circuits.
Used internally for aggregate provenance. Returns the token unchanged if it is gate_zero() or gate_one(), and gate_one() if the token is NULL.
Build an aggregate provenance gate from grouped tokens
Called internally by the query rewriter for GROUP BY queries. Creates an agg gate linking all contributing tokens and records the aggregate function OID and the computed scalar value.
| aggfnoid | OID of the SQL aggregate function |
| aggtype | OID of the aggregate result type |
| val | computed aggregate value |
| tokens | array of provenance tokens being aggregated |
| is_scalar | true for a scalar (no GROUP BY) aggregation, whose output row exists even when no tuple is present; stored in the high bit of info2 |
Create a semimodule scalar multiplication gate
Pairs a scalar value with a provenance token, used internally by the query rewriter for aggregate provenance.
| val | the scalar value |
| token | the provenance token to multiply |
Functions for computing probabilities, expected values, and game-theoretic contribution measures (Shapley/Banzhaf values) from provenance circuits.
| DOUBLE PRECISION update_provenance::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, and MAX.
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 update_provenance::banzhaf | ( | UUID | token, |
| UUID | variable, | ||
| TEXT | method = NULL, | ||
| TEXT | arguments = NULL ) |
Compute the Banzhaf power index of an input variable.
| SETOF RECORD update_provenance::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 update_provenance::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.
| VOID update_provenance::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 update_provenance::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 update_provenance::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 update_provenance::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 |
| RECORD update_provenance::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 update_provenance::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 update_provenance::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).
| VOID update_provenance::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 update_provenance::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) |
| VOID update_provenance::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 update_provenance::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.
| token | provenance token to evaluate |
| method | knowledge compilation method (NULL for default) |
| arguments | additional arguments for the method |
| VOID update_provenance::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 and Shapley values | 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 update_provenance::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 update_provenance::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 update_provenance::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 update_provenance::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 update_provenance::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 update_provenance::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.
| VOID update_provenance::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 update_provenance::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 update_provenance::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.
| VOID update_provenance::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[] update_provenance::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 update_provenance::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 and Shapley values | 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 update_provenance::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 update_provenance::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 update_provenance::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 update_provenance::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 update_provenance::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 update_provenance::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 update_provenance::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 update_provenance::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 update_provenance::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 update_provenance::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 update_provenance::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 update_provenance::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 update_provenance::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.