Capturing Homomorphism-Closed Decidable Queries with Existential Rules (Extended Abstract)

1 Introduction

At the core of contemporary logic-based knowledge representation is the concept of querying data sources, often using elaborate query formalisms that allow for taking background knowledge into account. The classical decision problem related to such knowledge-aware querying is Boolean query entailment. From an abstract point of view, a Boolean query identifies a class of databases D - those that satisfy the query, i.e., to which the query "matches". This view allows us to define and investigate properties of (abstract) queries independently from the syntax used to specify them. Such properties can be structural (morphisms, closure properties) or computational (decidability, complexity).

A very popular querying formalism are existential rules, also referred to as tuple-generating dependencies. It is straightforward that the class of databases satisfying some existential rule query is closed under homomorphisms and recursively enumerable. Conversely, it was established that every homomorphism-closed query that is recursively enumerable can be expressed using existential rules [Rudolph and Thomazo, 2015]. That is, plain existential rules already realize their full potential; further syntactic extensions within these boundaries do not enhance expressivity.

∗This is an extended abstract of the paper that won the 2021 Ray Reiter Best Paper Prize at the Int. Conf. on Principles of Knowledge Representation and Reasoning [Bourgaux et al., 2021]

For questions related to automated deduction, however, decidability rather than recursive enumerability is of central interest. The crucial question we tackle in this paper is thus:

Can we characterize an existential rules fragment capable of expressing every decidable homomorphism-closed query?

The generic computational paradigm for existential rules, the chase [Beeri and Vardi, 1984], is based on repetitive, forwardchaining rule application, starting from the database. As this may cause the iterated introduction of new domain elements, this procedure is not guaranteed to terminate - yet, termination is a crucial criterion for decidability. The chase comes in several variants, mainly differing in their (increasingly thorough) mechanisms to prevent unnecessary rule applications: While the Skolem chase [Marnette, 2009] essentially just avoids duplicate rule applications, the standard [Fagin et al., 2005] and the core chase [Deutsch et al., 2008] check for redundancy on a local and global level, respectively.

The class of existential rule sets with terminating 1 Skolem chase has already been weighed and found wanting: it only comprises those queries that are already expressible in plain Datalog - and hence can be evaluated in polynomial time [Marnette, 2009; Kr¨otzsch and Rudolph, 2011; Zhang et al., 2015]. For the standard-chase-terminating and the core-chase-terminating existential rules classes, on the other hand, we only know that the former is contained in the latter [Grahne and Onet, 2018], but little more than that [Kr¨otzsch et al., 2019]. In this paper, we clarify the situation significantly by showing the following:

Standard-chase-terminating existential rules capture the class of all decidable homomorphism-closed queries.

Notably, this implies that standard-chase-terminating and core-chase-terminating existential rule queries are equally expressive and no decidable enhancement of this formalism that preserves homomorphism-closedness (e.g. by allowing disjunction in rule heads) can be strictly more expressive.

As a downside, the existential rules fragment thus identified is not even semi-decidable, that is, one cannot semidecide whether a set of rules is universally terminating for the standard chase. We show that this downside is unavoidable:

1 We always mean universal termination, i.e., for every database.

There are no semi-decidable query languages that (i) express all decidable, homomorphism-closed queries and (ii) for which query answering is decidable.

2 Preliminaries

We first briefly introduce the notions we need in this paper.

Rules We consider first-order formulas over countably infinite sets Vars of variables and Preds of predicates, where each p ∈ Preds has an arity Ar(p) ≥ 0. An atom is an expression p(⃗x) with p ∈ Preds and ⃗x a list of variables of length Ar(p). The fragment of disjunctive existential rules consists of formulas of the form:

where β[⃗x] and ηi[⃗xi, ⃗yi] (i = 1, . . . , k) are conjunctions of atoms with variables ⃗x and ⃗xi ∪ ⃗yi, respectively. We call β body and ∨ki=1 ∃⃗yi.ηi head. Bodies can be empty, but heads must be non-empty. We require that ⃗x and ⃗ yi are mutually disjoint and that ⃗xi ⊆ ⃗x for all i = 1, . . . , k. We single out the fragment of existential rules by disallowing disjunction, i.e. requiring k = 1, and Datalog rules by disallowing existential quantifiers. We omit the universal quantifiers from rules.

Databases, Interpretations, and Entailment The semantics of formulas is based on interpretations, defined as relational structures over a countably infinite set Nulls of nulls. A schema S is a finite set of predicates. An interpretation I over S is a set of expressions p(⃗n) with p ∈ S and ⃗n a list of nulls of length Ar(p). A database is a finite interpretation.

A homomorphism h : I1 → I2 between interpretations I1 and I2 is a mapping h from the nulls in I1 to the nulls in I2, such that p(⃗n) ∈ I1 implies p(h(⃗n)) ∈ I2.

A substitution σ is a mapping from variables to nulls. A rule ρ as in (1) is satisfied by interpretation I if every substitution σ : ⃗x → Nulls with σ(β) ⊆ I can be extended to σ′ : ⃗x ∪ ⃗yi → Nulls for some i ∈ {1, . . . , k} such that σ′ (ηi) ⊆ I. Otherwise, if σ(β) ⊆ I but no extension σ′ of σ verifies σ′ (ηi) ⊆ I for some i, then 〈ρ, σ〉 is applicable to I.

An interpretation I satisfies a set Σ of rules if it satisfies every rule in Σ. An interpretation J is satisfied by an interpretation I if there is a homomorphism h : J → I. I is a model of a rule/rule set/interpretation/database X if X is satisfied by I, written I |= X. As usual, we also write X |= Y if every model of X is a model of Y, where X and Y might be rules, rule sets, databases, or lists of several such elements. Note that the semantics of a database D in this context corresponds to the semantics of a Boolean conjunctive query ∃⃗x. ∧{p(xn1 , . . . , xnℓ ) | p(n1, . . . , nℓ) ∈ D} - we will therefore not introduce such queries as a separate notion. Also note that entailment and satisfaction between interpretations/databases coincide.

AbstractQueries, Expressivity, andDecidability An (abstract) query Q over a schema S is a set of databases over S that is closed under isomorphism, i.e., such that whenever D ∈ Q and D′ is obtained from D by bijective renaming of nulls, then D′ ∈ Q. The query Q is further closed under homomorphisms if, for all D ∈ Q and all homomorphisms h : D → D′ , we have D′ ∈ Q.

Definition 1. Let Goal be a nullary predicate. A query Q over S is expressed by a set Σ of rules if, for every database D over S, we have D ∈ Q if and only if Σ, D |= Goal.

To discuss decidability of queries, we need to see databases as Turing machine (TM) inputs over a fixed alphabet. A serialisation for a schema S is a word s ∈ ({0, 1, ‖} ∪ S)∗ of the form e1 · · · en where n ≥ 0 and ei = pi‖wi1‖ · · · ‖wiAr(pi)‖ for wij ∈ {0, 1}+ and pi ∈ S. Given s of this form and an injection η : {0, 1}+ → Nulls, let η(s) denote the database {pi(η(wi1), . . . , η(wiAr(pi))) | 1 ≤ i ≤ n}. Then s corresponds to a database D if η(s) is isomorphic to D; note that this does not depend on the choice of η.

A query Q with schema S is decidable if the set of all serialisations for S that correspond to some D ∈ Q is decidable.

Universal Models and the Chase Entailment of databases (corresponding to Boolean conjunctive queries) can be decided by considering only a subset of all models. Given sets I and K of interpretations, I is universal for K if, for all K ∈ K, there is I ∈ I and a homomorphism I → K. Consider a rule set Σ and database D, and let M be the set of all models of Σ, D. Then I is a universal model set for Σ and D if I ⊆ M and I is universal for M.

Fact 1. If I is a universal model set for Σ and D then, for every database C, we have Σ, D |= C iff I |= C for all I ∈ I.

Universal model sets can be computed with the chase algorithm. We consider a variation of the standard (or restricted) chase for rules with disjunctions [Carral et al., 2017].

Definition 2. A chase tree for Σ and D is a (finite or infinite) tree where each node is labelled by a database, such that:

1. The root is labelled with D.
2. For every node with label E that has ℓ children labelled C1, . . . , Cℓ, there is a rule ρ ∈ Σ and a substitution σ : ⃗x → Nulls such that (i) 〈ρ, σ〉 is applicable to E, (ii) ρ has ℓ head disjuncts, and (iii) Ci = E ∪ σi(ηi) where σi extends σ by mapping each y ∈ ⃗yi to a fresh null.
3. For each ρ ∈ Σ and σ, there is i ≥ 1 such that 〈ρ, σ〉 is not applicable to the label of any node of depth ≥ i.

The result that corresponds to a chase tree is the set of all interpretations that can be obtained as the union of all interpretations along a path in the tree.

Point (3) ensures fair rule application, but different orders of application can lead to different chase trees, and different results. Nevertheless, every result is semantically correct:

Fact 2. Every result of a chase on a rule set Σ and database D is a universal model set for Σ and D.

The pair 〈Σ,D〉 is chase-terminating if all its chase trees are finite; this corresponds to all-strategy termination. Σ is chase-terminating if 〈Σ,D〉 is chase-terminating for every database D; this corresponds to universal termination.

3 Main Results

We are now ready to state the main results of the paper.

Capturing Decidable Homomorphism-Closed Queries

Given a homomorphism-closed query Q over signature S, and a Turing machine MQ that decides Q, we describe in the next section how to construct a set of standard-chaseterminating existential rules Σ that expresses Q.

Theorem 3. Chase-terminating existential rules capture the class of all decidable homomorphism-closed queries.

Limitations of Semi-Decidable Languages A query language F over a schema S is a function from a set L to 2DS , where DS is the set of all databases over schema S. We say that F is semi-decidable if membership to L is semidecidable, and that its query answering problem is decidable if there exists a TM MF that takes as input some (l,D) ∈ (L × DS ) and decides whether D ∈ F(l).

The set of chase-terminating existential rule sets is a query language that is not semi-decidable [Grahne and Onet, 2018] and for which the query answering problem is decidable (by running the chase). In fact, we show that one cannot find a semi-decidable query language with similar properties.

Theorem 4. There are no semi-decidable query languages that (i) express all decidable, homomorphism-closed queries and (ii) for which query answering is decidable.

To show this result, we define a set M of TMs (intuitively, M is the set of all deciders that solve homomorphism-closed queries over databases in D{ed}), show that M can be enumerated up to equivalence if there is a semi-decidable language that satisfies (i) and (ii) above, and finally prove that M is not enumerable up to equivalence.

4 Construction for Theorem 3

In this section we explain how we construct the standardchase-terminating existential rules Σ that expresses the homomorphism-closed query Q to prove Theorem 3.

4.1 Overview

The construction works in three steps:

1. We express Q with a set of disjunctive existential rules simulating a TMMQ deciding Q. Disjunction is actually used in a very light way: It is only used to guess an ordering on the database elements, and to guess which atoms are not present in D.
2. We ensure termination of the standard chase by modifying our rule set. Known syntactic criteria to ensure termination come with an upper bound on the length of the chase (possibly exponential) and are thus not applicable in our setting, as MQ may take arbitrarily long to halt. We thus adapt the "emergency brake" technique [Kr¨otzsch et al., 2019] by casting it as a general rule set transformation, and apply it by detecting the situations in which the previous rule set leads to non-termination. This essentially happens when the "linear order" relation that is guessed contains cycles.
3. Finally, we remove disjunction by noticing that the rule set has a specific shape, in which all disjunctive rules are Datalog rules that can be applied before any existential rules. For such a rule set, we adapt another technique by

Figure 1: The rule set R1, where rules (4) and (14) are instantiated for each p ∈ S, and rules (8) are instantiated for each R ∈ {First, Last, Eq, NEq, LT} ∪ {Inp, NInp | p ∈ S} and 1 ≤ i ≤ Ar(R), and ⃗xxi↦→y denotes ⃗x with xi replaced by y.

Figure 2: The rule set R2 contains R1 (see Figure 1) and all above rules, where (19) and (20) are instantiated for each p ∈ S.

Kr¨otzsch et al. [2019] to create an equivalent set of nondisjunctive existential rules: It builds all possible worlds corresponding to choices made by disjunctive Datalog rules, simulates the application of non-disjunctive existential rules in each world independently, and aggregates the results from all worlds.

In the remaining of this section, we focus on the first step.

4.2 Expressing Qwith Disjunctive Rules

We build five rule sets R1 ⊆ R2 ⊆ R3 ⊆ R4 ⊆ R5 such that for any database D over S, there is a universal model set M of R5 and D s.t. D ∈ Q iff Goal ∈ I for every I ∈ M.

Intuitively, R1 constructs all possible linear orders over the nulls in D, as well as all possible completions of D with facts built using these nulls; R2 \ R1 extracts successor relations from the linear orders; R3 \ R2 associates to nulls representations of their positions in successor relations; R4 \ R3 encodes all initial TM configurations corresponding to some linear order and completion; and R5 \ R4 simulates the run of the TM on these configurations. The two last steps being more standard (e.g. [Abiteboul et al., 1995] and [Baget et al., 2011a]), we focus on R1 to R3 (see Figures 1-3).

Figure 3: The rule set R3 contains R2 (Figure 2) and all of the above rules, where (27) and (28) are instantiated for each ∗ ∈ {0, 1}.

Guessing an Order and Completing the Database R1 serves two distinct purposes: (1) predicates First, Last, Eq ("="), NEq ("̸="), and LT ("<") encode representations of possible linear orders over nulls in D (collected in predicate DbDom); and (2) predicates Inp and NInp for each p ∈ S explicitly encode positive and negative (absent) facts in D. Both purposes require disjunctive reasoning. Possible models include representations of strict, total linear orders (1) and the exact database completion (2), but also models for collapsed orders and inconsistent completions. The latter is not problematic since we consider homomorphism-closed queries.

Building a Tree Structure According to the Order The purpose of R2 is to extract successor relations from the transitive linear order LT. It builds a tree structure - defined using predicates Root, Chi ("child"), and Leaf - where each path is a sequence of nulls representing a sequence of elements that respects the linear order LT. Unavoidably, some elements may be skipped in some sequences, but one path is complete, and it is the successor relation with respect to LT. Note that it may lead to non-termination of the restricted chase when the guessed LT contains a cycle. This problem is dealt with in the second part of the construction. Moreover, nulls are related via predicates In′p and NIn′p that reflect the relations for Inp and NInp that hold between the represented elements (in the database completion of the considered model I of R1).

Creating a Binary Encoding of the Distance from the Root The purpose of R3 is to associate each node in the tree of R2 with a binary encoding of its distance from the root (the root starts with "distance" 2 for technical reasons). Encodings start at the least significant bit and always end in 1 (i.e., have no leading 0s). To simplify upcoming steps, encodings take the form of little TM tapes, represented by a Nxt-connected chain of nulls with unary predicates S0 and S1 encoding the symbol at each position. Nodes u relate to the first and last null ts and te of their "tape" through facts Enc(u, ts, te). Facts Cpy(as, ae, bs, be) are used to create a tape between bs and be that contains a copy of the information on the tape between as and ae. Predicate Cpy+1 is analogous, but creates a representation of the successor of the number that is copied.

5 Discussion and Conclusion

We characterized all decidable homomorphism-closed Boolean queries: These are exactly the chase-terminating existential rule queries, that is, queries that can be expressed by a set of (non-disjunctive) existential rules for which the standard chase universally terminates irrespective of the order of rule applications (as long as it is fair).

By its nature, our result immediately shows that various extensions of our framework do not increase its expressivity:

Theorem 5. Chase-terminating existential rule queries have the same expressivity as

1. existential rule queries with guaranteed existence of some finite chase tree (for every database)
2. existential rule queries for which the chase terminates according to some fair strategy (such as datalog-first),
3. core-chase-terminating [Deutsch et al., 2008] existential rule queries,
4. disjunctive chase-terminating existential rule queries.

Moreover, our result also applies to query languages and querying formalisms of different types. An interesting example is the existential rules fragment of bounded treewidth sets (bts) of rules [Baget et al., 2011a] that is not chaseterminating and encompasses many well-known existential rule fragments with decidable query entailment, including guarded [Cal`ı et al., 2008], frontier-guarded [Baget et al., 2011a], and glut-guarded existential rules [Kr¨otzsch and Rudolph, 2011], as well as greedy bts [Baget et al., 2011b]:

Theorem 6. Let Σ be a bounded-treewidth set of rules and Q a conjunctive query. There is a chase-terminating set ΣQ of existential rules such that D, Σ |= Q iff D, ΣQ |= Goal.

While possibly surprising, this is a consequence of decidability of conjunctive query entailment from bts and of homomorphism-closedness of existential rule queries. Note, however, that every Q would give rise to a different ΣQ. Asking for a "uniform" chase-terminating existential rules set Σ′ satisfying D, Σ′ |= Q iff D, Σ |= Q would change the game [Zhang et al., 2015]. Such a set will not exist in all cases.

As we learned recently, Cabibbo [1998] shows a result akin to Theorem 3 for monotonic queries and Horn logic with inequality. This is important prior work that nonetheless also has important differences, explaining why our proof required several new techniques. A detailed discussion is planned for future work. Another direction of future research is to look at complexity instead of expressivity. Indeed, even though several chase variants can express the same query, we believe that not all of them lead to worst-case optimal computations.

Acknowledgements

The authors thank Jan van den Bussche for pointing them to the related work of Cabibbo [1998] during a discussion at ICDT conference 2022.

This work is partly supported by DFG in project number 389792660 (TRR 248, Center for Perspicuous Systems), by BMBF in the Center for Scalable Data Analytics and Artificial Intelligence (ScaDS.AI), by the Center for Advancing Electronics Dresden (cfaed), by the ERC Consolidator Grant DeciGUT (project number 771779), and by the ANR project CQFD (ANR-18-CE23-0003).