 |
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
|
Return the ProvSQL UUID namespace (used for deterministic gate UUIDs). More...
Topics | |
| Semiring evaluation | |
| Create a times (product) gate from multiple provenance tokens. | |
Functions | |
| UUID | provenance_times (UUID[] tokens) |
| Create a times (product) gate from multiple provenance tokens. | |
| UUID | provenance_monus (UUID token1, UUID token2) |
| Create a monus (difference) gate from two provenance tokens. | |
| UUID | provenance_project (UUID token, INT[] positions) |
| Create a project gate for where-provenance tracking. | |
| UUID | provenance_eq (UUID token, INT pos1, INT pos2) |
| Create an equijoin gate for where-provenance tracking. | |
| UUID | provenance_plus (UUID[] tokens) |
| Create a plus (sum) gate from an array of provenance tokens. | |
| VOID | eval_recursive (TEXT body_sql, TEXT work_name, TEXT colnames, TEXT coldef, INT max_iter=1000) |
| Driver for provenance over recursive queries (WITH RECURSIVE). | |
| UUID | provenance_cmp (UUID left_token, OID comparison_op, UUID right_token) |
| Create a comparison gate for HAVING clause provenance. | |
| UUID | provenance_arith (INTEGER op, UUID[] children) |
| Create an arithmetic gate over scalar-valued provenance children. | |
Return the ProvSQL UUID namespace (used for deterministic gate UUIDs).
Functions that build provenance circuit gates for semiring operations.
Return the UUID of the semiring zero gate
Return the UUID of the semiring one gate
Return the epsilon threshold used for probability comparisons
Functions that build provenance circuit gates for semiring operations. These are called internally by the query rewriter.
These are called internally by the query rewriter.
| VOID update_provenance::eval_recursive | ( | TEXT | body_sql, |
| TEXT | work_name, | ||
| TEXT | colnames, | ||
| TEXT | coldef, | ||
| INT | max_iter = 1000 ) |
Driver for provenance over recursive queries (WITH RECURSIVE).
Invoked by the planner hook (lower_recursive_cte in provsql.c) when it lowers a recursive CTE whose body touches provenance-tracked relations. The hook deparses the CTE body to SQL and calls this function, which runs naive bottom-up (fixpoint) evaluation: each round re-evaluates the body base UNION recursive over a tracked working table until the provenance tokens stop changing. Every round goes through ProvSQL's normal rewriting, so the recursive join yields times gates, the untracked base branch yields gate_one, and the UNION yields the plus merge of alternative derivations – no provenance is plumbed by hand here. The result is left in a tracked temp table named work_name, which the hook then scans in place of the CTE.
The working tables (work_name and a scratch _new) are created once and reused across rounds (TRUNCATE + INSERT), so the round count never accumulates relation locks. Because content-addressed gate UUIDs make structurally identical sub-circuits share, the fixpoint test is an exact relational EXCEPT and the circuit stays the shared (polynomial) form.
Scope: UNION (set) recursion. On acyclic input the structural fixpoint is reached and the resulting circuit is the universal provenance, sound for any semiring. On cyclic input the circuit never stabilises structurally; when the session's provenance class (provsql.provenance) is 'absorptive' or 'BOOLEAN' we instead stop at the value-fixpoint bound (number of derivable tuples) – every minimal, tuple-repetition-free derivation is then covered, and the longer ones are absorbed in any absorptive semiring (after Deutch, Milo, Roy & Tannen, ICDT 2014) – and wrap the resulting tokens in the 'absorptive' assumption marker, so that non-absorptive semiring evaluations (counting, why-provenance: genuinely infinite on cyclic data) refuse them while probability, Boolean, formula-as-circuit and min-plus evaluations proceed. Under the general classes, cyclic input trips the max_iter guard.
This function has no SET search_path on purpose: body_sql is the caller's deparsed query and must resolve relation names in the caller's path.
| body_sql | the recursive CTE body, e.g. 'SELECT 1 UNION SELECT e.dst FROM edge e JOIN reach r ON e.src=r.node' |
| work_name | the working relation name body_sql references (the CTE name) |
| colnames | comma-separated user columns, e.g. 'node' |
| coldef | column definitions for the working table, e.g. 'node INTEGER' |
| max_iter | safety bound on fixpoint rounds (non-termination guard) |
| UUID update_provenance::provenance_arith | ( | INTEGER | op, |
| UUID[] | children ) |
Create an arithmetic gate over scalar-valued provenance children.
Builds a deterministic gate_arith from an operator tag and an ordered list of children. The tag is one of the provsql_arith_op ENUM values declared in src/provsql_utils.h (PLUS=0, TIMES=1, MINUS=2, DIV=3, NEG=4) and is stored in the gate's info1 field. Children must be UUIDs of scalar-producing gates (gate_rv, gate_value, or another gate_arith). The token UUID is derived deterministically from op and children so identical sub-expressions share their gate.
| op | Operator tag (provsql_arith_op). |
| children | Ordered list of child gate UUIDs. |
gate_arith. | UUID update_provenance::provenance_cmp | ( | UUID | left_token, |
| OID | comparison_op, | ||
| UUID | right_token ) |
Create a comparison gate for HAVING clause provenance.
| left_token | provenance token for the left operand |
| comparison_op | OID of the comparison operator |
| right_token | provenance token for the right operand |
| UUID update_provenance::provenance_eq | ( | UUID | token, |
| INT | pos1, | ||
| INT | pos2 ) |
Create an equijoin gate for where-provenance tracking.
| token | child provenance token |
| pos1 | attribute index in the first relation |
| pos2 | attribute index in the second relation |
| UUID update_provenance::provenance_monus | ( | UUID | token1, |
| UUID | token2 ) |
Create a monus (difference) gate from two provenance tokens.
Implements m-semiring monus. Returns token1 if token2 is NULL (used for LEFT OUTER JOIN semantics in the EXCEPT rewriting).
| UUID update_provenance::provenance_plus | ( | UUID[] | tokens | ) |
Create a plus (sum) gate from an array of provenance tokens.
Filters out NULL and zero-gates; returns gate_zero() if all tokens are trivial, or a single token if only one remains. Before creating a gate, probes the canonical address of the multiset – a dedicated v5 recipe namespace over the sorted tokens (plus is commutative), in which this function never creates anything, so a gate found there is always a deliberate pre-creation computing the same sum. That is the bounded-hop reachability route's hook: it plants, at the canonical address of a vertex's per-length tokens, a certified gate over its native within-bound circuit, keeping the natural hop-discarding query on the linear evaluation route. Absent a canonical gate, the ordinary order-dependent recipe is used, so ordinary plus gates (and their formula rendering) are untouched.
| UUID update_provenance::provenance_project | ( | UUID | token, |
| INT[] | positions ) |
Create a project gate for where-provenance tracking.
Records the mapping between input and output attribute positions.
| token | child provenance token |
| positions | array encoding attribute position mappings |
| UUID update_provenance::provenance_times | ( | UUID[] | tokens | ) |
Create a times (product) gate from multiple provenance tokens.
Filters out NULL and one-gates; returns gate_one() if all tokens are trivial, or a single token if only one remains.
Before creating an ordinary gate, the times-canonical address of the surviving multiset – uuid5('times-canonical{sorted tokens}') – is probed: the reachability rewriter pre-creates there, for self-join conjunctions of reachability tokens, a certified equivalent (the all-members-reachable circuit; see plant_reach_cover). Ordinary creation never writes under that recipe, so a hit is always a deliberate plant; the ordinary order-dependent recipe is used otherwise, so ordinary times gates (and their formula rendering) are untouched.