Worked example: query evaluation over probabilistic databases #

This file is a tutorial, read top to bottom like DescriptiveComplexity.Examples.ConjunctiveQueries, and the first one about a counting problem. The domain is probabilistic databases: a database whose facts are present independently, each with its own probability, and the problem of computing the probability that a fixed Boolean query holds (probabilistic query evaluation). Its data complexity is #P-hard already for the conjunctive query

h₀ = ∃ x y, R(x) ∧ S(x, y) ∧ T(y)

(Dalvi and Suciu 2012, Proposition 5.2), which is the first result formalized here; the second is that on the same instances the query

∃ x y, R(x) ∧ S(x, y)

is easy: the numerator of its probability is in FP, the polynomial-time functions. The two queries are the smallest pair on the two sides of the dichotomy of that paper, the second being hierarchical and the first not; the dichotomy itself is not formalized, and nothing here is generic in the query.

The model #

A fact is certain, or it is uncertain and present with some probability, independently of the others. The file works in two stages.

Uniform probability. Steps 1 to 6 take every uncertain fact to be present with probability 1/2. A probability is then a count: with k uncertain facts there are 2 ^ k equally likely possible worlds (DescriptiveComplexity.card_isWorld), and the probability of a query is the number of worlds in which it holds, divided by 2 ^ k. This is all the hardness of h₀ needs.
Probabilities in the instance. Step 7 gives each uncertain fact its own probability a / (a + c), as two natural weights written in binary (DescriptiveComplexity.Counting.WeightedWorlds). The probability of a query is then a ratio of two numbers, WeightedWorlds φ / WeightedWorlds ⊤ (DescriptiveComplexity.funcProb_holdsEvent_eq_ratio), both of them in #P for every first-order query (DescriptiveComplexity.weightedWorlds_mem_sharpP). The uniform case is the case where all weights are 1, so the hardness of h₀ carries over to the numerator.

The steps #

Vocabulary. The schema FirstOrder.Language.rst of the query; an instance is a structure over two copies of it, certain facts and uncertain ones. This step, and the next two, are generic in the schema and are library helpers, in DescriptiveComplexity.Counting.PossibleWorlds.
Semantics. A possible world keeps the certain facts and some of the uncertain ones (DescriptiveComplexity.IsWorld), and DescriptiveComplexity.PossibleWorlds φ counts the worlds satisfying φ.
Membership. A world is one relation per symbol of the schema, so the problem counts the witnesses of a first-order kernel: it is in #P for every first-order query (DescriptiveComplexity.possibleWorlds_mem_sharpP). Nothing is specific to h₀ up to here.
The query, DescriptiveComplexity.h0, and what it says of a world (DescriptiveComplexity.realize_h0).
Hardness. From #PP2DNF (DescriptiveComplexity.SharpPP2DNF), the models of ⋁ (x ∧ y) over the edges of a bipartite graph. The instance has the edges as certain S-facts, the left vertices as uncertain R-facts and the right vertices as uncertain T-facts (DescriptiveComplexity.h0Interp); a world is then a set of vertices, and h₀ holds in it exactly when some edge has both ends chosen (DescriptiveComplexity.possibleWorlds_h0_eq). The reduction is parsimonious, one-dimensional and quantifier-free.
The theorem: counting the worlds of h₀ is one-call #P-complete (DescriptiveComplexity.possibleWorlds_h0_sharpP_oneCallComplete).
Probabilities in the instance: the numerator of the probability of h₀ is one-call #P-complete (DescriptiveComplexity.weightedWorlds_h0_sharpP_oneCallComplete), by the ordered parsimonious reduction from the uniform case (DescriptiveComplexity.possibleWorlds_ordered_parsimonious_weightedWorlds).
A concrete database. DescriptiveComplexity.ProbDb is a probabilistic database in plain terms: n constants and, for each possible fact, whether it is absent, certain, or uncertain with two weights. Its weighted count DescriptiveComplexity.ProbDb.count and its total weight DescriptiveComplexity.ProbDb.total are computed (the #guards at the end run them). DescriptiveComplexity.probDbEncoding encodes a database as a weighted instance, with the size bounds of DescriptiveComplexity.Encoding discharged, and it is faithful (DescriptiveComplexity.probDbEncoding_countFaithful, DescriptiveComplexity.probDbEncoding_countFaithful_total): the abstract counting problems return, on the encoded instance, the two numbers computed from the database. So the probability of h₀ over a database is count / total (DescriptiveComplexity.probDb_worldProb_eq).

What kind of hardness #

#PP2DNF is itself complete under one-call reductions only, so the statement is one-call completeness, not plain completeness: every problem of #P is answered by one question about the probability of h₀, followed by arithmetic. A formula of this kind always has a world in which it holds as soon as the graph has an edge, so no parsimonious reduction from #SAT can exist unless P = NP. Whether the problem is complete under subtractive reductions is not known here.

The decoder. DescriptiveComplexity.probDbDecode reads a database back from any presented weighted instance whose position order is linear, by a computation (it runs, too), and the database has the weighted count of the instance (DescriptiveComplexity.probDbDecoding, a DescriptiveComplexity.CountDecoding). So the hardness of the abstract problem is hardness on instances that are databases.

The easy query #

Steps 10 to 15 are the second result, on the same weighted instances.

The query, DescriptiveComplexity.rs.
The weights. Every fact is a Boolean variable with a weight of presence and a weight of absence (DescriptiveComplexity.Counting.WeightedFacts); the facts of the schema are the R-facts, the S-facts and the T-facts (DescriptiveComplexity.factEquiv).
Failing is a product. The query fails in a world when no x has both R(x) and some S(x, y). Given which R-facts are present, this constrains each S-fact separately; summing over the R-facts then factorizes too. The weight of the worlds in which the query fails is ∏x. F(x), times the total weight of the T-facts (DescriptiveComplexity.SafeQ.weightedCount_fail), F(x) being the weight of failing at x.
Succeeding, without a subtraction. The weight of the worlds in which the query holds is the total weight minus that product. A quantitative term has no subtraction; the first success identity (DescriptiveComplexity.prod_add_eq_prod_add_sum) removes it, by sorting the worlds by the first x at which the query succeeds – and, inside the weight of succeeding at x, by the first y (DescriptiveComplexity.SafeQ.weightedWorlds_rs_eq).
The term. The closed form is a term of quantitative first-order logic over the instance, its leaves being the weights, read in binary (DescriptiveComplexity.SafeQ.rsT). The order it sorts by is the order of the definition, on which the value does not depend.
The theorem: DescriptiveComplexity.weightedWorlds_rs_mem_FP.

Steps 12 and 13 use the library's lemmas on independent Boolean variables (DescriptiveComplexity.Counting.Independence), and step 14 its helpers for writing terms (DescriptiveComplexity.Counting.QuantitativeBinders, DescriptiveComplexity.Counting.WeightedTerms).

The concrete step, and what it relies on #

The two other tutorials open with the concrete instances; here they come last (steps 8 and 9), the hardness result needing none of it. The encoder and the decoder are two corollaries of one theorem: an instance that matches a database (DescriptiveComplexity.ProbDb.Matches) has its counts (DescriptiveComplexity.ProbDb.Matches.count_eq). The step is short because its two generic ingredients are library lemmas: the binary digits written by an encoder decode to the number they came from (DescriptiveComplexity.binNum_fin_of_testBit, in DescriptiveComplexity.Numbers.BinEnum), and faithfulness for a counting problem is DescriptiveComplexity.Encoding.CountFaithful. What remains is specific to the database format: reading a status off each fact (DescriptiveComplexity.factWeight_of_status) and matching the abstract worlds and facts with the three tables of a concrete world (DescriptiveComplexity.worldEquiv, DescriptiveComplexity.factEquiv).

One restriction of the format is deliberate: the weights are written on n bits, n being the number of constants, since the constants double as bit positions. A database with longer weights is padded with unused constants.

Worked example: query evaluation over probabilistic databases #

The model #

The steps #

What kind of hardness #

The easy query #

The concrete step, and what it relies on #

Steps 1 and 4: the schema, and the query #

Step 5: hardness, from #PP2DNF #

Step 6: the theorems #

Step 7: probabilities in the instance #

Step 8: a concrete database, and its encoding #

The concrete semantics #

Faithfulness #

The encoding is faithful #

Step 9: the decoder #

A database, computed #

Step 10: the easy query #

Step 11: the weights #

Step 12: failing is a product #

Step 13: succeeding, without a subtraction #

Step 14: the term #

Step 15: the theorem #