 |
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
|
RV / AGG_TOKEN evaluators return the restricted distribution. More...
Topics | |
| Provenance table management | |
| Create a new gate in the provenance circuit. | |
Functions | |
| VOID | create_gate (UUID token, PROVENANCE_GATE type, UUID[] children=NULL) |
| Create a new gate in the provenance circuit. | |
| PROVENANCE_GATE | get_gate_type (UUID token) |
| Return the gate type of a provenance token. | |
| UUID[] | get_children (UUID token) |
| Return the children of a provenance gate. | |
| VOID | set_prob (UUID token, DOUBLE PRECISION p) |
| Set the probability of an input gate. | |
| DOUBLE PRECISION | get_prob (UUID token) |
| Get the probability associated with an input gate. | |
| VOID | set_infos (UUID token, INT info1, INT info2=NULL) |
| Set additional INTEGER values on provenance circuit gate. | |
| RECORD | get_infos (UUID token, OUT INT info1, OUT INT info2) |
| Get the INTEGER info values associated with a circuit gate. | |
| UUID | provenance_assume (UUID token, TEXT assumption) |
Wrap token in a fresh gate_assumed carrying assumption as its label, and return the wrapper's UUID. | |
| UUID | assume_boolean (UUID token) |
Wrap token in a Boolean-assumption marker (compatibility name; see provenance_assume). | |
| UUID | annotate (UUID token, TEXT extra) |
Wrap token in a fresh transparent gate_annotation carrying extra, and return the wrapper's UUID. | |
| UUID | cond (UUID target, UUID evidence) |
| Condition a provenance token (a Boolean event) on another. | |
| BOOLEAN | UUID_op_UUID (UUID left, UUID right) |
Binary "target | evidence". | |
| UUID | cond_predicate (UUID target, BOOLEAN predicate) |
Placeholder for "X | (predicate)" on a UUID event. | |
| BOOLEAN | UUID_op_boolean (UUID left, BOOLEAN right) |
| UUID | regular_indicator (BOOLEAN cond) |
| Deterministic indicator gate for an ordinary (regular) comparison. | |
| UUID | given (UUID evidence) |
Whole-tuple output conditioning directive: "given(evidence)". | |
| UUID | given_predicate (BOOLEAN predicate) |
Prefix unary given, "| evidence". | |
| UUID | provenance_not (UUID event) |
Event negation: "! event" / "provenance_not(event)". | |
| TEXT | inversion_free_key (TEXT root, TEXT sec, INT factor) |
Prefix unary ! | |
| VOID | set_extra (UUID token, TEXT data) |
| Set extra TEXT information on provenance circuit gate. | |
| TEXT | get_extra (UUID token) |
| Get the TEXT-encoded extra data associated with a circuit gate. | |
| BIGINT | get_nb_gates () |
| Return the total number of materialized gates in the provenance circuit. | |
RV / AGG_TOKEN evaluators return the restricted distribution.
Low-level functions for creating and querying provenance circuit gates.
For the UUID carrier it is a TERMINAL gate (never a child of a semiring gate); nested conditioning folds into a conjunction of evidence. Refused by every general sr_* semiring (normalization is not a semiring operation). Signed Möbius combination over child islands: one INTEGER coefficient per child in extra (the gate_arith precedent), probability_evaluate returns Σ_i coeff_i · P(child_i). The one new primitive of the safe-UCQ Möbius-inversion route, evaluated only in the measure interpretation; refused by every general sr_* semiring (a signed combination is not a semiring operation).
Low-level functions for creating and querying provenance circuit gates.
| UUID update_provenance::annotate | ( | UUID | token, |
| TEXT | extra ) |
Wrap token in a fresh transparent gate_annotation carrying extra, and return the wrapper's UUID.
Unlike every other gate, the annotation wrapper's UUID folds in extra (not just the child): uuid_generate_v5 over concat('annotation', token, extra). This is deliberate – two annotations over the same child with different extra must be distinct gates (e.g. the same input tuple carrying different per-occurrence order keys, or two queries attaching different certificates to a shared root). The wrapper is transparent (identity) for EVERY evaluator; extra is inert metadata read only by the code that placed it. No-op (returns NULL) on a NULL input.
| UUID update_provenance::assume_boolean | ( | UUID | token | ) |
Wrap token in a Boolean-assumption marker (compatibility name; see provenance_assume).
| UUID update_provenance::cond | ( | UUID | target, |
| UUID | evidence ) |
Condition a provenance token (a Boolean event) on another.
Builds the terminal gate_conditioned that the measure evaluators read as "P(target ∧ evidence) / P(evidence)". This is the backing function of the binary | operator ("target | evidence", value-level conditioning of the UUID carrier).
The gate stores three children [target, evidence, joint] with joint = times(target, evidence); evaluation is then the plain ratio P(joint)/P(evidence), and content-addressing makes a base tuple shared by target and evidence the same input gate in both circuits, so the conditional is exact and correlation-aware.
Conventions:
evidence NULL or gate_one() returns target unchanged ("P(X|true)=P(X)").target with no provenance defaults to the certain event 1, so "1 | c" is the well-defined certain-row posterior."(X | A) | B = X | (A ∧ B)" – the gate never nests, it stays one level deep with the evidence accumulated by times.The result is TERMINAL: a conditioned token may not become a child of a plus / times / monus / agg gate (those constructors refuse it); the only operation it admits is more conditioning.
| UUID update_provenance::cond_predicate | ( | UUID | target, |
| BOOLEAN | predicate ) |
Placeholder for "X | (predicate)" on a UUID event.
Lets the conditioning event be written as a natural Boolean combination of random_variable / aggregate comparisons (e.g. "event | (sensor > 3)") instead of a hand-built gate. Never executes: the ProvSQL planner hook converts the Boolean operand into a condition gate and emits cond.
| VOID update_provenance::create_gate | ( | UUID | token, |
| PROVENANCE_GATE | type, | ||
| UUID[] | children = NULL ) |
Create a new gate in the provenance circuit.
| token | UUID identifying the new gate |
| type | gate type (see PROVENANCE_GATE) |
| children | optional array of child gate UUIDs |
| UUID[] update_provenance::get_children | ( | UUID | token | ) |
Return the children of a provenance gate.
| TEXT update_provenance::get_extra | ( | UUID | token | ) |
Get the TEXT-encoded extra data associated with a circuit gate.
| PROVENANCE_GATE update_provenance::get_gate_type | ( | UUID | token | ) |
Return the gate type of a provenance token.
Returns 'input' for any token not yet materialized in the circuit, since input is the default semantics of an unmaterialized provenance token.
| RECORD update_provenance::get_infos | ( | UUID | token, |
| OUT INT | info1, | ||
| OUT INT | info2 ) |
Get the INTEGER info values associated with a circuit gate.
| BIGINT update_provenance::get_nb_gates | ( | ) |
Return the total number of materialized gates in the provenance circuit.
Input gates for provenance-tracked table rows are created lazily on first reference; rows that have never appeared in a query result are not counted.
| DOUBLE PRECISION update_provenance::get_prob | ( | UUID | token | ) |
Get the probability associated with an input gate.
| UUID update_provenance::given | ( | UUID | evidence | ) |
Whole-tuple output conditioning directive: "given(evidence)".
Written as a term in the select list, given(c) conditions the OUTPUT provenance of the current query's rows on c:
The query rewriter recognises the marker, STRIPS it from the visible projection, and wraps each output row's provenance expression in cond(row_provenance, c) – deriving a new conditioned relation, never mutating any stored provenance. c is evaluated per output row and may correlate with the row's columns, so each tuple is conditioned on its own evidence. When the rewriter is inactive the call is a harmless identity (it returns evidence as an ordinary column).
| UUID update_provenance::given_predicate | ( | BOOLEAN | predicate | ) |
Prefix unary | : alias for given, "| evidence".
Disambiguated from the binary | by the absence of a left operand ("a, | c" parses "| c" as the prefix form). PostgreSQL keeps prefix operators on every supported version (postfix operators were removed in PG14), so "| c" is safe across the CI matrix.
Placeholder for the prefix "| (predicate)" whole-tuple form.
Lets the whole-tuple conditioning event be a natural Boolean predicate (e.g. "SELECT a, | (sensor > 3) FROM readings") instead of a hand-built gate. Never executes: the planner converts the Boolean operand into a condition gate and emits given, which the rewriter then strips and folds into each output row's provenance.
| TEXT update_provenance::inversion_free_key | ( | TEXT | root, |
| TEXT | sec, | ||
| INT | factor ) |
Prefix unary !
: alias for provenance_not, "! event".
Prefix operators are kept on every supported PostgreSQL version (postfix operators were removed in PG14), and core PG defines no prefix ! on UUID, so "! event" is safe across the CI matrix.
Build a per-input order-key string for the inversion-free path.
Emitted by the planner per certified atom: K-prefixed, length-prefixed "K<factor> <octet_length(root)>:<root><octet_length(sec)>:<sec>", parsed back at evaluation by safe_cert_key_parse. root / sec are the tuple's root- and secondary-class column values (TEXT-cast by the caller); the byte-length prefixes keep the values unambiguous for any column type, including TEXT containing spaces, colons or digits. factor is the atom's factor id (or -1 for the shared self-join guard). IMMUTABLE so the planner can fold it and the marker dedups by content-addressing.
| UUID update_provenance::provenance_assume | ( | UUID | token, |
| TEXT | assumption ) |
Wrap token in a fresh gate_assumed carrying assumption as its label, and return the wrapper's UUID.
Public primitive callable from any rewrite or driver that needs to flag a sub-circuit as sound only under an evaluation assumption:
'BOOLEAN' – the sub-circuit only preserves the Boolean function of the lineage (e.g. the safe-query rewrite collapses derivation multiplicities); transparent for semirings admitting a homomorphism from Boolean functions.'absorptive' – the sub-circuit was truncated at the absorptive value fixpoint (cyclic recursive query); transparent for absorptive semirings (probability, BOOLEAN, min-plus over nonnegative costs...), fatal for the rest (counting, why-provenance).Incompatible evaluators raise a CircuitException. Always kept as an explicit node in PROV-XML export.
The wrapper UUID is content-derived via uuid_generate_v5 on the assumption and the child, so identical children always wrap to the same outer UUID per assumption. No-op (returns NULL) on a NULL input.
| UUID update_provenance::provenance_not | ( | UUID | event | ) |
Event negation: "! event" / "provenance_not(event)".
The complement of a Boolean provenance event: "!x" holds in exactly the worlds where x does not. It is sugar for "monus(one, x)" -- an ordinary m-semiring expression (Boolean NOT, probability "1 - P(x)"), NOT a measure-only marker – so it composes like any monus, and a conditioned / terminal token is refused as its child (so "!(x | c)" errors, as conditioning cannot be buried under further algebra).
The motivating use is conditioning on the NON-occurrence of an arbitrary violation query W (a denial constraint), where W itself is built with ordinary idioms and needs no hand-rolled gates:
Named provenance_not, after the "provenance_times / _plus / _monus" family; the prefix ! operator is the ergonomic form (SQL's reserved NOT keyword cannot serve as a function name).
| UUID update_provenance::regular_indicator | ( | BOOLEAN | cond | ) |
Deterministic indicator gate for an ordinary (regular) comparison.
The predicate-provenance of an ordinary comparison (both sides of regular type, e.g. "region = 'north'") is the deterministic indicator "χ(cond)": gate_one() when the comparison holds on the row, gate_zero() otherwise (Definition in the HAVING-provenance semantics). The planner emits this for a regular comparison appearing inside a MIXED conditioning predicate (one that also has a random_variable / aggregate comparison); cond is evaluated per row, so the indicator is the row's own truth value, combined by ⊗ / ⊕ with the probabilistic gates.
| VOID update_provenance::set_extra | ( | UUID | token, |
| TEXT | data ) |
Set extra TEXT information on provenance circuit gate.
This function sets TEXT-encoded data associated to a circuit gate, used in different ways by different gate types:
| token | UUID of the circuit gate |
| data | TEXT-encoded information |
| VOID update_provenance::set_infos | ( | UUID | token, |
| INT | info1, | ||
| INT | info2 = NULL ) |
Set additional INTEGER values on provenance circuit gate.
This function sets two INTEGER values associated to a circuit gate, used in different ways by different gate types:
| token | UUID of the circuit gate |
| info1 | first INTEGER value |
| info2 | second INTEGER value |
| VOID update_provenance::set_prob | ( | UUID | token, |
| DOUBLE PRECISION | p ) |
Set the probability of an input gate.
| token | UUID of the input gate |
| p | probability value in [0,1] |
| BOOLEAN update_provenance::UUID_op_boolean | ( | UUID | left, |
| BOOLEAN | right ) |
| BOOLEAN update_provenance::UUID_op_UUID | ( | UUID | left, |
| UUID | right ) |
Binary | : value-level conditioning, "target | evidence".
Carrier-parametric in its left operand; the UUID form builds the terminal gate_conditioned via cond. Does not collide with core PostgreSQL's INTEGER bitwise | (different argument types).