Foundations of Declarative Data Analysis Using Limit Datalog Programs

1 Introduction

Analysing complex datasets is currently a hot topic in information systems. The term 'data analysis' covers a broad range of techniques that often involve tasks such as data aggregation, property verification, or query answering. Such tasks are currently often solved imperatively (e.g., using Java or Scala) by specifying how to manipulate the data, and this is undesirable because the objective of the analysis is often obscured by evaluation concerns. It has recently been argued that data analysis should be declarative [Alvaro et al., 2010; Markl, 2014; Seo et al., 2015; Shkapsky et al., 2016]: users should describe what the desired output is, rather than how to compute it. For example, instead of computing shortest paths in a graph by a concrete algorithm, one should (i) describe what a path length is, and (ii) select only paths of minimum length. Such a specification is independent of evaluation details, allowing analysts to focus on the task at hand. An evaluation strategy can be chosen later, and general parallel and/or incremental evaluation algorithms can be reused 'for free'.

An essential ingredient of declarative data analysis is an efficient language that can capture the relevant tasks, and Datalog is a prime candidate since it supports recursion. Apart from recursion, however, data analysis usually also requires integer arithmetic to capture quantitative aspects of data (e.g., the length of a shortest path). Research on combining the two dates back to the '90s [Mumick et al., 1990;

Kemp and Stuckey, 1991; Beeri et al., 1991; Van Gelder, 1992; Consens and Mendelzon, 1993; Ganguly et al., 1995; Ross and Sagiv, 1997], and is currently experiencing a revival [Faber et al., 2011; Mazuran et al., 2013]. This extensive body of work, however, focuses primarily on integrating recursion and arithmetic with aggregate functions in a coherent semantic framework, where technical difficulties arise due to nonmonotonicity of aggregates. Surprisingly little is known about the computational properties of integrating recursion with arithmetic, apart from that a straightforward combination is undecidable [Dantsin et al., 2001]. Undecidability also carries over to the above formalisms and practical Datalogbased systems such as BOOM [Alvaro et al., 2010], DeALS [Shkapsky et al., 2016], Myria [Wang et al., 2015], SociaLite [Seo et al., 2015], Overlog [Loo et al., 2009], Dyna [Eisner and Filardo, 2011], and Yedalog [Chin et al., 2015].

To develop a sound foundation for Datalog-based declarative data analysis, we study DatalogZ-negation-free Datalog with integer arithmetic and comparisons. Our main contribution is a new limit DatalogZ fragment that, like the existing data analysis languages, is powerful and flexible enough to naturally capture many important analysis tasks. However, unlike DatalogZ and the existing languages, reasoning with limit programs is decidable, and it becomes tractable in data complexity under an additional stability restriction.

In limit DatalogZ, all intensional predicates with a numeric argument are limit predicates. Instead of keeping all numeric values for a given tuple of objects, such predicates keep only the minimal (min) or only the maximal (max) bounds of numeric values entailed for the tuple. For example, if we encode a weighted directed graph using a ternary predicate edge, then rules (1) and (2), where sp is a min limit predicate, compute the cost of a shortest path from a given source node v0 to every other node.

If these rules and a dataset entail a fact sp(v, k), then the cost of a shortest path from v0 to v is at most k; hence, sp(v, k′ ) holds for each k′ ≥ k since the cost of a shortest path is also at most k′ . Rule (2) intuitively says that, if x is reachable from v0 with cost at most m and 〈x, y〉 is an edge of cost n, then v′ is reachable from v0 with cost at most m+n. This is different from DatalogZ, where there is no implicit semantic connection between sp(v, k) and sp(v, k′ ), and such semantic connections allow us to prove decidability of limit DatalogZ. We provide a direct semantics for limit predicates based on Herbrand interpretations, but we also show that this semantics can be axiomatised in standard DatalogZ. Our formalism can thus be seen as a fragment of DatalogZ, from which it inherits well-understood properties such as monotonicity and existence of a least fixpoint model [Dantsin et al., 2001].

Our contributions are as follows. First, we introduce limit DatalogZ programs and argue that they can naturally capture many relevant data analysis tasks. We prove that fact entailment in limit DatalogZ is undecidable, but, after restricting the use of multiplication, it becomes CONEXPTIME- and CONP-complete in combined and data complexity, respectively. To achieve tractability in data complexity (which is very important for robust behaviour on large datasets), we additionally introduce a stability restriction and show that this does not prevent expressing the relevant analysis tasks.

The proofs of all results are given in an extended version of this paper [Kaminski et al., 2017].

2 Preliminaries

In this section, we recapitulate the well-known definitions of Datalog with integers, which we call DatalogZ.

Syntax A vocabulary consists of predicates, objects, object variables, and numeric variables. Each predicate has an integer arity n, and each position 1 ≤ i ≤ n is of either object or numeric sort. An object term is an object or an object variable. A numeric term is an integer, a numeric variable, or of the form s1 + s2, s1 - s2, or s1 × s2 where s1 and s2 are numeric terms, and +, -, and × are the standard arithmetic functions. A constant is an object or an integer. The magnitude of an integer is its absolute value. A standard atom is of the form B(t1, . . . , tn), where B is a predicate of arity n and each ti is a term whose type matches the sort of position i of B. A comparison atom is of the form (s1 < s2) or (s1 ≤ s2), where < and ≤ are the standard comparison predicates, and s1 and s2 are numeric terms. A rule r is of the form ∧i αi ∧ ∧j βj → α, where α(i) are standard atoms, βj are comparison atoms, and each variable in r occurs in some αi. Atom h(r) = α is the head of r; sb(r) = ∧i αi is the standard body of r; cb(r) = ∧j βj is the comparison body of r; and b(r) = sb(r) ∧ cb(r) is the body of r. A ground instance of r is obtained from r by substituting all variables by constants. A (DatalogZ) program P is a finite set of rules. Predicate B is intensional (IDB) in P if B occurs in P in the head of a rule whose body is not empty; otherwise, B is extensional (EDB) in P. A term, atom, rule, or program is ground if it contains no variables. A fact is a ground, function-free, standard atom. Program P is a dataset if h(r) is a fact and b(r) = ∅ for each r ∈ P. We often say that P contains a fact α and write α ∈ P, which actually means → α ∈ P. We write a tuple of terms as t, and we often treat conjunctions and tuples as sets and write, say, αi ∈ sb(r), |t|, and ti ∈ t.

Semantics A (Herbrand) interpretation I is a (not necessarily finite) set of facts. Such I satisfies a ground atom α, written I |= α, if (i) α is a standard atom and evaluating the arithmetic functions in α produces a fact in I, or (ii) α is a comparison atom and evaluating the arithmetic functions and comparisons produces true. The notion of satisfaction is extended to conjunctions of ground atoms, rules, and programs as in first-order logic, where each rule is universally quantified. If I |= P, then I is a model of programP; and P entails a fact α, written P |= α, if I |= α holds whenever I |= P.

Complexity In this paper we study the computational properties of checking P |= α. Combined complexity assumes that both P and α are part of the input. In contrast, data complexity assumes that P is given as P ′ ∪D for P ′ a program and D a dataset, and that only D and α are part of the input while P ′ is fixed. Unless otherwise stated, all numbers in the input are coded in binary, and the size ‖P‖ of P is the size of its representation. Checking P |= α is undecidable even if the only arithmetic function in P is + [Dantsin et al., 2001].

Presburger arithmetic is first-order logic with constants 0 and 1, functions + and -, equality, and the comparison predicates < and ≤, interpreted over all integers Z. The complexity of checking sentence validity (i.e., whether the sentence is true in all models of Presburger arithmetic) is known when the number of quantifier alternations and/or the number of variables in each quantifier block are fixed [Berman, 1980; Gr¨adel, 1988; Sch¨oning, 1997; Haase, 2014].

3 Limit Programs

Towards introducing a decidable fragment of DatalogZ for data analysis, we first note that the undecidability proof of (plain) DatalogZ outlined by Dantsin et al. [2001] uses atoms with at least two numeric terms. Thus, to motivate introducing our fragment, we first prove that undecidability holds even if atoms contain at most one numeric term. The proof uses a reduction from the halting problem for deterministic Turing machines. To ensure that each standard atom in P has at most one numeric term, combinations of a time point and a tape position are encoded using a single integer.

Theorem 1. For P a DatalogZ program and α a fact, checking P |= α is undecidable even if P contains no × or - and each standard atom in P has at most one numeric term.

We next introduce limit DatalogZ, where limit predicates keep bounds on numeric values. This language can be seen as either a semantic or a syntactic restriction of DatalogZ.

Definition 2. In limit DatalogZ, a predicate is either an object predicate with no numeric positions, or a numeric predicate where only the last position is numeric. A numeric predicate is either an ordinary numeric predicate or a limit predicate, and the latter is either a min or a max predicate. Atoms with object predicates are object atoms, and analogously for other types of atoms/predicates. A DatalogZ rule r is a limit (DatalogZ) rule if (i) b(r) = ∅, or (ii) each atom in sb(r) is an object, ordinary numeric, or limit atom, and h(r) is an object or a limit atom. A limit (DatalogZ) program P is a program containing only limit rules; and P is homogeneous if it does not contain both min and max predicates.

In the rest of this paper we make three simplifying assumptions. First, numeric atoms occurring in a rule body are function-free (but comparison atoms and the head can contain arithmetic functions). Second, each numeric variable in a rule occurs in at most one standard body atom. Third, distinct rules in a program use different variables. The third assumption is clearly w.l.o.g. because all variables are universally quantified so their names are immaterial. Moreover, the first two assumptions are w.l.o.g. as well since, for each rule, there exists a logically equivalent rule that satisfies these assumptions. In particular, we can replace an atom such as A(t, m1 + m2) with conjunction

where m is a fresh variable and I is a fresh predicate axiomatised to hold on all integers as follows:

Also, we can replace atoms A1(t1, m) ∧ A2(t2, m) with conjunction A1(t1,m) ∧A2(t2,m′ ) ∧ (m≤m′ ) ∧ (m′ ≤m), where m′ is a fresh variable.

Intuitively, a limit fact B(a, k) says that the value of B for a tuple of objects a is at least k (if B is max) or at most k (if B is min). For example, a fact sp(v, k) in our shortest path example from Section 1 says that node v is reachable from v0 via a path with cost at most k. To capture this intended meaning, we require interpretations I to be closed for limit predicates-that is, whenever I contains a limit fact α, it also contains all facts implied by α according to the predicate type. In our example, this captures the observation that the existence of a path from v0 to v of cost at most k implies the existence of such a path of cost at most k′ for each k′ ≥ k.

Definition 3. An interpretation I is limit-closed if, for each limit fact B(a, k) ∈ I where B is a min (resp. max) predicate, B(a, k′ ) ∈ I holds for each integer k′ with k ≤ k′ (resp. k′ ≤ k). An interpretation I is a model of a limit program P if I |= P and I is limit-closed. The notion of entailment is modified to take into account only limit-closed models.

The semantics of limit predicates in a limit DatalogZ program P can be axiomatised explicitly by extending P with the following rules, where Z is a fresh predicate. Thus, limit DatalogZ can be seen as a syntactic fragment of DatalogZ.

for each max predicate B in P

Each limit program can be reduced to a homogeneous program; however, for the sake of generality, in our technical results we do not require programs to be homogeneous.

Proposition 4. For each limit program P and fact α, a homogeneous program P ′ and fact α′ can be computed in linear time such that P |= α if and only if P ′ |= α′ .

Intuitively, program P ′ in Proposition 4 is obtained by replacing all min (or all max) predicates in P by fresh max (resp. min) predicates and negating their numeric arguments.

In Section 1 we have shown that limit DatalogZ can compute the cost of shortest paths in a graph. We next present further examples of data analysis tasks that our formalism can handle. In all examples, we assume that all objects in the input are arranged in an arbitrary linear order using facts first(a1), next(a1, a2), . . . , next(an-1, an); we use this order to simulate aggregation by means of recursion.

Example 5. Consider a social network where agents are connected by the 'follows' relation. Agent as introduces (tweets) a message, and each agent ai retweets the message if at least kai agents that ai follows tweet the message, where kai is a positive threshold uniquely associated with ai. Our goal is to determine which agents tweet the message eventually. To achieve this using limit DatalogZ, we encode the network structure in a dataset Dtw containing facts follows(ai, aj) if ai follows aj, and ordinary numeric facts th(ai, kai ) if ai's threshold is kai . Program Ptw, containing rules (3)-(8), encodes message propagation, where nt is a max predicate.

Specifically, Ptw ∪Dtw |= tw(ai) iff ai tweets the message. Intuitively, nt(ai, aj,m) is true if, out of agents {a1, . . . , aj} (according to the order), at least m agents that ai follows tweet the message. Rules (4) and (5) initialise nt for the first agent in the order; nt is a max predicate, so if the first agent tweets the message, rule (5) 'overrides' rule (4). Rules (6) and (7) recurse over the order to compute nt as stated above.

Example 6. Limit DatalogZ can also solve the problem of counting paths between pairs of nodes in a directed acyclic graph. We encode the graph in the obvious way as a dataset Dcp that uses object predicates node and edge. Program Pcp, consisting of rules (9)-(14) where np and np ′ are max predicates, then counts the paths.

Specifically, Pcp ∪Dcp |= np(ai, aj, k) iff at least k paths exist from node ai to node aj . Intuitively, np ′ (ai, aj , ak, m) is true if m is at least the sum of the number of paths from each a′ ∈ {a1, . . . , ak} (according to the order) to aj for which there exists an edge from ai to a′ . Rule (9) says that each node has one path to itself. Rule (10) initialises aggregation by saying that, for the first node z, there are zero paths from x to y, and rule (11) overrides this if there exists an edge from x to z. Finally, rule (12) propagates the sum for x to the next z in the order, and rule (13) overrides this if there is an edge from x to z by adding the number of paths from z′ and z to y.

Example 7. Assume that, in the graph from Example 6, each node ai is associated with a bandwidth bai limiting the number of paths going through ai to at most bai . To count the paths compliant with the bandwidth requirements, we extend Dcp to dataset Dbcp that additionally contains an ordinary numeric fact bw(ai, bai ) for each node ai, and we define Pbcp by replacing rule (14) in Pcp with the following rule.

Then, Pbcp ∪Dbcp |= np(ai, aj, k) iff there exist at least k paths from node ai to node aj, where the bandwidth requirement is satisfied for all nodes on each such path.

4 Fixpoint Characterisation of Entailment

Programs are often grounded to eliminate variables and thus simplify the presentation. In limit DatalogZ, however, numeric variables range over integers, so a grounding can be infinite. Thus, we first specialise the notion of a grounding.

Definition 8. A rule r is semi-ground if each variable in r is a numeric variable that occurs in r in a limit body atom. A limit program P is semi-ground if all of its rules are semi-ground. The semi-grounding of P contains, for each r ∈ P, each rule obtained from r by replacing each variable not occurring in r in a numeric argument of a limit atom with a constant of P.

Obviously, P |= α if and only if P ′ |= α for P ′ the semigrounding of P. We next characterise entailment of limit programs by pseudo-interpretations, which compactly represent limit-closed interpretations. If a limit-closed interpretation I contains B(b, k) where B is a min predicate, then either the limit value ℓ ≤ k exists such that B(b, ℓ) ∈ I and B(b, k′ ) ̸∈ I for k′ < ℓ, or B(b, k′ ) ∈ I holds for all k′ ≤ k, and dually for B a max predicate. Thus, to characterise the value of B on a tuple of objects b in I, we just need the limit value, or information that no such value exists.

Definition 9. A pseudo-interpretation J is a set of facts over integers extended with a special symbol ∞ such that k = k′ holds for all limit facts B(b, k) and B(b, k′ ) in I.

Limit-closed interpretations correspond naturally and oneto-one to pseudo-interpretations, so we can recast the notions of satisfaction and model using pseudo-interpretations. Unlike for interpretations, the number of facts in a pseudo-model of a semi-ground limit program P can be bounded by |P|.

Definition 10. A limit-closed interpretation I corresponds to a pseudo-interpretation J if I contains exactly all object and ordinary numeric facts of J, and, for each limit predicate B, each tuple of objects b, and each integer ℓ, (i) B(b, k) ∈ I for all k if and only if B(b,∞) ∈ J, and (ii) B(b, ℓ) ∈ I and B(b, k) ̸∈ I for all k < ℓ (resp. ℓ < k) and B is a min (resp. max) predicate if and only if B(b, ℓ) ∈ J.

Let J and J ′ be pseudo-interpretations corresponding to interpretations I and I ′ . Then, J satisfies a ground atom α, written J |= α, if I |= α; J is a pseudo-model of a program P, written J |= P, if I |= P; finally, J ⊑ J ′ holds if I ⊆ I ′ .

Example 11. Let I be the interpretation consisting of A(1), A(2), B(a, k) for k ≤ 5, and B(b, k) for k ∈ Z, where A is an ordinary numeric predicate, B is a max predicate, and a and b are objects. Then, {A(1),A(2),B(a, 5),B(b,∞)} is the pseudo-interpretation corresponding to I.

We next introduce the immediate consequence operator TP of a limit program P on pseudo-interpretations. We assume for simplicity that P is semi-ground. To apply a rule r ∈ P to a pseudo-interpretation J while correctly handling limit atoms, operator TP converts r into a linear integer constraint C(r, J) that captures all ground instances of r applicable to the limit-closed interpretation I corresponding to J. If C(r, J) has no solution, r is not applicable to J. Otherwise, h(r) is added to J if it is not a limit atom; and if h(r) is a min (max) atom B(b,m), then the minimal (maximal) solution ℓ for m in C(r, J) is computed, and J is updated such that the limit value of B on b is at least (at most) ℓ-that is, the application of r to J keeps only the 'best' limit value.

Definition 12. For P a semi-ground limit program, r ∈ P, and J a pseudo-interpretation, C(r, J) is the conjunction of comparison atoms containing (i) cb(r); (ii) (0 < 0) if an object or ordinary numeric atom α ∈ sb(r) exists with α ̸∈ J, or a limit atom B(b, s) ∈ sb(r) exists with B(b, ℓ) ̸∈ J for each ℓ; and (iii) (ℓ ≤ s) (resp. (s ≤ ℓ)) for each min (resp. max) atom B(b, s) ∈ sb(r) with B(b, ℓ) ∈ J and ℓ ̸=∞. Rule r is applicable to J if C(r, J) has an integer solution.

Assume r is applicable to J. If h(r) is an object or ordinary numeric atom, let hd(r, J) = h(r). If h(r) = B(b, s) is a min (resp. max) atom, the optimum value opt(r, J) is the smallest (resp. largest) value of s in all solutions to C(r, J), or ∞ if no such bound on the value of s in the solutions to C(r, J) exists; moreover, hd(r, J) = B(b, opt(r, J)).

Operator TP(J) maps J to the smallest (w.r.t. ⊑) pseudointerpretation satisfying hd(r, J) for each r ∈ P applicable to J. Finally, T0P = ∅, and TnP = TP(Tn-1 P ) for n > 0.

Example 13. Let r be A(x) ∧ (2 ≤ x) → B(x + 1) with A and B max predicates. Then, C(r, ∅) = (2 ≤ x) ∧ (0 < 0) does not have a solution, and therefore rule r is not applicable to the empty pseudo-interpretation. Moreover, for J = {A(3)}, conjunction C(r, J) = (2 ≤ x) ∧ (x ≤ 3) has two solutions-{x ↦→ 2} and {x ↦→ 3}-and therefore rule r is applicable to J. Finally, B is a max predicate, and so opt(r, J) =max{2+1, 3+1} = 4, and hd(r, J) = B(4). Consequently, T{r}(J) = {B(4)}.

Lemma 14. For each semi-ground limit programP, operator TP is monotonic w.r.t. ⊑. Moreover, J |= P if and only if TP(J) ⊑ J for each pseudo-interpretation J.

Monotonicity ensures existence of the closure T∞P of Pthe least pseudo-interpretation such that TnP ⊑ T∞P for each n ≥ 0. The following theorem characterises entailment and provides a bound on the number of facts in the closure.

Theorem 15. For P a semi-ground limit program and α a fact, P |= α if and only if T∞P |= α; also, |T∞P | ≤ |P|; and J |= P implies T∞P ⊑ J for each pseudo-interpretation J.

The proofs for the first and the third claim of Theorem 15 use the monotonicity of TP analogously to plain Datalog. The second claim holds since, for each n ≥ 0, each pair of distinct facts in TnP must be derived by distinct rules in P.

5 Decidability of Entailment: Limit-Linearity

We now start our investigation of the computational properties of limit DatalogZ. Theorem 15 bounds the cardinality of the closure of a semi-ground program, but it does not bound the magnitude of the integers occurring in limit facts; in fact, integers can be arbitrarily large. Moreover, due to multiplication, checking rule applicability requires solving nonlinear inequalities over integers, which is undecidable.

Theorem 16. For P a semi-ground limit program and α a fact, checking P |= α and checking applicability of a rule of P to a pseudo-interpretation are both undecidable.

The proof of Theorem 16 uses a straightforward reduction from Hilbert's tenth problem.

Checking rule applicability is undecidable due to products of variables in inequalities; however, for linear inequalities that prohibit multiplying variables, the problem can be solved in NP, and in polynomial time if we bound the number of variables. Thus, to ensure decidability, we next restrict limit programs so that their semi-groundings contain only linear numeric terms. All our examples satisfy this restriction.

Definition 17. A limit rule r is limit-linear if each numeric term in r is of the form s0 + ∑ni=1 si ×mi, where (i) each mi is a distinct numeric variable occurring in a limit body atom of r, (ii) term s0 contains no variable occurring in a limit body atom of r, and (iii) each si with i ≥ 1 is a term constructed using multiplication ×, integers, and variables not occurring in limit body atoms of r. A limit-linear program contains only limit-linear rules. 1

In the rest of this section, we show that entailment for limitlinear programs is decidable and provide tight complexity bounds. Our upper bounds are obtained via a reduction to the validity of Presburger formulas of a certain shape.

Lemma 18. For P a semi-ground limit-linear program and α a fact, there exists a Presburger sentence ϕ = ∀x∃y. ∨ni=1 ψi that is valid if and only if P |= α. Each ψi is a conjunction of possibly negated atoms. Moreover, |x| + |y| and each ‖ψi‖ are bounded polynomially by ‖P‖+‖α‖. Number n is bounded polynomially by |P| and exponentially by maxr∈P ‖r‖. Finally, the magnitude of each integer in ϕ is bounded by the maximal magnitude of an integer in P and α.

The reduction in Lemma 18 is based on three main ideas. First, for each limit atom B(b, s) in a semi-ground program P, we use a Boolean variable defBb to indicate that an atom of the form B(b, ℓ) exists in a pseudo-model of P, a Boolean variable finBb to indicate whether the value of ℓ is finite, and an integer variable valBb to capture ℓ if it is finite. Second, each rule of P is encoded as a universally quantified Presburger formula by replacing each standard atom with its encoding. Finally, entailment of α from P is encoded as a sentence stating that, in every pseudo-interpretation, either some rule in P is not satisfied, or α holds; this requires universal quantifiers to quantify over all models, and existential quantifiers to negate the (universally quantified) program.

Lemma 19 bounds the magnitude of integers in models of Presburger formulas from Lemma 18. These bounds follow from recent deep results on semi-linear sets and their connection to Presburger arithmetic [Chistikov and Haase, 2016].

1 Note that each multiplication-free limit program can be normalised in polynomial time to a limit-linear program.

Lemma 19. Let ϕ = ∀x∃y. ∨ni=1 ψi be a Presburger sentence where each ψi is a conjunction of possibly negated atoms of size at most k mentioning at most ℓ variables, a is the maximal magnitude of an integer in ϕ, and m= |x|. Then, ϕ is valid if and only if ϕ is valid over models where each integer variable assumes a value whose magnitude is bounded by (2O(ℓ log ℓ) · akℓ )n2ℓ ·O(m4 ) .

Lemmas 18 and 19 provide us with bounds on the size of counter-pseudo-models for entailment.

Theorem 20. For P a semi-ground limit-linear program, D a dataset, and α a fact, P ∪D ̸|= α if and only if a pseudomodel J of P ∪D exists where J ̸|= α, |J| ≤ |P ∪D|, and the magnitude of each integer in J is bounded polynomially by the largest magnitude of an integer in P ∪D, exponentially by |P|, and double-exponentially by maxr∈P ‖r‖.

By Theorem 20, the following nondeterministic algorithm decides P ̸|= α:

1. compute the semi-grounding P ′ of P;
2. guess a pseudo-interpretation J that satisfies the bounds given in Theorem 20;
3. if TP ′(J) ⊑ J (so J |= P ′ ) and J ̸|= α, return true.

Step 1 requires exponential (polynomial in data) time, and it does not increase the maximal size of a rule. Hence, Step 2 is nondeterministic exponential (polynomial in data), and Step 3 requires exponential (polynomial in data) time to solve a system of linear inequalities. Theorem 21 proves that these bounds are both correct and tight.

Theorem 21. For P a limit-linear program and α a fact, deciding P |= α is CONEXPTIME-complete in combined and CONP-complete in data complexity.

The upper bounds in Theorem 21 follow from Theorem 20, CONP-hardness in data complexity is shown by a reduction from the square tiling problem, and CONEXPTIME-hardness in combined complexity is shown by a similar reduction from the succinct version of square tiling.

6 Tractability of Entailment: Stability

Tractability in data complexity is important on large datasets, so we next present an additional stability condition that brings the complexity of entailment down to EXPTIME in combined and PTIME in data complexity, as in plain Datalog.

6.1 Cyclic Dependencies in Limit Programs

The fixpoint of a plain Datalog program can be computed in PTIME in data complexity. However, for P a limit-linear program, a na¨ıve computation of T∞P may not terminate since repeated application of TP can produce larger and larger numbers. Thus, we need a way to identify when the numeric argument ℓ of a limit fact A(a, ℓ) diverges-that is, grows or decreases without a bound; moreover, to obtain a procedure tractable in data complexity, divergence should be detected after polynomially many steps. Example 22 illustrates that this can be achieved by analysing cyclic dependencies.

Example 22. Let Pc contain facts A(0) and B(0), and rules A(m) →B(m) and B(m) →A(m+1), where A and B are max predicates. Applying the first rule copies the value of A into B, and applying the second rule increases the value of A; thus, both A and B diverge in T∞Pc . The existence of a cyclic dependency between A and B, however, does not necessarily lead to divergence. Let program P ′c be obtained from Pc by adding a max fact C(5) and replacing the first rule with A(m) ∧ C(n) ∧ (m ≤ n) → B(m). While a cyclic dependency between A and B still exists, the increase in the values of A and B is bounded by the value of C, which is independent of A or B; thus, neither A nor B diverge in T∞P ′c .

In the rest of this section, we extend <, +, and - to ∞ by defining k < ∞, ∞+ k = ∞, and ∞- k = ∞ for each integer k. We formalise cyclic dependencies as follows.

Definition 23. For each n-ary limit predicate B and each tuple b of n - 1 objects, let vBb be a node unique for B and b. The value propagation graph of a semi-ground limitlinear program P and a pseudo-interpretation J is the directed weighted graph GJP = (V, E, µ) defined as follows.

1. For each limit fact B(b, ℓ) ∈ J, we have vBb ∈ V.
2. For each rule r ∈ P applicable to J with the head of the form A(a, s) where vAa ∈ V and each body atom B(b,m) of r where vBb ∈ V and variable m occurs in term s, we have 〈vBb, vAa〉 ∈ E; such r is said to produce the edge 〈vBb, vAa〉 in E.
3. For each r ∈ P and each edge e = 〈vBb, vAa〉 ∈ E produced by r, δe r (J) = ∞ if opt(r, J) = ∞; otherwise,

where ℓ is such that B(b, ℓ) ∈ J. The weight of each edge e ∈ E is then given by

A positive-weight cycle in GJP is a cycle for which the sum of the weights of the contributing edges is greater than 0.

Intuitively, GJP describes how, for each limit predicate B and objects b such that B(b, ℓ) ∈ J, operator TP propagates ℓ to other facts. The presence of a node vBb in V indicates that B(b, ℓ) ∈ J holds for some ℓ ∈ Z∪ {∞}; this ℓ can be uniquely identified given vBb and J. An edge e = 〈vBb, vAa〉 ∈ E indicates that at least one rule r ∈ P is applicable to J where h(r) = A(a, s), B(b, m) ∈ sb(r), and m occurs in s; moreover, applying r to J produces a fact A(a, ℓ′ ) where ℓ′ satisfies ℓ + µ(e) ≤ ℓ′ if both A and B are max predicates, and analogously for the other types of A and B. In other words, edge e indicates that the application of TP to J will propagate the value of vBb to vAa while increasing it by at least µ(e). Thus, presence of a positive-weight cycle in GJP indicates that repeated rule applications might increment the values of all nodes on the cycle.

6.2 Stable Programs

As Example 22 shows, the presence of a positive-weight cycle in GJP does not imply the divergence of all atoms corresponding to the nodes in the cycle. This is because the weight of such a cycle may decrease after certain rule applications and so it is no longer positive.

This motivates the stability condition, where edge weights in GJP may only grow but never decrease with rule application. Hence, once the weight of a cycle becomes positive, it will remain positive and thus guarantee the divergence of all atoms corresponding to its nodes. Intuitively, P is stable if, whenever a rule r ∈ P is applicable to some J, rule r is also applicable to each J ′ with larger limit values, and applying r to such J ′ further increases the value of the head. Definition 24 defines stability as a condition on GJP . Please note that, for all pseudo-interpretations J and J ′ with J ⊑ J ′ and GJP = (V, E, µ) and GJ ′ P = (V ′ , E ′ , µ′ ) the corresponding value propagation graphs, we have E ⊆ E ′ .

Definition 24. A semi-ground limit-linear program P is stable if, for all pseudo-interpretations J and J ′ with J ⊑ J ′ , GJP = (V, E, µ), GJ ′ P = (V ′ , E ′ , µ′ ), and each e ∈ E, 1. µ(e) ≤ µ′ (e), and

1. e = 〈vBb, vAa〉 and B(b,∞) ∈ J imply µ(e) =∞. A limit-linear program is stable if its semi-grounding is stable.

Example 25. Program Pc from Example 22 is stable, while P ′c is not: for J = {A(0), C(0)} and J ′ = {A(1), C(0)}, we have J ⊑ J ′ , but µ(〈vA, vB〉) = 0 and µ′ (〈vA, vB〉) = -1.

For each semi-ground program P and each integer n, we have TnP ⊑ Tn+1 P , and stability ensures that edge weights only grow after rule application. Thus, recursive application of the rules producing edges involved in a positive-weight cycle leads to divergence, as shown by the following lemma.

Lemma 26. For each semi-ground stable program P, each pseudo-interpretation J with J ⊑ T∞P , and each node vAa on a positive-weight cycle in GJP , we have A(a,∞) ∈ T∞P .

Algorithm 1 uses this observation to deterministically compute the fixpoint of P. The algorithm iteratively applies TP ; however, after each step, it computes the corresponding value propagation graph (line 4) and, for each A(a, ℓ) where node vAa occurs on a positive-weight cycle (line 5), it replaces ℓ with ∞ (line 6). By Lemma 26, this is sound. Moreover, since the algorithm repeatedly applies TP , it necessarily derives each fact fromT∞P eventually. Finally, Lemma 27 shows that the algorithm terminates in time polynomial in the number of rules in a semi-ground program. Intuitively, the proof of the lemma shows that, without introducing a new edge or a new positive weight cycle in the value propagation graph, repeated application of TP necessarily converges in O(|P|2 ) steps; moreover, the number of edges in GJP is at most quadratic |P|, and so a new edge or a new positive weight cycle can be introduced at most O(|P|2 ) many times.

Lemma 27. When applied to a semi-ground stable program P, Algorithm 1 terminates after at most 8|P|6 iterations of the loop in lines 2-8.

Lemmas 26 and 27 imply the following theorem.

Theorem 28. For P a semi-ground stable program, D a dataset, and α a fact, Algorithm 1 decides P ∪ D |= α in time polynomial in ‖P ∪ D‖ and exponential in maxr∈P ‖r‖.

Since the running time is exponential in the maximal size of a rule, and semi-grounding does not increase rule sizes,

Algorithm 1 Entailment for Semi-Ground Stable Programs

Input: semi-ground stable programP, fact α Output: true if P |= α 1: J ′ ··= ∅ 2: repeat 3: J ··= J ′ 4: GJP ··= (V, E, µ) 5: for each vAa ∈ V in a positive-weight cycle in GJP do 6: replace A(a, ℓ) in J with A(a, ∞) 7: J ′ ··= TP(J) 8: until J = J ′ 9: return true if J |= α and false otherwise

Algorithm 1 combined with a semi-grounding preprocessing step provides an exponential time decision procedure for stable, limit-linear programs. This upper bound is tight since entailment in plain Datalog is already EXPTIME-hard in combined and PTIME-hard in data complexity.

Theorem 29. For P a stable program and α a fact, checking P |= α is EXPTIME-complete in combined and PTIMEcomplete in data complexity.

6.3 Type-Consistent Programs

Unfortunately, the class of stable programs is not recognisable, which can again be shown by a reduction from Hilbert's tenth problem.

Proposition 30. Checking stability of a limit-linear program P is undecidable.

We next provide a sufficient condition for stability that captures programs such as those in Examples 5-7. Intuitively, Definition 31 syntactically prevents certain harmful interactions. In the second rule of program P ′c from Example 22, numeric variable m occurs in a max atom and on the lefthand side of a comparison atom (m≤ n); thus, if the rule is applicable for some value of m, it is not necessarily applicable for each m′ ≥ m, which breaks stability.

Definition 31. A semi-ground limit-linear rule r is typeconsistent if

• each numeric term t in r is of the form k0 + ∑ni=1 ki ×mi where k0 is an integer and each ki, 1 ≤ i ≤ n, is a nonzero integer, called the coefficient of variable mi in t;
• if h(r) = A(a, s) is a limit atom, then each variable occurring in s with a positive (resp. negative) coefficient also occurs in a (unique) limit body atom or r that is of the same (resp. different) type (i.e., min vs. max) as h(r); and
• for each comparison (s1 < s2) or (s1 ≤ s2) in r, each variable occurring in s1 with a positive (resp. negative) coefficient also occurs in a (unique) min (resp. max) body atom, and each variable occurring in s2 with a positive (resp. negative) coefficient also occurs in a (unique) max (resp. min) body atom of r.

A semi-ground limit-linear program is type-consistent if all of its rules are type-consistent. Moreover, a limit-linear program P is type-consistent if the program obtained by first semi-grounding P and then simplifying all numeric terms as much as possible is type-consistent.

The first condition of Definition 31 ensures that each variable occurring in a numeric term contributes to the value of the term. For example, it disallows terms such as 0 · x and x - x, since a rule with such a term in the head may violate the second condition. Moreover, the second condition of Definition 31 ensures that, if the value of a numeric variable x occurring in the head 'increases' w.r.t. the type of the body atom introducing x (i.e., x increases if it occurs in a max body atom and decreases otherwise), then so does the value of the numeric term in the head; this is essential for the first condition of stability (cf. Definition 24). Finally, the third condition of Definition 31 ensures that comparisons cannot be invalidated by 'increasing' the values of the variables involved, which is required for both conditions of stability.

Type consistency is a purely syntactic condition that can be checked by looking at one rule and one atom at a time. Hence, checking type consistency is feasible in LOGSPACE.

Proposition 32. Each type-consistent limit-linear program is stable.

Proposition 33. Checking whether a limit-linear program is type-consistent can be accomplished in LOGSPACE.

7 Conclusion and FutureWork

We have introduced several decidable/tractable fragments of Datalog with integer arithmetic, thus obtaining a sound theoretical foundation for declarative data analysis. We see many challenges for future work. First, our formalism should be extended with aggregate functions. While certain forms of aggregation can be simulated by iterating over the object domain, as in our examples in Section 3, such a solution may be too cumbersome for practical use, and it relies on the existence of a linear order over the object domain, which is a strong theoretical assumption. Explicit support for aggregation would allow us to formulate tasks such as the ones in Section 3 more intuitively and without relying on the ordering assumption. Second, it is unclear whether integer constraint solving is strictly needed in Step 7 of Algorithm 1: it may be possible to exploit stability of P to compute TP(J) more efficiently. Third, we shall implement our algorithm and apply it to practical data analysis problems. Fourth, it would be interesting to establish connections between our results and existing work on data-aware artefact systems [Damaggio et al., 2012; Koutsos and Vianu, 2017], which faces similar undecidability issues in a different formal setting.

Acknowledgments

We thank Christoph Haase for explaining to us his results on Presburger arithmetic and semi-linear sets, which were key to some of our technical results. Our work has also benefited from discussions with Michael Benedikt. This research was supported by the Royal Society and the EPSRC projects DBOnto, MaSI3 , and ED3 .