 |
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 that build provenance circuit gates for semiring operations. More...
Functions | |
| UUID | provsql.provenance_times (UUID[] tokens) |
| Create a times (product) gate from multiple provenance tokens. | |
| UUID | provsql.provenance_monus (UUID token1, UUID token2) |
| Create a monus (difference) gate from two provenance tokens. | |
| UUID | provsql.provenance_project (UUID token, INT[] positions) |
| Create a project gate for where-provenance tracking. | |
| UUID | provsql.provenance_eq (UUID token, INT pos1, INT pos2) |
| Create an equijoin gate for where-provenance tracking. | |
| UUID | provsql.provenance_plus (UUID[] tokens) |
| Create a plus (sum) gate from an array of provenance tokens. | |
| VOID | provsql.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 | provsql.provenance_cmp (UUID left_token, OID comparison_op, UUID right_token) |
| Create a comparison gate for HAVING clause provenance. | |
| UUID[] | provsql.cmp_surviving_factors (UUID[] tokens, UUID cmp) |
| The factors of a row annotation an aggregate comparison does not subsume. | |
| UUID | provsql.provenance_cmp_times (UUID cmp, UUID[] tokens) |
| Combine a lifted aggregate comparison with the row annotation it supersedes only part of. | |
| UUID | provsql.provenance_arith (INTEGER op, UUID[] children) |
| Create an arithmetic gate over scalar-valued provenance children. | |
| UUID | provsql.provenance_case (UUID[] children) |
| Create a guarded-selection gate over scalar (RV) children. | |
Functions that build provenance circuit gates for semiring operations.
These are called internally by the query rewriter.
They are declared IMMUTABLE: each derives its gate UUID deterministically from its arguments (a uuid5 content address) and the create_gate write at that address is idempotent, so the token a call returns is a pure function of its inputs. The marking matters for parallelism: PL/pgSQL runs a non-volatile function's inner SPI read-only, so the per-row builders the rewriter injects into a scan do not call CommandCounterIncrement – which would raise "cannot start
commands during a parallel operation" once the enclosing statement has gone parallel. A VOLATILE builder both blocks that parallel plan and loses the query-wide speed-up.
| UUID[] provsql.cmp_surviving_factors | ( | UUID[] | tokens, |
| UUID | cmp ) |
The factors of a row annotation an aggregate comparison does not subsume.
A lifted comparison entails the existence of the group it ranges over, so it supersedes that group's gate_delta instead of multiplying with it. This reports which factors of tokens survive that supersede: a bare δ over the compared group disappears, a times keeps its other factors, and anything else – an earlier comparison on the same group, an input – is kept whole.
| VOID provsql.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 provsql.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 provsql.provenance_case | ( | UUID[] | children | ) |
Create a guarded-selection gate over scalar (RV) children.
Builds a deterministic gate_case from the flattened wire list [guard_1, value_1, ..., guard_k, value_k, default] (odd length): the value of the first guard event that holds, else the default (first-match semantics). Each guard is a Boolean event token (a gate_cmp or Boolean combination); each value and the default are scalar-producing gates (gate_rv, gate_value, gate_arith, another gate_case, ...). The token UUID is derived deterministically from children so identical CASE expressions share their gate.
| children | Flattened guard/value wires ending with the default (array_length must be odd and >= 1). |
gate_case. | UUID provsql.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 provsql.provenance_cmp_times | ( | UUID | cmp, |
| UUID[] | tokens ) |
Combine a lifted aggregate comparison with the row annotation it supersedes only part of.
| cmp | Gate of the lifted comparison. |
| tokens | Row-annotation factors at the level owning the comparison. |
cmp multiplied with whatever of tokens it does not subsume. | UUID provsql.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 provsql.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 provsql.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 provsql.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 provsql.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.