We review a recently introduced extension of Datalog that allows complex values constructed by nesting elements of the input database in sets and tuples. We study its complexity and show that it can be translated into existential rules for which the standard chase terminates on every input database. We identify a tractable fragment, for which membership is undecidable and propose decidable suficient conditions for membership.
An atom is of the form (1, . . . , ar()), where ∈ P and 1, . . . , ar() ∈ C ∪ V ∪ N are terms. An atom is ground if it contains neither variables nor labelled nulls. An existential rule (also called Tuple-Generating Dependency) is a formula of first-order logic of the form ∀, . [, ] → ∃. [, ], where (i) , , and are mutually disjoint lists of variables, (ii) and are conjunctions of null-free atoms, (iii) contains only variables from ∪ , and (iv) contains only variables from ∪ . If is empty, then is a Datalog rule. We call the body and the head of .
A boolean conjunctive query (BCQ) is a first-order sentence of the form ∃. [] with a
conjunction of atoms. A rule set Σ is a finite set of existential rules. Σ is a Datalog program if
each rule ∈ Σ is a Datalog rule. An EDB schema is a finite set PEDB ⊊ P of predicate names;
Σ is compatible with PEDB if no predicate name ∈ PEDB occurs in the head of a rule in Σ . A
database over PEDB is a finite set of ground atoms using only predicate names from PEDB.
We always assume that is over an EDB schema compatible with Σ . A database instance is a
set of variable-free atoms. We consider the usual first-order semantics: a database instance ℐ is
a model of and Σ if ⊆ ℐ and ℐ |= Σ as a first-order theory. Σ and entail BCQ (written
Σ , |= ) if ℐ |= for every model ℐ of Σ and . A model ℐ of Σ and is universal if ℐ |=
if Σ , |= for all BCQ . The standard chase is a well-known algorithm for computing (finite)
universal models; in general, it need not terminate. It terminates universally for a rule set if it
terminates on any database over a compatible EDB schema.
3. DatalogCV
Before defining DatalogCV formally, we can already gain some intuition for complex values and
the additional expressive power they ofer by looking at the following example.
Example 1 Consider a database encoding a directed graph using facts edge(, ) to denote
edges from vertex to vertex . In our proposed formalism DatalogCV, we can query for paths
(represented as sets of edges, i.e., as sets of pairs of vertices) from to as follows:
edge(, ) → path(, , {⟨, ⟩})
path(, , ) ∧ edge(, ) → path(, , ∪ {⟨, ⟩})
(
Consider a database with the following facts: edge(, ) edge(, ) edge(, ) edge(, ) edge(, ) edge(, ) Then we can derive the following three paths from to : path(, , {⟨, ⟩}) path(, , {⟨, ⟩, ⟨, ⟩}) path(, , {⟨, ⟩, ⟨, ⟩})
The set S of sorts is defined inductively; it contains (i) the domain sort ∆ , (ii) for all ∈ S, the set sort { }, and (iii) for all ℓ ≥ 2 and 1, . . . , ℓ ∈ S, the tuple sort ⟨ 1, 2, . . . , ℓ⟩. Every variable ∈ V has a sort sort() = such that the set V = {′ ∈ V | sort(′) = } is countably infinite. The sets T of terms of sort are defined as follows:
TΔ ::= | T⟨ 1,..., ℓ⟩ ::= ⟨1, . . . , ℓ⟩ |
T{ } ::= {1, . . . , } | ( ∩ ′) | ( ∪ ′) | ∈ C, ∈ VΔ ∈ T for 1 ≤ ≤ ℓ, ∈ V⟨ 1,..., ℓ⟩ ∈ T for 1 ≤ ≤ , ′ ∈ T{ }, ∈ V{ }
Terms are constants (of the domain sort), tuples (over the individual component sorts), set literals (over an element sort), intersections or unions of set terms (of a set sort), or variables (of any sort). We also write {} as ∅, and we may emphasise the sort for overloaded symbols with a subscript, as in ∅{ }. Basic terms do not contain ∪ or ∩ ; ground terms are variable-free.
A predicate ∈ P has associated sort sort(). A schema S = ⟨PEDB, PIDB⟩ is a partition of P into EDB predicates PEDB and IDB predicates PIDB. An atom for predicate ∈ P is an expression () where ∈ Tsort(). For tuple-sorted predicates, we write the usual (1, . . . , ℓ) instead of (⟨1, . . . , ℓ⟩); for set terms, we may omit the outermost parentheses, writing, e.g., 1 ∪ 2 for (1 ∪ 2). A fact is an atom (), where contains only basic ground terms. A rule is a sentence of the form ∀. [] → [], where body (possibly empty) and head (non-empty) are conjunctions of atoms. Universal quantifiers are usually omitted. A DatalogCV program for schema S is a finite set of rules, where no rule head contains an EDB predicate. A database D for schema S is a finite set of facts using only EDB predicates. A DatalogCV BCQ is a sentence of the form ∃. [] with a conjunction af atoms containing only basic terms.
Some useful predicates and operations can be defined in DatalogCV.
Example 2 The following rules express the powerset function – we interpret PS (, ) as “
(of sort = { }) has powerset (of sort { } = {{ }}) – and predicates ⊆ , ∈ , ∈/ , ̸= ,
and ⊂ for a set sort and an arbitrary sort , which we write infix 1 ◇ 2 instead of ◇ (1, 2)
for better readability.
(
→ PS (∅, {∅}) PS (, ) ∧ PSU (, , ) → PS ( ∪ {}, ∪ ) → PSU (, ∅, ∅) → ⊆ ∪ ∪ {} ⊆ → ∈ ∩ {} ⊆ ∅ → ∈/ {} ∩ {} ⊆ { } ∅ → ̸= ⊆ ∧ ∈ ∧ ∈/ → ⊂
Rule (8) states that the powerset of ∅ is {∅} and rule (9) states that, given the powerset of
, the powerset of ∪ {} is obtained from by adding ∪ {} for every ∈ , which
is computed by rules (
PSU (, ∅, ∅) PS (∅, {∅})
PSU (, {∅}, {{}})
PS ({}, {∅, {}})
PSU (, {{∅}}, {∅})
Note that rules like (
We assume that these shortcuts are always available in DatalogCV programs, and that databases are flat , i.e., they contain only facts of the domain sort ∆ or of some tuple sort ⟨∆ , . . . , ∆ ⟩ over domain elements; all other facts can be constructed using appropriate rules.
Similar to Datalog, we base our semantics on an Herbrand interpretation with the set of constants syntactically occurring in a given program and database as domain, where we interpret constants as themselves (unique name assumption). For sorts and ground terms, we define the interpretation using a function eval(· ). For sorts, let eval(∆) := C, eval(⟨ 1, . . . , ℓ⟩) := eval( 1) × · · · × eval( ℓ), and eval({ }) := (eval( )) = { | ⊆ eval( )}. For ground terms , we define eval() as follows:
eval() := eval(⟨1, . . . , ℓ⟩) := ⟨eval(1), . . . , eval(ℓ)⟩ eval({1, . . . , }) := {eval(1), . . . , eval()} eval(1 ∩ 2) := eval(1) ∩ eval(2) eval(1 ∪ 2) := eval(1) ∪ eval(2) ∈ C (15) (16) (17) (18) (19)
The domain dom(P, D) of a DatalogCV program P and database D is the set of all constants occurring in P or D. An interpretation for P and D maps every predicate to a set ℐ ⊆ eval(sort()) containing only constants from dom(P, D). ℐ satisfies a ground atom (), written ℐ |= (), if eval() ∈ ℐ ; it satisfies a conjunction of such atoms, written ℐ |= , if ℐ |= for all ∈ ; and it satisfies a variable-free rule → , written ℐ |= → , if ℐ ̸|= or ℐ |= . ℐ satisfies D if ℐ |= for all ∈ D. If ℐ satisfies , we also call ℐ a model of .
As usual, we obtain a notion of entailment from this model theory: a ground fact is entailed by P and D, written P, D |= , if ℐ |= for all models ℐ of P and D. We can reduce BCQ entailment to ground fact entailment by using BCQs as bodies of a rule with some ground head atom not derived by any other rule.
As for Datalog, entailment can be decided by considering a single least model, which can also be computed by a chase-like process.
The complexity of reasoning for program P depends on the nesting of sorts occurring in P. The set-height of a sort is the maximal nesting level of sets within, e.g., s-height(∆) = 0 and s-height({{0}}) = 2.
Theorem 1 Let P be a DatalogCV program and D be a database for schema S, and let be a ground fact. Deciding P, D |= is ExpTime-complete for data complexity and ( + 2)ExpTimecomplete for combined complexity, where is the largest set-height of a sort in S. For hardness, we extend a linear order encoded in D to levels of nested powersets, obtaining a -exponentially long Turing tape. For the additional exponent (over Datalog) in combined complexity, we first obtain a doubly-exponential chain by ordering nested tuples, which forms the new basis for the powerset construction.
DatalogCV programs, databases, and BCQs admit a translation into sets of existential rules such that query entailment over the translation has the same answers and the same complexity. This requires additional rules and also additional facts for every fact ∈ D: Theorem 2 Let P be a DatalogCV program and D be a database for P. Then there is a set tr(P) of existential rules and a set of facts tr(D) such that: (i) for every DatalogCV BCQ , there is tr() with P, D |= if tr(P), tr(D) |= tr(); (ii) tr(P), tr(D), and tr() can be computed in logarithmic space; and (iii) every standard chase sequence for tr(P) over tr(D) terminates in a number of steps that is -exponential in the size of D and ( + 2)-exponential in the size of P. 4. Tractable reasoning with DatalogCV We now identify a fragment of DatalogCV for which reasoning is still data-tractable. As 0ExpTime is PTime, one such fragment is set-free DatalogCV. By flattening nested tuples, set-free DatalogCV programs can be translated into Datalog programs with exponentially larger arities. We can do this even in the presence of sets, as long as we can bound the cardinality of all sets that might be derived.
A program P has -bounded cardinality if, for any database D for P, all ground facts with P, D |= are of the form {1, . . . , } with ≤ . It has bounded cardinality if it has -bounded cardinality for some . A -bounded cardinality DatalogCV program can be transformed into a set-free DatalogCV program by replacing set sorts = { } with -tuples ⟨, . . . , ⟩ and filling up empty positions with placeholders □ .
Theorem 3 Entailment for bounded cardinality DatalogCV programs is PTime-complete for data complexity and 2ExpTime-complete for combined complexity.
While bounded cardinality is undecidable, we can check for -bounded cardinality by considering a variant of the critical instance with ( + 1) elements. Theorem 4 It is undecidable whether a program P has bounded cardinality; given ≥ 0, deciding if P has -bounded cardinality is 2ExpTime-complete.
Weak set acyclicity tracks the propagation of sets along positions of the program and ensures the absence of cycles involving set unions. The cardinality constraints problem is a system of inequalities estimating the minimal cardinality of sets. Both approaches lead to suficient conditions for bounded cardinality: Theorem 5 Let P be a DatalogCV program. Deciding if P is weakly set-acyclic is NL-complete; checking if the cardinality constraints problem for P has an optimal value is in PTime. Both conditions imply bounded cardinality.
Many syntactic criteria guarantee universal termination of the chase, but all fragments identified so far exhibit PTime data complexity. Yet rule sets with universally terminating chases can express arbitrarily complex queries [5, 4]. This makes DatalogCV the first structured approach for obtaining such rule sets, and it puts complex values within reach of reasoners such as VLog [6].
The authors thank Stephan Mennicke for feedback on an earlier draft of this paper. This work is partly supported by Deutsche Forschungsgemeinschaft (DFG, German Research Foundation) in project number 389792660 (TRR 248, Center for Perspicuous Systems), by the Bundesministerium für Bildung und Forschung (BMBF, Federal Ministry of Education and Research) in the Center for Scalable Data Analytics and Artificial Intelligence (ScaDS.AI), and by BMBF and DAAD (German Academic Exchange Service) in project 57616814 (SECAI, School of Embedded and Composite AI).