Finite Controllability of Conjunctive Query Answering with Existential Rules: Two Steps Forward

1 Introduction

The problem of answering a Boolean query q against a logical theory consisting of an extensional database D and an ontology Σ is attracting the attention of various fields of Computer Science, fromArtificial Intelligence [Baget et al., 2011; Calvanese et al., 2013; Gottlob et al., 2014; Amendola et al., 2018] to Database Theory [Bienvenu et al., 2014; Alviano and Pieris, 2015] and Logic [P´erez-Urbina et al., 2010]. This problem, known as ontology-based query answering (OBQA), is usually stated as D∪Σ |=a q, and it is equivalent to checking whether q is satisfied by all models of D∪Σ according to the "open-world" semantics of first-order logic (where |=a is the entailment under arbitrary models).

Both Description Logics [Baader et al., 2002] and Datalog± [Cal`ı et al., 2009a] have been recognized as effective families of formal knowledge representation languages to specify Σ, while union of (Boolean) conjunctive queries, U(B)CQs for short, is the most common and studied formalism to express q. Unfortunately, for both these families, OBQA is generally undecidable [Johnson and Klug, 1984; Rosati, 2007; Cal`ı et al., 2013]. Hence, a number of syntactic decidable classes of the above languages have been singled out. But decidability alone is not the only desideratum. For example, a good balance between computational complexity and expressiveness is of high importance too. But there is another property that is turning out to be as interesting as challenging to prove: finite controllability [Johnson and Klug, 1984]. A class C of ontologies is finitely controllable if, for each triple 〈D, Σ, q〉 with Σ ∈ C, it holds that D∪Σ |=a q if, and only if, D ∪ Σ |=f q, where |=f is the entailment under finite models only. Note that this is equivalent to D∪Σ ̸|=a q implies there is a finite model M of D ∪ Σ such that M ̸|= q, as the "only if" direction is trivially true. And there are applications, both in Databases [Johnson and Klug, 1984; Rosati, 2006] and Knowledge Representation [Rosati, 2008; Ib´a˜nez-Garc´ıa et al., 2014], where reasoning over finite models is preferred.

In this paper we focus on the Datalog± family, and consider for Σ a set of existential rules of the form ∀X∀Y(φ(X,Y) → ∃Zp(X,Z)), where the body φ(X,Y) is a conjunction of atoms, and the head p(X,Z) is a single atom. The main decidable classes rely on the following basic five syntactic properties: weak-acyclicity [Fagin et al., 2005], linearity [Cal`ı et al., 2009b], guardedness [Cal`ı et al., 2013], stickiness [Cal`ı et al., 2010], and shyness [Leone et al., 2012], which underlie the basic classes called weakly-acyclic, linear, guarded, sticky, and shy, respectively. Several variants and combinations of these classes have been defined and studied too [Baget et al., 2010; Kr¨otzsch and Rudolph, 2011; Cal`ı et al., 2012; Gottlob et al., 2013; 2018], as well as semantic properties subsuming the syntactic ones [Baget et al., 2011; Leone et al., 2012].

The above basic classes are pairwise uncomparable, except for linear which is strictly contained in guarded and shy, as reported in Figure 1. Interestingly, both weakly-acyclic and shy strictly contain datalog -the well-known class of existentialfree rules of the form ∀X∀Y(φ(X, Y) → p(X)). Moreover, sticky strictly contains joinless -the class collecting sets of rules where each body contains no repeated variable. The latter, introduced by [Gogacz and Marcinkowski, 2017] to prove that sticky is finitely controllable, is also exploited in this paper. Finally, both linear and joinless strictly contain inclusion-dependencies -the well-known class of relational database dependencies collecting sets of rules with one single body atom and no repeated variable.

Under arbitrary models, OBQA can be reduced to answering q over a universal model U that can be homomorphically embedded into every other arbitrary (finite or infinite) model of D ∪ Σ. Hence, D ∪ Σ |=a q if, and only if, U |= q. A way to compute such a U is to employ the chase procedure [Beeri and Vardi, 1984]. Intuitively, starting fromD, the chase "repairs" violations of rules by repeatedly adding new atoms - introducing fresh values, called nulls, whenever required by an existential variable- until all rules are satisfied. In the classical setting, the chase is sound and complete. But when finite model reasoning is required, then the chase is generally uncomplete, unless ontologies are finitely controllable.

Finite controllability of weakly-acyclic comes for free as every ontology here admits a finite universal model [Fagin et al., 2005]. Conversely, the proof of this property for the subsequent three classes has been a very different matter. Complex, yet intriguing, constructions have been devised for linear [Rosati, 2006; B´ar´any et al., 2014], guarded [B´ar´any et al., 2014], and more recently for sticky [Gogacz and Marcinkowski, 2017]. To complete the picture, we address the same problem for shy, while taking two steps forward: 1

▶We devise a general technique, called canonical rewriting, to facilitate the process of (dis)proving finite controllability of any class of existential rules. Indeed, via this technique, we can immediately (re)confirm that linear is finitely controllable since inclusion-dependencies is. Additionally, we can prove that sticky-join [Cal`ı et al., 2012] -generalizing both sticky and linear- is finitely controllable since sticky is.

▶We specialize the canonical rewriting to complete the picture for the aforementioned five basic classes, and show that also shy is finitely controllable since joinless is.

2 Basics: Ontology-Based Query Answering

Basics. Let C, N and V denote pairwise disjoint discrete sets of constants, nulls and variables, respectively. A term t is an element of T = C∪N∪V. An atom α is a labeled tuple p(t1, ..., tm), where p is a predicate symbol, m is the arity of both p anf α, and t1, ..., tm are terms. An atom is simple if it contains no repeated term, and it is propositional if it has arity 0. Given two sets A and B of atoms, a homomorphism from A to B is a mapping h : T → T such that c ∈ C implies h(c) = c, and h(A) ⊆ B with h(A) obtained from A by replacing each term t by h(t). An instance I is a discrete set of atoms where each term is either a constant or a null.

Syntax. A database D is a finite null-free instance. An (existential) rule ρ is a logical implication of the form ∀X∀Y(φ(X,Y) → ∃Z p(X,Z)), with X ∪ Y ∪ Z ⊆ V, whose body (resp., head) body(ρ) = φ(X,Y) (resp., head(ρ) = {p(X,Z)}) is a conjunction (or set) of atoms, possibly with constants. The set X is called the frontier of ρ. An ontology Σ is a set of rules. A union of Boolean conjunctive query, UBCQ for short, q is a first-order expression of the form ∃Y1ψ1(Y1) ∨ . . . ∨ ∃Ykψk(Yk), where each ψj(Yj) is a conjunction of atoms. Constants may occur also in q.

1 This paper is an abridged version of [Amendola et al., 2017].

Semantics. Consider a triple 〈D,Σ, q〉 as above. An instance I satisfies a rule ρ ∈ Σ, written I |= ρ, if whenever there is a homomorphism h from body(ρ) to I, then there is a homomorphism h′ ⊇ h|X from head(ρ) to I. Also, I satisfies Σ, written I |= Σ, if I satisfies each rule of Σ. The (arbitrary) models of D∪Σ, written amods(D, Σ), are the set {I : I ⊇ D and I |= Σ}. Amodel U is universal if, for each M ∈ amods(D, Σ), there is a homomorphism from U to M. An instance I satisfies q, written I |= q, if there is a homomorphism from some ψj(Yj) to I. Also, q is true over D∪Σ, written D ∪ Σ |=a q, if each model of D ∪ Σ satisfies q.

Finite controllability. A class C of ontologies is finitely controllable if, for each triple 〈D,Σ, q〉 with Σ ∈ C, D ∪ Σ ̸|=a q implies there is M ∈ fmods(D, Σ) s.t. M ̸|= q, where fmods(D, Σ) denotes the finite models of D ∪ Σ. This is usually stated as D∪Σ |=a q if, and only if, D∪Σ |=f q.

3 Step 1: Canonical Rewriting

We design a general technique (see Figure 2) to facilitate the process of (dis)proving finite controllability of an arbitrary class of existential rules. Specifically, any triple 〈D,Σ, q〉 is rewritten in the semantically equivalent (canonical) triple 〈Dc , Σc , qc 〉 that has the advantage of being structurally simpler than the original one. Indeed, Dc is a propositional database, while Σc and qc are constant-free structures containing simple atoms only. Rather than giving boring formal details, we prefer to shed some light on our construction via a simple example. Let D = {p(a), p(b), r(a, b)}, and Σ consist of the following rules:

We now construct Dc = {p[a], p[b], r[a,b]} as the propositional database obtained by encoding each atom of D in a different fresh predicate. Then, from Σ we build Σc as follows:

Intuitively, new predicates encode tuples of terms consisting of constants (a and b) from D ∪ Σ, and placeholders (1 and 2, where the latter is the maximum arity among predicates occurring in Σ) of arbitrary terms of C ∪ N. Any rule ρi,j of Σc is called child of ρi, while the latter is the parent of ρi,j. Finally, by following the same intuition, we apply the canonical rewriting to a set A of atoms over C∪V w.r.t. the constants of D∪Σ. E.g., given A = {r(a, X), p(X)}, we obtain the following family of sets Ac = {{r[a,a], p[a]}, {r[a,b], p[b]}, {r[a,1](X), p[1](X)}}. Thus, given the UBCQ q = ∃X{r(a,X), p(X)} ∨ ∃Y {r(Y, Y )}, its canonical rewriting will be qc = {r[a,a], p[a]} ∨ {r[a,b], p[b]} ∨ ∃X{r[a,1](X), p[1](X)} ∨ {r[a,a]} ∨ {r[b,b]} ∨ ∃Y {r[1,1](Y )}.

Accordingly, let us define the unpacking function R from atoms over the set of canonical predicates to atoms over the set of original ones. The function generalizes in the obvious way to set of atoms, rules, and queries. For instance, if A′ = {r[1,2](X, Y ), r[1,a](η), r[1,1](η)} with η ∈ N, then R(A′ ) = {r(X, Y ), r(η, a), r(η, η)}. Informally, the unpacking function acts like an "inverse" operator of the canonical rewriting. Consider now the model M = D ∪ {p(η), r(η, a), r(η, b), r(η, η), s(η)} of D ∪ Σ. Also, let M ′ = Dc ∪ {p[1](η), r[1,a](η), r[1,b](η), r[1,2](η, η)} be a model of Dc ∪ Σc . Note that, whenever there is a homomorphism h from the body of some rule ρi,j to M ′ , then h also maps the body of the parent ρi to M. Indeed, this is true as R(M ′ ) ⊆ M. However, although M ′ is a model of Dc ∪ Σc , R(M ′ ) is not a model of D ∪ Σ, as α′ = r[1,2](η, η) does not trigger any rule of Σc , while R(α′ ) triggers ρ2. In fact, this happens because: there is no bijection between the placeholders {1, 2} and {η}, and also M ′ contains no atom of the form r[1,1](η), where a bijection between {1} and {η} exists. To overcome such a

mismatch, we focus on a suitable subset of amods(Dc ∪Σc ).

Definition 1. A model N ′ of Dc ∪Σc is canonical if: (i) it is constant-free; and (ii) for each non-simple atoms α′ of N ′ , there is a simple atom β′ of N ′ such that R(α′ ) = R(β′ ).

From any M ′ it is possible to build a canonical model N ′ that can be homomorphically mapped to M ′ : (1) set N ′ to M ′ ; (2) replace each constant c of N ′ by a fresh null ηc; (3) let E be the set of nulls occurring in atoms of N ′ that violate condition (ii); (4) for each null η of E, let pad(η) = {η1, ..., ηk}, where k is the maximum number of times that η occurs in an atom of N ′ ; (5) for each η of E, replace each atom α′ of N ′ containing η with new atoms obtained from α′ by arranging the elements of pad(η) in the positions where η occurs, while avoiding repetitions; and (6) remove all atoms of N ′ violating condition (ii). Hence, in our running example, N ′ = Dc ∪ {p[1](η1), p[1](η2), r[1,a](η1), r[1,a](η2), r[1,b](η1), r[1,b](η2), r[1,2](η1, η2), r[1,2](η2, η1)}. Now, from the above intuitions, we collect some relevant properties.

Proposition 1. Let A be a set of atoms over C∪V w.r.t. the constants of D ∪ Σ, M ′ be a model of Dc ∪ Σc , and N ′ be a canonical model of Dc ∪Σc . It holds that:

1. If, for some A′ ∈ Ac , M ′ |= A′ , then R(M ′ ) |= A;
2. If R(N ′ ) |= A, then N ′ |= A′ , for some A′ ∈ Ac ;
3. There is N ′0 ∈ camods(Dc ,Σc ) that can be homomorphically mapped toM ′ . Also, if M ′ is finite, then N ′0 is.
4. R(N ′ ) is a model of D∪Σ;
5. amods(D,Σ) ⊆R(amods(Dc ,Σc )).

With these properties in hand we are able to provide a formal argument for the implications depicted in Figure 2.

Theorem 1. It holds that:

Proof sketch. We now describe the proof sketch for finite model reasoning (b). We start with the "only-if" direction.

Dc ∪Σc ̸|=f qc

⇒ ∃N ′ ∈ cfmods(Dc ,Σc ) s.t. N ′ ̸|= qc

⇒ ∀q′ ∈ qc it holds that N ′ ̸|= q′

⇒ R(N ′ ) ̸|= q

(by contradiction)

(by Prop. 1.c)

(by definition)

(by Prop. 1.b)

⇒ D∪Σ ̸|=f q

(by Prop. 1.d)

Now, we sketch the proof for the "if" direction.

The implication chains hold also for arbitrary model reasoning (a), by replacing |=f by |=a, and cfmods by camods.

By exploiting our tool, we can reprove that linear is finitely controllable. In fact, the canonical rewriting of a linear ontology belongs to inclusion-dependencies. Moreover, since the canonical rewriting of a sticky-join [Cal`ı et al., 2012] ontology belongs to sticky, we prove (for the first time) that:

Theorem 2. sticky-join is finitely controllable.

Note that the definitions of linear and sticky-join in [Gogacz and Marcinkowski, 2017] are not standard (actually stricter): there, in linear repeated variables are admitted only in rule heads, and the difference between sticky and stickyjoin "can only be seen if repeated variables in the heads of the rules are allowed". Hence, the finite controllability of sticky-join was unknown before our work. One can verify that the proof of their Lemma 4 breaks when moving to the linear (hence sticky-join) ontology Σ = {p(X, X) → r(X); r(X) → ∃Y r(Y )} paired with the database D = {p(c, c)}.

4 Step 2: Finite Controllability of Shy

Differently from linear and sticky-join, the canonical rewriting of a shy ontology -although it is still a shy ontologyfalls in none of the known finitely controllable classes. Hence, to prove the finite controllability of shy, we are going to specialize the canonical rewriting. But before, let us recall the key properties of this class. Fix a triple 〈D, Σ, q〉:

Proposition 2 ([Leone et al., 2012]). Assume Σ ∈ shy. Given a universal model U of D∪Σ, a rule ρ of Σ, and a homomorphism h from the atoms of ρ to U, it holds that:

1. if a variable X of ρ occurs in two different atoms of body(ρ), then h(X) ∈ C; and
2. if two frontier variables X, Y of ρ occur in two different atoms of body(ρ) and h(X) = h(Y ), then h(X) ∈ C.

Consider now the canonical rewriting 〈Dc ,Σc , qc 〉 of 〈D,Σ, q〉. Inspired by well-supported interpretations [Fages, 1991], we define a suitable subset of all finite models:

Definition 2. A finite model M ′ of Dc ∪Σc is well-supported if there is an ordering α1, ..., αm of its atoms s.t., for each j ∈ {1, ...,m}, it holds that: (i) αj ∈ Dc , or (ii) there is ρ ∈ Σc and a homomorphism from the atoms of ρ to {α1, ..., αj} mapping body(ρ) to {α1, ..., αj-1} and head(ρ) to {αj}.

Subsequently, we define Σc⊖ as the set of all joinless rules of Σc . For instance, consider the ontology Σ = {ρ0 = p(X) → r(X, Y ); ρ1 = p(X) → s(X, Y ); ρ2 = r(X, Y ), s(X, Y ) → t(X)} and the database D = {p(a)}. According to the canonical rewriting, Σc = {ρ0,0 = p[a] → r[a,1](Y ); ρ0,1 = p[1](X) → r[1,2](X, Y ); ρ1,0 = p[a] → s[a,1](Y ); ρ1,1 = p[1](X) → s[1,2](X, Y ); ρ2,0 = r[a,a], s[a,a] → t[a]; ρ2,1 = r[a,1](Y ), s[a,1](Y ) → t[a]; ρ2,2 = r[1,a](X), s[1,a](X) → t[1](X); ρ2,3 = r[1,2](X, Y ), s[1,2](X, Y ) → t[1](X)}, and Dc = {p[a]}. Hence, Σc⊖ = {ρ0,0, ρ0,1, ρ1,0, ρ1,1, ρ2,0}. Let M ′ = {p[a], r[a,1](η), s[a,1](η), t[1](η)} be a finite model of Dc ∪ Σc⊖ (and not of Dc ∪ Σc ). It can be checked that M ′ is not well-supported. Intuitively, there is no support for the atom t[1](η). However, we can find a subset of M ′ that is a well-supported model of Dc ∪ Σc⊖. In this case, N ′ = M ′ \ {t[1](η)} is the right one, and p[a], r[a,1](η), s[a,1](η) is an ordering satisfying Definition 2.

Note that N ′ is not a model of Dc ∪Σc , as ρ2,1 is not satisfied. Now, starting from N ′ we can build a well-supported finite model of Dc ∪Σc that can be homomorphically embedded into N ′ . To this end, we have developed a technique called propagation ordering. Intuitively, as r[a,1](η) and s[a,1](η) can be generated only by rules ρ0,0 and ρ1,0, respectively, there is no "real necessity" to consider the same null to satisfy both rules. Hence, by exploiting the given ordering of N ′ , we rename and propagate some of the terms of N ′ to construct a well-supported finite model of Dc ∪ Σc . More precisely, we define 〈r[a,1](η)〉 = r[a,1](〈η, 2, 1〉), as r[a,1](η) is the second atom in the ordering given above, and η occurs in the first position of r[a,1]. Similarly, we set 〈s[a,1](η)〉 = s[a,1](〈η, 3, 1〉). That is, 〈η, 2, 1〉 and 〈η, 3, 1〉 are distinct fresh nulls corresponding to η. In this example, we can stop here, as no other propagation appears. It is clear that the new instance N ′0 = {p[a], r[a,1](〈η, 2, 1〉), s[a,1](〈η, 3, 1〉)} is a well-supported model of Dc ∪Σc . Note that here is where the shyness of Σc is crucial. Also, N ′0 can be homomorphically embedded into N ′ by mapping 〈η, 2, 1〉 to η, and 〈η, 3, 1〉 to η. These insights are the basis of the following properties.

Proposition 3. It holds that:

1. The ontology Σc⊖ is finitely controllable [Gogacz and Marcinkowski, 2017];
2. For each M ′ ∈ fmods(Dc ∪ Σc ) there exists a wellsupported finite model N ′ of Dc ∪ Σc s.t. N ′ ⊆ M ′ ;
3. Whenever Σ is shy, for each M ′ ∈ wsfmods(Dc ,Σc⊖), there is a model N ′ ∈ wsfmods(Dc ,Σc ) that can be homomorphically embedded into M ′ .

With these properties in hand, we can now provide a formal argument to show the main result of the section.

Theorem 3. Under shy ontologies, it holds that:

Proof sketch. We prove the "if" direction.

Therefore, we can conclude that the statement is true since the "only if" direction trivially holds.

Finally, the finite controllability of shy follows by combining Theorem 3 with Theorem 1.

Theorem 4. shy is finitely controllable.

5 Conclusion

To complete the related works started with the Introduction, we recall that finite controllability in OBQA was formalized for the first time by [Rosati, 2006] while he was working on a question left open two decades before by [Johnson and Klug, 1984] about containment of conjunctive queries in case of both arbitrary and finite databases. Basically, using our terminology, they proved that ontologies mixing both inclusiondependencies and functional-dependencies are not finitely controllable, by leaving open the case in which ontologies contain inclusion-dependencies only. Rosati then answered positively this question. And a decade later, by demonstrating that shy is finitely controllable (Step 2), we complete an important picture around the basic decidable Datalog± classes. But we believe that the techniques developed here could have future further applications. For example, it would be interesting to extend the canonical rewriting (Step 1) by encoding in the predicates also a bounded number of nulls (apart from constants and placeholders of nulls). This requires more complex techniques, which however would apply to both glutguarded [Kr¨otzsch and Rudolph, 2011] (extending guarded and weakly-acyclic), and weakly-sticky-join [Cal`ı et al., 2012] (extending sticky-join and weakly-acyclic).

Acknowledgments

The paper was partially supported by MISE under project "S2BDW" (F/050389/01-03/X32)-"Horizon2020" PON I&C 2014-20, and by Regione Calabria under project "DLV Large Scale" (CUP J28C17000220006)-POR Calabria 2014-20.