 |
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.planted_scope (TEXT work_name) |
| Declare the working table of a recursive CTE, just (re)created (internal). | |
| UUID | provsql.plant_canonical (TEXT work_name, TEXT kind, UUID[] tokens, UUID target, INT info1, INT info2=0) |
| Plant a certified gate in place of a sum or a product (internal). | |
| 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). | |
| VOID | provsql.eval_recursive_all (TEXT q0_sql, TEXT q1_sql, TEXT work_name, TEXT all_name, TEXT colnames, TEXT coldef, INT max_iter=1000) |
Drive a UNION ALL recursion, one round per bag of derivations. | |
| 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 provsql_rec_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) |
| VOID provsql.eval_recursive_all | ( | TEXT | q0_sql, |
| TEXT | q1_sql, | ||
| TEXT | work_name, | ||
| TEXT | all_name, | ||
| TEXT | colnames, | ||
| TEXT | coldef, | ||
| INT | max_iter = 1000 ) |
Drive a UNION ALL recursion, one round per bag of derivations.
The bag recursion is not a fixpoint over a set: its rounds are M0 = q0 and M(i+1) = q1 over Mi – the PREVIOUS round, not what has been derived so far – and its answer is the bag union of every round, which ends when a round derives nothing. Each tuple of it is one derivation, annotated by the product along that derivation, and two derivations of the same tuple are two rows and are not merged: that is what distinguishes it from UNION, whose driver (eval_recursive) sums the derivations of a tuple into one row and stops when the set of rows stops changing.
work_name holds the previous round, which the recursive term reads by the name of the CTE; all_name accumulates the answer and is what the query reads. Ending on an empty round is SQL's own rule, so a recursion PostgreSQL runs to completion ends here too, and one it does not is caught by max_iter as before.
| q0_sql | the non-recursive term, as SQL |
| q1_sql | the recursive term, reading work_name |
| work_name | temp table of the previous round (the CTE's name) |
| all_name | temp table accumulating the rounds |
| colnames | comma-separated user column names |
| coldef | column definitions ("name type, ...") |
| max_iter | safety bound on the number of rounds |
| UUID provsql.plant_canonical | ( | TEXT | work_name, |
| TEXT | kind, | ||
| UUID[] | tokens, | ||
| UUID | target, | ||
| INT | info1, | ||
| INT | info2 = 0 ) |
Plant a certified gate in place of a sum or a product (internal).
Creates a kind gate with the single child target at the canonical address of the multiset tokens – the v5 UUID of 'plus-canonical{sorted tokens}' or 'times-canonical{…}', a recipe under which nothing else creates gates – and remembers the address in this session: while the working table work_name exists, provenance_plus / provenance_times given that very multiset return the planted gate. The tokens are row tokens of the working table, a temporary table, so the sum or product is computed by the session that planted, never by a parallel worker; the store is not consulted, and sessions that planted nothing pay nothing.
| work_name | working table the tokens belong to |
| kind | 'plus' or 'times' |
| tokens | the multiset the planted gate stands for |
| target | root of the certified circuit |
| info1 | first info of the planted gate |
| info2 | second info of the planted gate |
| VOID provsql.planted_scope | ( | TEXT | work_name | ) |
Declare the working table of a recursive CTE, just (re)created (internal).
Gates planted from now on belong to it; those planted for the table of the same name it replaces, and for working tables that no longer exist, are forgotten.
| work_name | name of the temporary working table |
| 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.Implemented in C (gate_builders.c): the gate is created together with what it records, in one unanswered message.
| 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 |
Implemented in C (gate_builders.c), with the declared cost of the PL/pgSQL function it was, so that plans stay the same.
| 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 |
Implemented in C (gate_builders.c): the gate is created together with what it records, in one unanswered message.
| 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).
Implemented in C (gate_builders.c), with the declared cost of the PL/pgSQL function it was, so that plans stay the same.
| 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. When the multiset is one for which this session planted a certified gate computing the same sum (see plant_canonical), that gate is returned. This is how the bounded-hop reachability route keeps the natural hop-discarding query on the linear evaluation route: it plants, for a vertex's per-length tokens, a certified gate over its native within-bound circuit. Otherwise 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 |
Implemented in C (gate_builders.c): the gate is created together with what it records, in one unanswered message.
| 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.
When the surviving multiset is one for which this session planted a certified equivalent (see plant_canonical; the reachability rewriter does so for self-join conjunctions of reachability tokens, see plant_reach_cover), the planted gate is returned. The ordinary order-dependent recipe is used otherwise, so ordinary times gates (and their formula rendering) are untouched.
Implemented in C (gate_builders.c). The cost is declared as that of a PL/pgSQL function, which this function was: the planner then keeps evaluating it after the cheaper conditions, and the plans of rewritten queries, on which the order of the children of a ⊕ depends, stay the same.