 |
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
|
Definitions of compiled semirings. More...
Functions | |
| VARCHAR | provsql.sr_formula (ANYELEMENT token, REGCLASS token2value) |
| Evaluate provenance as a symbolic formula (e.g., "a ⊗ b ⊕ c"). | |
| INT | provsql.sr_counting (ANYELEMENT token, REGCLASS token2value) |
| Evaluate provenance over the counting semiring (ℕ). | |
| VARCHAR | provsql.sr_why (ANYELEMENT token, REGCLASS token2value) |
| Evaluate provenance as why-provenance (set of witness sets). | |
| VARCHAR | provsql.sr_how (ANYELEMENT token, REGCLASS token2value) |
| Evaluate provenance as how-provenance (canonical polynomial provenance ℕ[X], universal commutative-semiring provenance). | |
| VARCHAR | provsql.sr_which (ANYELEMENT token, REGCLASS token2value) |
| Evaluate provenance as which-provenance (lineage: a single set of contributing labels). | |
| VARCHAR | provsql.sr_boolexpr (ANYELEMENT token, REGCLASS token2value=NULL) |
| Evaluate provenance as a Boolean expression. | |
| BOOLEAN | provsql.sr_boolean (ANYELEMENT token, REGCLASS token2value) |
| Evaluate provenance over the Boolean semiring (true/false). | |
| BOOLEAN | provsql.true_nonzero (UUID token) |
| Structural universal-zero test (C backend of nonzero's default mode). | |
| BOOLEAN | provsql.nonzero (UUID token, TEXT semiring=NULL, REGCLASS mapping=NULL) |
| Test whether a provenance annotation is nonzero. | |
| BOOLEAN | provsql.present (UUID token) |
| Presence in the vanilla SQL answer on this instance. | |
| FLOAT | provsql.sr_tropical (ANYELEMENT token, REGCLASS token2value, BOOLEAN nonnegative=false) |
| Evaluate provenance over the tropical (min-plus) m-semiring. | |
| FLOAT | provsql.sr_viterbi (ANYELEMENT token, REGCLASS token2value) |
| Evaluate provenance over the Viterbi (max-times) m-semiring. | |
| FLOAT | provsql.sr_lukasiewicz (ANYELEMENT token, REGCLASS token2value) |
| Evaluate provenance over the Łukasiewicz fuzzy m-semiring. | |
| ANYENUM | provsql.sr_minmax (UUID token, REGCLASS token2value, ANYENUM element_one) |
| Evaluate provenance over the min-max m-semiring on a user ENUM. | |
| ANYENUM | provsql.sr_maxmin (UUID token, REGCLASS token2value, ANYENUM element_one) |
| Evaluate provenance over the max-min m-semiring on a user ENUM. | |
Definitions of compiled semirings.
| BOOLEAN provsql.nonzero | ( | UUID | token, |
| TEXT | semiring = NULL, | ||
| REGCLASS | mapping = NULL ) |
Test whether a provenance annotation is nonzero.
Returns false only on a proof that the annotation is zero; true otherwise, so filtering with WHERE nonzero(provenance()) never discards a row whose annotation could be nonzero.
The default mode (semiring NULL) tests universal zero-ness: zero in every (m-)semiring under every leaf valuation, decided by sound structural rules (zero propagation through the gates; a comparison gate whose satisfying-world set is empty). Filtering on it can never contradict any downstream semiring evaluation.
A named semiring evaluates the circuit there and tests against that semiring's zero: 'BOOLEAN' is presence in the vanilla SQL answer on this instance (the mode that filters, e.g., the null-padded arm of a difference), 'counting' is bag multiplicity. An absent mapping reads every leaf as the semiring's one (true / 1); with a mapping, leaves take their mapped values.
A NULL token reads as the neutral 1 (an untracked row): true.
| token | provenance token to test |
| semiring | NULL (universal zero test), 'BOOLEAN', or 'counting' |
| mapping | optional mapping table from tokens to leaf values |
| BOOLEAN provsql.present | ( | UUID | token | ) |
Presence in the vanilla SQL answer on this instance.
Shorthand for nonzero(token, 'BOOLEAN') with every leaf true: WHERE present(provenance()) restores the result set the query has without provenance tracking, filtering the zero-annotated extras (antijoin arms, failed HAVING groups, unknown comparisons) that the rewriting keeps visible.
| BOOLEAN provsql.sr_boolean | ( | ANYELEMENT | token, |
| REGCLASS | token2value ) |
Evaluate provenance over the Boolean semiring (true/false).
| VARCHAR provsql.sr_boolexpr | ( | ANYELEMENT | token, |
| REGCLASS | token2value = NULL ) |
Evaluate provenance as a Boolean expression.
The optional token2value mapping labels the leaves of the formula: when omitted, leaves are rendered as bare x<id> placeholders.
| INT provsql.sr_counting | ( | ANYELEMENT | token, |
| REGCLASS | token2value ) |
Evaluate provenance over the counting semiring (ℕ).
| VARCHAR provsql.sr_formula | ( | ANYELEMENT | token, |
| REGCLASS | token2value ) |
Evaluate provenance as a symbolic formula (e.g., "a ⊗ b ⊕ c").
| VARCHAR provsql.sr_how | ( | ANYELEMENT | token, |
| REGCLASS | token2value ) |
Evaluate provenance as how-provenance (canonical polynomial provenance ℕ[X], universal commutative-semiring provenance).
| FLOAT provsql.sr_lukasiewicz | ( | ANYELEMENT | token, |
| REGCLASS | token2value ) |
Evaluate provenance over the Łukasiewicz fuzzy m-semiring.
Inputs are read as float8 graded-truth values in \([0,1]\). Addition is \(\max\); multiplication is the Łukasiewicz t-norm \(\max(a + b - 1, 0)\), which preserves crisp truth and avoids the near-zero collapse of long product chains.
| ANYENUM provsql.sr_maxmin | ( | UUID | token, |
| REGCLASS | token2value, | ||
| ANYENUM | element_one ) |
Evaluate provenance over the max-min m-semiring on a user ENUM.
Dual of :sqlfunc:sr_minmax: addition is ENUM-max, multiplication is ENUM-min. The fuzzy / availability / trust shape: alternatives combine to the most permissive label, joins combine to the strictest label. The third argument is a sample value of the carrier ENUM, used only for type inference; its value is ignored.
| token | Provenance token to evaluate. |
| token2value | Mapping from input gates to ENUM values. |
| element_one | Sample value of the carrier ENUM (any value works). |
| ANYENUM provsql.sr_minmax | ( | UUID | token, |
| REGCLASS | token2value, | ||
| ANYENUM | element_one ) |
Evaluate provenance over the min-max m-semiring on a user ENUM.
Inputs are read as values of a user-defined ENUM carrier; addition is ENUM-min, multiplication is ENUM-max. Bottom and top of the ENUM are derived from pg_enum.enumsortorder. The third argument is a sample value of the carrier ENUM, used only for type inference; its value is ignored.
The security shape: alternative derivations combine to the least sensitive label, joins combine to the most sensitive label.
| token | Provenance token to evaluate. |
| token2value | Mapping from input gates to ENUM values. |
| element_one | Sample value of the carrier ENUM (any value works). |
| FLOAT provsql.sr_tropical | ( | ANYELEMENT | token, |
| REGCLASS | token2value, | ||
| BOOLEAN | nonnegative = false ) |
Evaluate provenance over the tropical (min-plus) m-semiring.
Inputs are read as float8 cost values; the additive identity is 'Infinity'::float8 and the multiplicative identity is 0. Returns the cost of the cheapest derivation.
With nonnegative, input costs are checked nonnegative and the semiring is absorptive: evaluation then also accepts circuits carrying the 'absorptive' assumption marker – notably cyclic recursive queries truncated at the absorptive value fixpoint, giving exact min-cost reachability on cyclic data.
| FLOAT provsql.sr_viterbi | ( | ANYELEMENT | token, |
| REGCLASS | token2value ) |
Evaluate provenance over the Viterbi (max-times) m-semiring.
Inputs are read as float8 probability values in \([0,1]\). Returns the probability of the most likely derivation.
| VARCHAR provsql.sr_which | ( | ANYELEMENT | token, |
| REGCLASS | token2value ) |
Evaluate provenance as which-provenance (lineage: a single set of contributing labels).
| VARCHAR provsql.sr_why | ( | ANYELEMENT | token, |
| REGCLASS | token2value ) |
Evaluate provenance as why-provenance (set of witness sets).
| BOOLEAN provsql.true_nonzero | ( | UUID | token | ) |
Structural universal-zero test (C backend of nonzero's default mode).