Lifted probabilistic inference#

This page lists the strategies NeuroLang uses to compute the probability of a query exactly by lifted inference, that is by translating the query into a plan of relational algebra operations on probabilities, without grounding the program into a propositional formula. For each strategy it gives the formula applied, when it applies and the reference it comes from.

Solvers and their order#

NeurolangPDL tries its solvers in order, and uses the first one which accepts the query:

  1. neurolang.probabilistic.small_dichotomy_theorem_based_solver, for hierarchical queries without self-joins (see Hierarchical queries without self-joins);

  2. neurolang.probabilistic.dalvi_suciu_lift, which first plans non-repeating queries with negation (see Non-repeating queries with negation), and otherwise lifts unions of conjunctive queries with self-joins (see Dalvi–Suciu lifting), extended to negations and comparisons which share relations with the rest of the query (see Negations and comparisons sharing relations);

  3. neurolang.probabilistic.weighted_model_counting, which is not lifted: it compiles the provenance of the query into a sentential decision diagram (SDD) [Darwiche2011] with pysdd and computes its weighted model count [Chavira2008]. It answers every query of the language but can be exponential in the size of the data.

A lifted solver declines a query by raising an UnsupportedSolverError, such as NonLiftableException, and the next one is then tried. Lifted plans are computed on the provenance semiring of probabilities (neurolang.relational_algebra_provenance), whose operations are listed in Operations of the lifted plans. Conditional queries (//, given, conditioned to) are answered as the ratio of two such queries, the joint and the condition.

The probabilistic semantics are those of CP-Logic [Vennekens2009], and the overall approach is described in [Zanitti2023]. Probabilistic facts are tuple-independent relations; probabilistic choices are relations with a single key-less block, where exactly one tuple is true, a special case of block-independent disjoint (BID) relations [Suciu2011].

Operations of the lifted plans#

Each operation computes the probability \(p\) of each tuple of its result from the probabilities of its inputs.

Operation

Probability

Used for

NaturalJoin (\(\bowtie\))

\(p_1 \, p_2\)

independent conjunction

Union

\(1 - (1 - p_1)(1 - p_2)\)

independent disjunction

Difference

\(p_1 \, (1 - p_2)\)

independent negation, \(A \land \lnot B\)

Subtraction (\(-_P\))

\(p_1 - p_2\)

\(P[A] - P[A \land B]\), for dependent \(A\) and \(B\)

IndependentProjection (ind-∃-π)

\(1 - \prod_i (1 - p_i)\)

existential quantifier on a separator variable

IndependentProjectionUniversal (ind-∀-π)

\(\prod_i p_i\)

universal quantifier on a separator variable

DisjointProjection (disj-π)

\(\sum_i p_i\)

projection of mutually exclusive tuples

WeightedNaturalJoin (Σ)

\(\sum_j w_j \, p_j\)

inclusion–exclusion with Möbius weights

Support

\(1\)

the tuples of a plan, to give values to its variables

Preparing the query#

Before lifting, solve_succ_query() rewrites the query as follows.

Flattening

The rules the query depends on are unfolded into its body, giving a union of conjunctive queries in disjunctive normal form.

Absorption in negations

Conjuncts asserted outside a negation are removed from it, by the absorption law

\[A \land \lnot(A \land B) \equiv A \land \lnot B, \qquad A \land \lnot\exists y\,(A \land B) \equiv A \land \lnot\exists y\, B \quad (y \text{ not free in } A).\]

The law holds in every interpretation, hence in every possible world. It removes, for instance, a probabilistic atom repeated within a negation, which can make the query non-repeating, the class of queries with negation for which Fink and Olteanu characterise liftability [Fink2016]. A negated conjunction all of whose conjuncts are asserted is a contradiction and is left unchanged (AbsorbAssertedConjunctsInNegations).

Contradicting disjuncts

A disjunct with a negated conjunct \(\lnot A\), where \(A\) is one of its conjuncts or is asserted by the conjunction of which the disjunction is a conjunct, is removed:

\[A \land (B \lor (C \land \lnot A)) \equiv A \land B, \qquad B \lor (A \land C \land \lnot A) \equiv B,\]

also through the existentials of the disjunct which do not quantify a variable of \(A\). A disjunction all of whose disjuncts are contradictions is left unchanged. The translation of a negated existential to rules gives such disjuncts: \(\lnot\exists y\,(B \land A)\), with \(y\) not free in \(A\), is \(\lnot\exists y\, B \lor \lnot A\), so that

\[A \land \lnot\exists y\,(B \land A) \equiv A \land (\lnot\exists y\, B \lor \lnot A) \equiv A \land \lnot\exists y\, B,\]

which is the absorption in negations, after the translation. For instance, with a choice \(C\), the query \(T(s, t) \land C(s) \land \lnot\exists t_1\, (T(s, t_1) \land t_1 \neq t \land C(s))\) is rewritten without the choice in the negation, and is lifted by the projection on the choice (RemoveContradictingDisjunctsMixin, in AbsorbAssertedConjuncts).

Deterministic negations

A negated conjunct \(\lnot N(\bar x)\) whose atoms are all deterministic relations or comparisons is the same relation in every possible world. With \(G(\bar x)\) the deterministic conjuncts of the query whose variables are among \(\bar x\), it is replaced by a fresh deterministic relation defined by a relational algebra expression,

\[D(\bar x) := G(\bar x) \land \lnot N(\bar x), \qquad G \land \lnot N \equiv G \land D,\]

\(G\) being conjoined within the existentials of \(N\) so that they are range-restricted, as in \(\lnot\exists t_1\,(T(t_1) \land M(s, t_1) \land t_1 \neq t)\). The negation is left unchanged when no non-empty \(G\) binds all of \(\bar x\), for instance when \(N\) is closed (neurolang.probabilistic.deterministic_subqueries). The expression is not evaluated while planning: marked with Materialise, it is a subexpression of the plan, computed as a set when the plan is evaluated.

Probabilistic choices

Two atoms of the same probabilistic choice relation are true together only if they are the same tuple, as exactly one tuple of the choice is true. Their arguments are therefore made equal (lift_optimization_for_choice_predicates()).

Shattering constants

An atom with a constant, such as \(R(x, a)\), is replaced by an atom of a new relation holding the tuples of \(R\) selected on that constant, so that the remaining atoms of \(R\) refer to disjoint sets of tuples [Dalvi2012] (neurolang.probabilistic.shattering).

Ranking

The query must be ranked: there is an order on the variables such that the arguments of every atom follow it [Dalvi2012] (neurolang.probabilistic.ranking). Atoms with a repeated variable, such as \(R(x, x)\), are first replaced by atoms of a new relation holding the selected tuples. A query whose variables still occur in both orders, such as \(\exists x, y\, R(x, y) \land R(y, x)\), is then rewritten into an equivalent ranked query (rank_query()), following Dalvi and Suciu’s Proposition 4.2. The variables to rank are those occurring in both orders or repeated, together with the variables at the same positions of the other atoms of their relations. For every weak order of them, each atom \(R(\bar x)\) becomes an atom of the relation of the tuples of \(R\) whose values at those positions are in that order, and the variables of each rank are the same in every order; the query is the disjunction of these queries, one per order. For \(R(x, y) \land R(y, x)\), the orders \(x < y\), \(x = y\) and \(y < x\) give

\[\exists x_1, x_2\, R_<(x_1, x_2) \land R_>(x_1, x_2) \;\lor\; \exists x_1\, R_=(x_1) \;\lor\; \exists x_1, x_2\, R_<(x_1, x_2) \land R_>(x_1, x_2),\]

with \(R_<\) the tuples \((a, b)\) of \(R\) with \(a < b\), \(R_>\) the tuples \((b, a)\) with \(a < b\), and \(R_=\) the tuples \((a, a)\). The ranked relations are computed on the data, each tuple keeping its probability.

The query is declined, and left to the next solver, when a relation to split is a probabilistic choice or occurs within a negation; when a ranked position has a constant, or a comparison or a function has a ranked variable; when an answer variable is to rank, as Dalvi and Suciu rank Boolean queries, the answer variables being constants; when the ranked columns are not all of real numbers or all of strings, the types with a total order and an equality, or contain NaN; or when more than MAX_RANKED_VARIABLES, two, variables are to rank, as the number of orders, 1, 3, 13, 75…, makes planning exponential. Only variables in both orders in two atoms are detected, as in the check of rankedness: a cycle such as \(R(x, y) \land R(y, z) \land R(z, x)\) is not ranked, which the separator variable rule still checks.

Checks

The query must have no built-in function, except comparisons within existential conjuncts (see Negations and comparisons sharing relations). Unless the check_unate option of [PROBABILISTIC_SOLVER] is turned off (see Performance and Configuration), it must also use a single kind of quantifier and be unate, each relation occurring only positively or only negatively. The negations and comparisons of Negations and comparisons sharing relations are exempt from this check, as their rules check each query they lift.

Hierarchical queries without self-joins#

For a conjunctive query in which no relation occurs twice, the small dichotomy theorem applies [Dalvi2007] [Fink2014]: writing \(at(x)\) for the atoms in which variable \(x\) occurs, the query can be computed in polynomial time if it is hierarchical, that is if for any two variables \(x\) and \(y\),

\[at(x) \subseteq at(y) \quad\text{or}\quad at(x) \supseteq at(y) \quad\text{or}\quad at(x) \cap at(y) = \emptyset,\]

and is #P-hard otherwise. The plan is built from the independent join and existential projection only. This solver declines queries with negations or disjunctions, which are left to the next solver; Fink and Olteanu’s extension of the theorem to negation is described in the next section.

Non-repeating queries with negation#

A query is non-repeating when none of its probabilistic relations occurs twice in it. Fink and Olteanu show that a non-repeating query without union, built from joins, projections and negations, on tuple-independent relations, can be computed in polynomial time if it is hierarchical, and is #P-hard otherwise [Fink2014]. The planner below also accepts disjunctions, comparisons, constants, deterministic relations and probabilistic choices, which this theorem does not cover: its plans are proved correct in Correctness of the plans, and it is not claimed to plan every tractable query. Before Dalvi–Suciu lifting, non_repeating_plan() plans the non-repeating queries with a negation in this way. The negations can be nested and can quantify variables, as in \(\exists x\, R(x) \land \lnot\exists y\, (S(x, y) \land \lnot U(x, y))\), whose quantifiers are mixed once the negations are moved to the atoms, which the checks of Dalvi–Suciu lifting decline.

The query is first rewritten with two equivalences, which hold in every possible world and keep it non-repeating:

  • equalities with a quantified variable are eliminated in every subformula, \(\exists v\, (v = e \land \varphi) \equiv \varphi[e/v]\) for a variable or a constant \(e\), as in \(\lnot\exists u\, (W(s, u) \land u = t) \equiv \lnot W(s, t)\);

  • a negated disjunction is the conjunction of the negated disjuncts, \(\lnot(A \lor B) \equiv \lnot A \land \lnot B\), the disjuncts possibly having different free variables, as in \(M(s, t) \land \lnot(K(s) \lor G(s, t))\).

As the subformulas of a non-repeating query have different relations, they are independent, and the plan is built with the independent operations only:

  • a conjunction is the join of its positive conjuncts, filtered by its comparisons, from which its negated conjuncts are removed with Difference, \(P[A \land \lnot B] = P[A]\,(1 - P[B])\);

  • a disjunction of formulas with the same free variables is their independent union;

  • \(\exists \bar v\, (\varphi_1 \lor \varphi_2)\) is planned as \(\exists \bar v\, \varphi_1 \lor \exists \bar v\, \varphi_2\), each disjunct keeping the quantifiers of its variables. For instance, a negated predicate defined by two rules, \(N(s) \leftarrow F(s)\) and \(N(s) \leftarrow M(s, t)\), flattens to \(\lnot\exists t\, (F(s) \lor M(s, t))\), which is planned as \(\lnot F(s) \land \lnot\exists t\, M(s, t)\);

  • \(\exists \bar v\, \varphi\) is first split into the groups of conjuncts of \(\varphi\) connected by the variables of \(\bar v\), the other conjuncts being moved out of the quantifier. Each group is then projected on one of its variables \(v\) that occurs in every probabilistic atom of the group, including those within its negations: the events \(\varphi(a)\) for different values \(a\) concern different tuples, and the projection is independent, \(1 - \prod_a (1 - P[\varphi(a)])\). When a probabilistic choice conjunct of the group has \(v\), the events are mutually exclusive instead, and the projection is disjoint, \(\sum_a P[\varphi(a)]\). If no variable of the group occurs in all of its probabilistic atoms, as in the #P-hard \(\exists x\, R(x) \land \lnot\exists y\, (S(x, y) \land T(y))\), or if another condition fails, such as a comparison or a negation whose variables are not bound by the rest of its conjunction, or a choice atom with the variable that is not a conjunct of the group, no plan is given and the query is left to Dalvi–Suciu lifting.

Deterministic relations do not count as repetitions, and do not need to have the projected variable.

In Datalog, the rules of a predicate share their head variables, so the negation of a predicate defined by several rules always has disjuncts with the same free variables once the quantifiers are pushed into them; disjuncts with different free variables only arise in queries built with the Python API.

Dalvi–Suciu lifting#

dalvi_suciu_lift() implements the algorithm of Dalvi and Suciu for unions of conjunctive queries [Dalvi2012], extended to probabilistic choices [Suciu2011]. Its rules are tried in the order below, each one calling the algorithm on the subqueries it produces. A query to which no rule applies is marked NonLiftable and declined. Dalvi and Suciu prove their algorithm complete for unions of conjunctive queries on tuple-independent databases: a query on which it fails is #P-hard [Dalvi2012]. The implementation restricts some of its rules, inclusion–exclusion for instance, so a query it declines is not necessarily #P-hard.

Base cases

A single atom is read from its relation; a subquery whose atoms are all deterministic is computed by ordinary relational algebra, with probability 1.

Minimisation

Redundant atoms and disjuncts are removed with the containment test of neurolang.probabilistic.containment, and the base cases are tried again.

Independent conjunction

With the query in conjunctive normal form, if its conjuncts split into components with no probabilistic relation in common, they are independent:

\[P[Q_1 \land Q_2] = P[Q_1]\,P[Q_2], \qquad P[Q_1 \land \lnot Q_2] = P[Q_1]\,(1 - P[Q_2]).\]

Negated components sharing no relation with the rest are planned this way, with Difference: the query is liftable when its positive and negated parts are (see Correctness of the plans). Fink and Olteanu study the converse, for queries with negation without repeated relations [Fink2014] [Fink2016].

Independent disjunction

With the query in disjunctive normal form, if its disjuncts split into components with no probabilistic relation in common:

\[P[Q_1 \lor Q_2] = 1 - (1 - P[Q_1])(1 - P[Q_2]).\]
Separator variable

A variable \(z\) is a separator variable of \(\exists z\,Q(z)\) if it occurs in every atom and, for each relation, in the same position of all of its atoms. The events \(Q(a)\) for different values \(a\) then concern different tuples and are independent:

\[P[\exists z\, Q(z)] = 1 - \prod_a (1 - P[Q(a)]).\]

The dual rule, for a universally quantified separator variable, gives \(\prod_a P[Q(a)]\) [Suciu2020].

Disjoint projection

If an atom of a probabilistic choice, or of a tuple-independent relation with constants in all its positions, occurs in a conjunctive query, the values of the projected variables give mutually exclusive events whose probabilities add up [Suciu2011] (section 4.3.1). For a union of conjunctive queries, the disjuncts with such an atom are separated with \(P[A \lor B] = P[A] + P[B] - P[A \land B]\).

Inclusion–exclusion

For a conjunction \(Q_1 \land \dots \land Q_n\) in conjunctive normal form,

\[P\Big[\bigwedge_{i} Q_i\Big] = \sum_{\emptyset \neq S \subseteq \{1..n\}} (-1)^{|S|+1}\, P\Big[\bigvee_{i \in S} Q_i\Big].\]

Terms whose disjunctions are equivalent are merged and their coefficients added, using the Möbius function of the lattice of the disjunctions ordered by containment [Dalvi2012]. This cancellation removes the terms that may be #P-hard while their sum is not. The rule is applied only when all the conjuncts have the same free variables, for which the containment test is sound.

Negations and comparisons sharing relations#

lift_with_dependent_negations() extends the algorithm to conjunctions \(A \land \lnot N\) in which the negated conjunct \(N\) shares probabilistic relations with \(A\), and to existential conjuncts with comparisons such as \(t \neq x\). Such conjunctions fall outside unions of conjunctive queries, so the completeness result above does not apply to them. The rules below are tried in turn when the relations shared are tuple-independent; a conjunction sharing a probabilistic choice is declined. Every rule checks each query it lifts, and the lifted plans are sound (see Correctness of the plans), but the rules are not known to be complete: some liftable conjunctions of this kind may still be declined and left to weighted model counting. These rules are NeuroLang’s own: the references they cite give the techniques they build on, not their correctness, which is proved below.

Comparisons in an existential conjunct

For \(A \land \exists t\,(\psi(t) \land C)\), or its negation, where \(C\) is a conjunction of comparisons between \(t\), the free variables and constants, e.g. \(P(x, y) \land \lnot\exists w\,(P(w, y) \land w \neq x)\). Following Olteanu and Huang [Olteanu2009], with \(L\) the plan of \(A\), the event \(E = \exists t\,(\psi(t) \land C)\) is computed as

\[E = \text{ind-}\pi\;\sigma_C\big(\mathrm{lift}(\psi(t)) \bowtie \mathrm{support}(L)\big)\]

and the plan is \(L \bowtie E\), or \(\mathrm{Difference}(L, E)\) when negated. It applies when \(t\) is a separator variable of \(\psi\), and when each probabilistic atom of \(\psi(t)\) has \(t\) in a position where the atoms of the same relation in \(A\) have a term that \(C\) makes different from \(t\), so that \(E\) and \(A\) concern different tuples.

Free-variable shattering

For \(A \land \lnot\exists t\,\psi(t)\) where the shared atoms have a free variable \(x\) of \(A\) in the position of \(t\), such as \(R(x) \land \lnot\exists t\,(R(t) \land S(x, t))\). Splitting the existential on \(t = x\) and \(t \neq x\), as shattering does [Dalvi2012],

\[\exists t\,\psi(t) \equiv \psi(x) \lor \exists t\,(t \neq x \land \psi(t)),\]

gives the plan, with \(L = \mathrm{lift}(A \land \lnot\psi(x))\),

\[\mathrm{Difference}\Big(L,\ \text{ind-}\pi\;\sigma_{t \neq x} \big(\mathrm{lift}(\psi(t)) \bowtie \mathrm{support}(L)\big)\Big).\]

It applies when \(t\) is a separator variable of \(\psi\), and when, for \(t \neq x\), each probabilistic atom of \(\psi(t)\) is a different tuple from the atoms of the same relation in \(A\) and \(\psi(x)\), the second part being then independent of \(L\).

Negation by subtraction

For any \(A \land \lnot N\), as \(A \land N\) implies \(A\),

\[P[A \land \lnot N] = P[A] - P[A \land N],\]

computed with Subtraction when both \(A\) and \(A \land N\) are liftable.

Existential shattering

For a positive existential conjunct \(A \land \exists t\,\psi(t)\) sharing relations with \(A\), which Dalvi–Suciu lifting declines,

\[P[A \land \exists t\,\psi(t)] = P[A] - P[A \land \lnot\exists t\, \psi(t)],\]

the latter being planned by free-variable shattering.

Projection on a choice or a separator variable

When the rules above decline \(\exists X\, \varphi\), it is planned by projecting the plan of \(\varphi\), lifted with all the rules of this page, on variables of \(X\) made free (projection_plan()). The quantifiers of the conjuncts of the query are first gathered, \(A \land \exists X\, \psi \equiv \exists X\, (A \land \psi)\), which holds as the query is standardised apart: a closed conjunct, such as an atom added by magic sets, does not prevent the projection. The projection is

  • disjointly, when a conjunct of \(\varphi\) is an atom \(C(\bar u)\) of a probabilistic choice \(C\) with variables \(X'\) of \(X\), and \(C\) occurs nowhere else:

    \[P[\exists X\, (C(\bar u) \land \varphi')] = \sum_a P[(C(\bar u) \land \exists (X - X')\, \varphi')[a/X']];\]
  • independently, when the conjuncts \(\psi\) of \(\varphi\) with variables of \(X\) share no probabilistic relation with the others, \(A\), and a variable \(v\) of \(X\) is in all the probabilistic atoms of \(\psi\), within its negations and existentials too, at a common position for any two atoms of a relation:

    \[P[\exists X\, (A \land \psi)] = P[A]\, \Big(1 - \prod_a \big(1 - P[(\exists (X - \{v\})\, \psi)[a/v]]\big)\Big).\]

For instance, the segregation of a term on the selected study,

\[\exists s\, \mathrm{mentions}(s, t) \land \mathrm{selected}(s) \land \lnot\exists s_2\, (\mathrm{mentions}(s_2, t) \land s_2 \neq s),\]

is the disjoint projection on \(s\) of a query that the comparison rule lifts once \(s\) is free; with \(t\) projected too, an independent projection on \(t\) follows. A body that is a union, of which the choice is not a conjunct of every disjunct, and block-independent disjoint relations other than choices, are not covered. The global checks of a single kind of quantifier and of unateness are skipped for a query of the first form, and applied to each query lifted.

Correctness of the plans#

A rule is liftable when its plan computes the exact probability of the query (soundness) in time polynomial in the size of the data, the query being fixed (data complexity). This section proves both for the rules of this page which are not covered by a cited theorem. Completeness, that every tractable query is lifted, is not claimed for them.

The probabilistic model

A tuple-independent relation has a Boolean random variable per tuple, these variables being independent. A probabilistic choice has one random variable whose value is the single tuple of the relation which is true. The variables of different relations are independent, and a possible world is a value for all of them. Deterministic relations are the same in every world.

For a formula \(\varphi\) and a tuple \(\theta\) of values for its free variables, the event \(\varphi\theta\) is the set of worlds in which it holds. It is determined by the random variables of the tuples \(R(\bar a)\) such that an atom of \(\varphi\theta\) can be \(R(\bar a)\) for some values of its quantified variables: these are its tuples. A plan computes, for every \(\theta\) in its support, \(P[\varphi\theta]\), and \(P[\varphi\theta] = 0\) outside it.

The rules identify the variables by their names, so the quantified variables are first renamed to fresh ones (standardise_apart(), applied by solve_succ_query()): no substitution is captured and no atom has a variable on which it does not depend.

Lemma 1 (independence)

If no two events of a family \(E_1, \dots, E_n\) have a tuple of a tuple-independent relation in common, nor both have tuples of the same probabilistic choice, the events are mutually independent: they are determined by pairwise disjoint sets of independent random variables. Formulas without a common probabilistic relation satisfy this.

Lemma 2 (exclusivity)

If \(E_1\) implies that the tuple \(C(\bar a)\) of a probabilistic choice \(C\) is true, and \(E_2\) that the tuple \(C(\bar b)\) is, with \(\bar a \neq \bar b\), then \(E_1 \land E_2\) is impossible, as a single tuple of \(C\) is true.

Polynomial time

Each operation of the plans (Operations of the lifted plans) is computed in time polynomial in the size of its inputs: joins, selections, left joins for Difference and Subtraction, and grouped products or sums for the projections. A plan is built from the query alone, so its size does not depend on the data, and it is computed in polynomial time if the construction terminates.

The rules of Negations and comparisons sharing relations call each other through the queries they lift. Each call is on a query that is smaller for the lexicographic order on (number of quantifiers, number of negations, size): negation by subtraction lifts \(A\), a part of \(A \land \lnot N\), and \(A \land N\), which has one negation less; free-variable shattering lifts \(A \land \lnot\psi(x)\) and \(\psi(t)\), with one quantifier less than \(A \land \lnot\exists t\, \psi(t)\); existential shattering lifts \(A\) and the queries of free-variable shattering; the comparison rule lifts \(A\) and \(\psi(t)\), parts of the query; the projections lift a body with at least one quantifier less, and a part of the query. The Dalvi–Suciu rules, whose recursion terminates [Dalvi2012], do not call the rules of this section. The order being well founded, the construction terminates.

Absorption in negations

In every world, for every \(\theta\): if \(A\theta\) holds, \(\lnot(A \land B)\theta\) and \(\lnot B\theta\) agree; otherwise both sides of \(A \land \lnot(A \land B) \equiv A \land \lnot B\) are false. When \(y\) is not free in \(A\), \(\exists y\, (A \land B) \equiv A \land \exists y\, B\), which gives the rule through existentials. A conjunct is removed from a negation only if it is one of the conjuncts asserted outside it and no variable quantified between the negation and it is free in it (_without_asserted_conjuncts), so that its variables are the same inside and outside. A negation whose conjuncts would all be removed is left unchanged. The rewriting is done once, before lifting.

Contradicting disjuncts

A disjunct \(\exists \bar y\,(C \land \lnot A)\) is false in every world and for every \(\theta\) where \(A\theta\) holds, provided no variable of \(\bar y\) is free in \(A\), so that \(A\) has the same variables inside the disjunct and outside it (_is_contradiction). If \(A\) is a conjunct of the disjunct, the disjunct is false in every world. If \(A\) is asserted by the conjunction \(A \land (B \lor D)\), then where \(A\theta\) holds \((B \lor D)\theta \equiv B\theta\), and where it does not both sides are false. Removing a false disjunct preserves the probability of every answer. A disjunction left with a single disjunct is replaced by it, and nested conjunctions are flattened, both equivalences. Every rewriting removes a disjunct or a nested conjunction, so it terminates. The rewriting is done once, before lifting, together with absorption in negations.

Deterministic negations

The atoms of \(N\) are deterministic relations or comparisons (_is_deterministic, the extensional database of a CPLogicProgram excluding its probabilistic relations), so \(N\), and the relation of \(D = G \land \lnot N\), defined by its relational algebra expression, are the same in every world. \(G\) being asserted by the conjunction, \(G \land \lnot N \equiv G \land D\) in every world. \(G\) binds every free variable of \(N\) (_can_replace), so \(D\) is finite. \(G\) is conjoined within the existentials of \(N\), whose variables are not free in \(G\): \(\lnot\exists t\, N \equiv \lnot\exists t\, (G \land N)\) given \(G\), by absorption. \(D\) is computed when the plan is, as one of its subexpressions, in time polynomial in the deterministic relations.

Independent negation

For \(A \land \lnot N\) where \(N\) shares no probabilistic relation with \(A\) and its free variables are among those of \(A\), which the range restriction of the rules, checked when they are declared (check_range_restriction()), ensures, Lemma 1 gives, for every \(\theta\), \(P[(A \land \lnot N)\theta] = P[A\theta]\,(1 - P[N\theta])\), which Difference computes, a tuple of \(A\) absent from the plan of \(N\) having \(P[N\theta] = 0\). The query is thus liftable when \(A\) and \(N\) are.

Negation by subtraction

\(A\theta\) is the disjoint union of \((A \land N)\theta\) and \((A \land \lnot N)\theta\), so \(P[(A \land \lnot N)\theta] = P[A\theta] - P[(A \land N)\theta]\) for any events. The free variables of \(N\) being among those of \(A\) (_split_dependent_conjunct), the plan of \(A \land N\) has the columns of the plan of \(A\), and Subtraction computes this difference tuple by tuple. Existential shattering is the same identity, with \(\exists t\, \psi(t)\) for \(N\).

Free-variable shattering

Splitting on \(t = x\), \(\exists t\, \psi(t) \equiv \psi(x) \lor E\) with \(E = \exists t\, (t \neq x \land \psi(t))\), so \(A \land \lnot\exists t\, \psi(t) \equiv L \land \lnot E\) with \(L = A \land \lnot\psi(x)\). The rule checks that

  • \(t\) is a separator variable of \(\psi\) (_is_separator_variable): every probabilistic atom of \(\psi\) has \(t\), and any two atoms of the same relation have \(t\) at a common position (find_separator_variables). A tuple of \(\psi(a)\) through one of them and a tuple of \(\psi(b)\) through the other have \(a\) and \(b\) at that position, so they differ when \(a \neq b\). A separator variable cannot be a variable of a probabilistic choice atom (extract_probabilistic_root_variables), so \(\psi\) has no such atom, and the relations shared with \(A\) are tuple-independent (_shares_a_choice_relation). By Lemma 1, the events \(\psi(a)\theta\) being mutually independent, \(P[E\theta] = 1 - \prod_{a \neq x\theta} (1 - P[\psi(a)\theta])\), which the independent projection of the plan computes, support(L) giving the value of \(x\);

  • for \(t \neq x\), each probabilistic atom of \(\psi(t)\) has \(t\) at a position where each atom of the same relation in \(A\) and \(\psi(x)\) has \(x\) (_are_different_tuples_when_different): the tuples of \(E\theta\) are not tuples of \(L\theta\), and by Lemma 1 \(P[(L \land \lnot E)\theta] = P[L\theta]\,(1 - P[E\theta])\), which Difference computes.

Comparisons in an existential conjunct

With \(E = \exists t\, (\psi(t) \land C)\), the rule checks that \(t\) is a separator variable of \(\psi\), which as above gives \(P[E\theta] = 1 - \prod_{a : C\theta(a)} (1 - P[\psi(a)\theta])\), computed by selecting \(C\) before the independent projection; and that each probabilistic atom of \(\psi(t)\) has \(t\) at a position where each atom of the same relation in \(A\) has a term \(u\) with \(t \neq u\), \(t < u\) or \(t > u\) in \(C\) (_terms_different_from, STRICT_COMPARISONS). When \(C\theta(a)\) holds, the tuples of \(\psi(a)\theta\) are thus not tuples of \(A\theta\), and by Lemma 1 \(P[(A \land E)\theta] = P[A\theta]\,P[E\theta]\) and \(P[(A \land \lnot E)\theta] = P[A\theta]\,(1 - P[E\theta])\), which the join and Difference compute. Olteanu and Huang [Olteanu2009] compute conjunctive queries with inequalities without self-joins on tuple-independent databases; this rule uses the inequalities instead to show that the tuples of a relation occurring in both \(A\) and \(\psi\) differ, which their result does not cover.

Non-repeating queries

non_repeating_plan() applies only if no probabilistic relation, fact or choice, occurs twice in the query (_is_non_repeating), the occurrences of an atom being counted: \(R(x) \land \lnot R(x)\) has two occurrences of \(R\), which are not independent. Its rewrites add no atom, so this holds for every subformula planned, and by Lemma 1 two subformulas without a common atom are independent. Then:

  • rewrites, by NormaliseNonRepeatingQuery: \(\exists v\, (v = e \land \varphi) \equiv \varphi[e/v]\) when no variable of \(e\) is captured, which UnifyExistentialVariableEqualitiesMixin checks with ExtractBoundVariables after the query is standardised apart; \(\lnot(A \lor B) \equiv \lnot A \land \lnot B\) (MoveNegationsIntoDisjunctionsMixin); \(\exists v\, (A \lor B) \equiv \exists v\, A \lor \exists v\, B\) (PushExistentialsDownDisjunctionsMixin); and, by the planner, \(\exists \bar v\, (A \land B) \equiv \exists \bar v_A\, A \land \exists \bar v_B\, B\) when \(A\) and \(B\) share no variable of \(\bar v\) (_connected_groups). These hold in every world;

  • conjunction: the join of independent positive conjuncts is the product of their probabilities; a comparison, deterministic, is a selection; for a negation whose free variables are bound by the positive conjuncts (checked in _conjunction_plan), Difference computes \(P[A\theta]\,(1 - P[N\theta])\) as for an independent negation above. Atoms with constants or repeated variables are selected on named columns (NonRepeatingPlanner.atom);

  • disjunction: its disjuncts have the same free variables (checked in NonRepeatingPlanner.disjunction) and are independent, so \(P[(A \lor B)\theta] = 1 - (1 - P[A\theta])(1 - P[B\theta])\);

  • projection: the variable \(v\) occurs in every probabilistic atom of the group \(\varphi\), including those within its negations and existentials (_root_variable); the query being standardised apart, these atoms depend on \(v\). Each relation occurring once, its atom has \(v\) at some position \(i\), so for \(a \neq b\) the tuples of \(\varphi(a)\theta\) and \(\varphi(b)\theta\) of that relation differ at \(i\). If no probabilistic choice atom has \(v\) (_projection), there is no choice atom in \(\varphi\), and by Lemma 1 the events \(\varphi(a)\theta\) are mutually independent: \(P[\exists v\, \varphi\theta] = 1 - \prod_a (1 - P[\varphi(a)\theta])\). If a conjunct of \(\varphi\) is an atom of a choice \(C\) with \(v\), \(\varphi(a)\theta\) and \(\varphi(b)\theta\) imply different tuples of \(C\), and by Lemma 2 they are mutually exclusive: \(P[\exists v\, \varphi\theta] = \sum_a P[\varphi(a)\theta]\). Otherwise no plan is given;

  • deterministic relations are the same in every world, so they neither count as repetitions nor need to have \(v\).

Each recursive call is on a smaller formula: a part of a conjunction, negation or disjunction, or a group with one quantifier less. Pushing \(\exists \bar v\) into a disjunction copies the quantifiers into every disjunct, but the disjuncts are planned one by one, and each \(\exists \bar v\, \varphi_i\) is smaller than \(\exists \bar v\, (\varphi_1 \lor \dots \lor \varphi_n)\). The rewrites remove equalities and negations of disjunctions without adding atoms. The plan is thus built from the query alone, and computed in polynomial time in the data.

Projection on a choice or a separator variable

Disjoint projection. The atom \(C(\bar u)\) is a conjunct of the body (_split_choice_projection), so for two values \(a \neq b\) of \(X'\) the events imply the different tuples \(C(\bar u)[a/X']\) and \(C(\bar u)[b/X']\) of \(C\), and are mutually exclusive by Lemma 2: their probabilities add up, which DisjointProjection computes. \(C\) occurring nowhere else in the body (the same check), \(C(\bar u)\) is independent of the rest of the body by Lemma 1, as the plan of the body, lifted with every rule, assumes.

Independent projection. Every probabilistic atom of \(\psi\) has \(v\), and any two atoms of a relation have it at a common position (_separates); the query being standardised apart, these atoms depend on \(v\). For \(a \neq b\), the tuples of \(\psi[a/v]\) and \(\psi[b/v]\) thus differ at that position, and none is of a probabilistic choice (also checked): the events are mutually independent by Lemma 1, and their disjunction has the probability that IndependentProjection computes. \(A\) sharing no probabilistic relation with \(\psi\) (_split_separator_projection), the join with its plan is a product by Lemma 1.

Dalvi–Suciu rules

The rules of Dalvi–Suciu lifting are those of Dalvi and Suciu [Dalvi2012], whose proofs apply to unions of conjunctive queries on tuple-independent databases, and of Suciu et al. [Suciu2011] (section 4.3.1) for the disjoint projection on probabilistic choices.

Ranking

Dalvi and Suciu prove the ranked query equivalent to the query, and its relations to be tuple-independent, by mapping each tuple of a relation to a single tuple of a single ranked relation [Dalvi2012] (Proposition 4.2). rank_query keeps what the proof needs:

  • every atom of a relation has variables to rank at the same positions (_ranked_variables_and_positions closes the set of variables to rank), so the ranked relations of \(R\) partition its tuples by the order of their values at these positions, and keep their probabilities: a tuple-independent relation gives tuple-independent relations;

  • a probabilistic choice, a single block of exclusive tuples, is not split: its parts would not be independent choices;

  • the atoms split are positive: each disjunct then implies the query, even when no atom forces its order, while a negated \(\lnot R_<(x, y)\) would hold whenever \(x > y\);

  • the order compared is total, with equality: real numbers or strings (_is_totally_ordered), without NaN. Sets, ordered by inclusion, would leave the tuples of incomparable values in no ranked relation.

The tests of the rules of Negations and comparisons sharing relations (neurolang/probabilistic/tests/test_lifted_negation.py) also compare their plans with an enumeration of the possible worlds of small databases.

References#

[Chavira2008]

M. Chavira and A. Darwiche. On probabilistic inference by weighted model counting. Artificial Intelligence, 172(6–7), 772–799, 2008.

[Dalvi2007]

N. Dalvi and D. Suciu. Efficient query evaluation on probabilistic databases. The VLDB Journal, 16(4), 523–544, 2007.

[Dalvi2012] (1,2,3,4,5,6,7,8,9)

N. Dalvi and D. Suciu. The dichotomy of probabilistic inference for unions of conjunctive queries. Journal of the ACM, 59(6), 1–87, 2012.

[Darwiche2011]

A. Darwiche. SDD: A new canonical representation of propositional knowledge bases. In Proceedings of the 22nd International Joint Conference on Artificial Intelligence (IJCAI), 819–826, 2011.

[Fink2014] (1,2,3)

R. Fink and D. Olteanu. A dichotomy for non-repeating queries with negation in probabilistic databases. In Proceedings of the 33rd ACM SIGMOD-SIGACT-SIGART Symposium on Principles of Database Systems (PODS), 144–155, 2014.

[Fink2016] (1,2)

R. Fink and D. Olteanu. Dichotomies for queries with negation in probabilistic databases. ACM Transactions on Database Systems, 41(1), 1–47, 2016.

[Olteanu2009] (1,2)

D. Olteanu and J. Huang. Secondary-storage confidence computation for conjunctive queries with inequalities. In Proceedings of the 2009 ACM SIGMOD International Conference on Management of Data, 389–402, 2009.

[Suciu2011] (1,2,3,4)

D. Suciu, D. Olteanu, C. Ré and C. Koch. Probabilistic Databases. Synthesis Lectures on Data Management. Morgan & Claypool, 2011.

[Suciu2020]

D. Suciu. Probabilistic databases for all. In Proceedings of the 39th ACM SIGMOD-SIGACT-SIGAI Symposium on Principles of Database Systems (PODS), 19–31, 2020.

[Vennekens2009]

J. Vennekens, M. Denecker and M. Bruynooghe. CP-logic: A language of causal probabilistic events and its relation to logic programming. Theory and Practice of Logic Programming, 9(3), 245–308, 2009.

[Zanitti2023] is listed in SQUALL: Controlled English for NeuroLang.