 |
ProvSQL C/C++ API
Adding support for provenance and uncertainty management to PostgreSQL databases
|
|
ProvSQL C/C++ API
Adding support for provenance and uncertainty management to PostgreSQL databases
|
Möbius-inversion exact route for safe UCQs (the last missing exact route of the Dalvi-Suciu dichotomy). More...
#include "postgres.h"#include "fmgr.h"#include "funcapi.h"#include "miscadmin.h"#include "access/htup_details.h"#include "access/xact.h"#include "catalog/pg_type.h"#include "executor/spi.h"#include "utils/array.h"#include "utils/builtins.h"#include "utils/resowner.h"#include "utils/uuid.h"#include "compatibility.h"#include "provsql_utils.h"#include "provsql_mmap.h"#include "c_cpp_compatibility.h"#include "CertifiedDDMaterialize.h"#include "mobius_evaluate.h"#include "provsql_utils_cpp.h"#include <algorithm>#include <cmath>#include <cstdint>#include <functional>#include <limits>#include <map>#include <set>#include <stdexcept>#include <string>#include <unordered_map>#include <unordered_set>#include <vector>
Go to the source code of this file.
Functions | |
| Datum | get_gate_type (PG_FUNCTION_ARGS) |
| Datum | ucq_mobius_materialize_tracked (PG_FUNCTION_ARGS) |
| Materialise the safe-UCQ Möbius circuit and return its root token. | |
| Datum | ucq_mobius_compile_stats (PG_FUNCTION_ARGS) |
| Compile the Möbius circuit and return the lattice statistics plus the probability (the demonstrability surface). | |
| Datum | ucq_mobius_provenance_answer (PG_FUNCTION_ARGS) |
| Per-answer Möbius provenance (the planner-substituted entry point for a non-Boolean UCQ with free head variables). | |
Variables | |
| int | provsql_mobius_max_gates |
Data-cost cap of the Möbius route: it declines (falling through to joint-width / the ladder) once its compile has built more than this many gates, bounding the \(O(|D|^k)\) blow-up of a high-level safe query on large data; provsql.mobius_max_gates GUC. | |
Möbius-inversion exact route for safe UCQs (the last missing exact route of the Dalvi-Suciu dichotomy).
Some unions of conjunctive queries are safe (PTIME data complexity) only because the #P-hard terms of their inclusion-exclusion expansion carry a zero Möbius value on the CNF lattice and cancel. The canonical witness is QW / q9 (Dalvi-Suciu 2012; Monet & Olteanu 2018). No other ProvSQL route handles it in PTIME: the safe-query rewriter is per-CQ and hierarchical, the query is not inversion-free (that is the point), and on adversarial data the joint treewidth is unbounded.
This file packages the extensional lattice-walking algorithm (Dalvi, Schnaitter & Suciu, "Computing query probability with incidence algebras", PODS 2010) the way the joint-width route already is: a compile-at-execution step producing a certified circuit over the gathered data, and a linear evaluation – the only genuinely new evaluation primitive being a signed linear combination at gate_mobius nodes (see provsql_utils.h and the gate_mobius handling in probability_evaluate.cpp).
The probability of a UCQ Q given in CNF as \(\bigwedge_i d_i\) is, by inclusion-exclusion on the \(\lnot d_i\),
\[ P(Q) = \sum_{\emptyset\neq s\subseteq[M]} (-1)^{|s|+1} P\Big(\bigvee_{i\in s} d_i\Big), \]
and grouping the \(\bigvee_{i\in s} d_i\) up to logical equivalence collapses the hard term (its coefficient sums to zero – the whole game). Each surviving \(\bigvee_{i\in s} d_i\) is a safe disjunctive sentence, compiled recursively by the standard IndepStep / MobiusStep lifted-inference recursion (component split, disjoint-symbol product, separator independent-project, inner Möbius step) into certified-independent Boolean islands, combined at the root gate_mobius by the signed coefficients.
Self-joins and constants are handled by the two normalizations the JACM dichotomy runs before its lifted recursion – ranking (Def. 4.1) and shattering (Prop. 2.10) – implemented here as one shard split (normalizeShards): each relation whose atoms do not all carry the trivial all-distinct-variables pattern is partitioned into shard symbols, one per (equality pattern, pinned query constants) signature of its tuples, and every atom is expanded into the disjunction of its compatible shards. Because the shards partition the relation, disjoint shard symbols certify disjoint tuples, which is what the independence steps of the recursion rest on. A within-disjunct self-join that survives normalization (two components over one shard symbol, the JACM's \(q_J\)) is not independent and is not declined either: it falls through to the Möbius step, whose \(P(c_1\land c_2) = P(c_1)+P(c_2)-P(c_1\lor c_2)\) is exactly the disjunctive detour the self-join forces (JACM Example 3.1).
Restrictions: tuple-independent (TID) inputs, one probabilistic tuple per (relation, element tuple), and no two fact slots sharing a base tuple. A query shape the recursion cannot certify (an inversion, a #P-hard CQ, a cap exceeded) declines (a C++ exception caught at the SQL boundary), so the query falls back to the normal provenance and never fails.
Definition in file mobius_evaluate.cpp.
|
extern |
| Datum ucq_mobius_compile_stats | ( | PG_FUNCTION_ARGS | ) |
Compile the Möbius circuit and return the lattice statistics plus the probability (the demonstrability surface).
Same columnar arguments as ucq_mobius_materialize_tracked.
Definition at line 1676 of file mobius_evaluate.cpp.
| Datum ucq_mobius_materialize_tracked | ( | PG_FUNCTION_ARGS | ) |
Materialise the safe-UCQ Möbius circuit and return its root token.
Columnar arguments (mirrors ucq_joint_materialize_tracked, TID inputs): 0..4 disjunct_nvars, atom_disjunct, atom_rel, atom_vars, atom_arity 5..8 fact_rel, fact_elems, fact_arity, fact_tokens 9 lineage (uuid, optional): the literal Boolean provenance of the query, carried on the root gate_mobius so the token still answers Shapley / semiring / PROV on the normal lineage (the Möbius combination is a probability-only shortcut layered over it).
The root is a gate_mobius carrying the certified-independent Boolean islands (the signed combination) and the lineage child; probability_evaluate answers the #P-hard UCQ in PTIME through the fast Möbius route, and every other evaluator passes through to the lineage. Declines raise an error so the SQL wrapper falls back.
Definition at line 1648 of file mobius_evaluate.cpp.
| Datum ucq_mobius_provenance_answer | ( | PG_FUNCTION_ARGS | ) |
Per-answer Möbius provenance (the planner-substituted entry point for a non-Boolean UCQ with free head variables).
Arguments: (descriptor jsonb, head_vars int[], head_vals text[], fallback uuid). Called once per output group; on the first call the facts are gathered once and the value dictionary cached, then each group pins its head variables (the canonical head indices head_vars, in every disjunct) to their values (head_vals, matched through the gather's text dictionary) and compiles the head-pinned Möbius circuit, caching head-key -> token. On any decline (unsafe shape, head value absent, ...) returns fallback.
Definition at line 1721 of file mobius_evaluate.cpp.
|
extern |
