-
The chase procedure is a fundamental tool for solving many issues involving
tuplegenerating dependencies, such as data integration, data-exchange, query answering
using views or query answering on probabilistic databases. In the last decade,
tuplegenerating dependencies raised a renewed interest under the name of existential rules
for the ontology-mediated query answering (OMQA) problem. In this context, the aim
is to query a knowledge base (I; R), where I is an instance (or factbase) and R is a set
of existential rules (see e.g. the survey chapters [
5,16
]). A fundamental property of the
chase is that it allows one to compute a (possibly infinite) universal model of (I; R),
i.e., a model that can be homomorphically mapped to any other model of (I; R). Hence,
the answers to a conjunctive query (and more generally to any kind of query closed by
homomorphism) over (I; R) can be defined by considering solely this universal model.
The chase starts from an instance and exhaustively performs a sequence of rule
applications with respect to a redundancy criterion, which differs according to the
considered chase variant. We focus in this paper on the main variants, namely: semi-oblivious
[15] (aka skolem [15]), restricted [
3,10
] (aka standard [17]) and core [
8
]. All these
produce homomorphically equivalent results but terminate for increasingly larger
subclasses of existential rules. The question of whether a chase variant terminates on all
instances for a given set of existential rules is known to be undecidable when there is
no restriction on the kind of rules [
1,11
]. A number of sufficient syntactic conditions
for termination have been proposed in the literature for the semi-oblivious chase (see
e.g. [
17,12,18
] for syntheses), as well as for the restricted chase [
7
] (note that the
latter paper also defines a sufficient condition for non-termination). However, only few
positive results exist regarding the termination of the chase on specific classes of rules.
Decidability was shown for the semi-oblivious chase on guarded-based rules (linear
rules, and their extension to (weakly-)guarded rules) [
4
]. Decidability of the core chase
termination on guarded rules for a fixed instance was shown in [
13
].
In this work, we provide new insights on the chase termination problem for
linear existential rules, which are precisely of the form 8x8y:[ 1(x; y) ! 9z: 2(x; z)],
where i is an atom and x; y and z are pairwise disjoint tuples of variables. Linear
rules form a simple yet important subclass of guarded existential rules, which
generalizes inclusion dependencies [
9
] and positive inclusions in DL-LiteR [
6
] (which can
be seen as inclusion dependencies restricted to unary and binary predicates).
Concerning the ontology-mediated query answering problem, we note that linear rules are
firstorder rewritable, hence OMQA on conjunctive queries can be solved by query rewriting.
However, it is well known that the size and the unusual form of the rewritten query may
give rise to practical efficiency issues. The materialization of ontological inferences in
the data is often a good alternative to query rewriting, provided that some chase
algorithm terminates. Finally, having the choice of how to process a set of linear rules may
extend the applicability of query answering techniques that combine query rewriting
and materialization [
1
].
The question of whether a chase variant terminates on all instances for a set of
linear existential rules can be asked under two forms: Does every (fair) chase sequence
terminate? Does some (fair) chase sequence terminate? It is well-known that these two
questions have the same answer for the semi-oblivious and the core chase variants, but
not for the restricted chase. Indeed, this last one may admit both terminating and
nonterminating sequences over the same knowledge base. We show that the termination
problem is decidable for linear existential rules, whether we consider any version of the
problem and any chase variant.
We study chase termination by exploiting in a novel way a graph structure, namely
the derivation tree, which was originally introduced to solve the ontology-mediated
(conjunctive) query answering problem for the family of greedy-bounded treewidth sets
of existential rules [
2,19
], a class of rules that generalizes guarded-based rules and in
particular linear rules. We first use derivation trees to show the decidability of the
termination problem for the semi-oblivious and restricted chase variants, and then generalize
them to entailment trees to show the decidability of termination for the core chase. For
any chase variant we consider, we adopt the same high-level procedure: starting from
a finite set of canonical instances (representative of all possible instances), we build a
(set of) tree structures for each canonical instance, while forbidding the occurrence of a
specific pattern, we call unbounded-path witness. The built structures are finite thanks
to this forbidden pattern, and this allows us to decide if the chase terminates on the
associated canonical instance. By doing so, we obtain a uniform approach to study the
termination of several chase variants, which we believe to be of theoretical interest per
se. The derivation tree is moreover a simple structure and the algorithms built on this
notion are likely to lead to an effective implementation.
Besides providing new theoretical tools to study chase termination, we obtain the
following results for linear existential rules:
– a new proof of the decidability of the semi-oblivious chase termination, building on
different objects than the previous proof provided in [
4
]; we show that our algorithm
provides the same complexity upper-bound;
– the decidability of the restricted chase termination, for both versions of the problem,
i.e., termination of all (fair) chase sequences and termination of some (fair) chase
sequence; to the best of our knowledge, these are the first positive results on the
decidability of the restricted chase termination;
– a new proof of the decidability of the core chase termination, with different objects
than previous work on the core chase termination reported in [
13
].
The full paper is available as a technical report [
14
].
15. Marnette, B.: Generalized schema-mappings: from termination to tractability. In: Paredaens,
J., Su, J. (eds.) Proceedings of the Twenty-Eigth ACM SIGMOD-SIGACT-SIGART
Symposium on Principles of Database Systems, PODS 2009, June 19 - July 1, 2009, Providence,
Rhode Island, USA. pp. 13–22. ACM (2009). https://doi.org/10.1145/1559795.1559799
16. Mugnier, M., Thomazo, M.: An introduction to ontology-based query answering with
existential rules. In: Reasoning Web. Reasoning on the Web in the Big Data Era - 10th
International Summer School 2014, Athens, Greece, September 8-13, 2014. Proceedings. pp.
245–278 (2014). https://doi.org/10.1007/978-3-319-10587-1_6
17. Onet, A.: The chase procedure and its applications.
Ph.D. thesis, Concordia University, Canada (2012),
https://pdfs.semanticscholar.org/6b1b/327a989d3d8e2488f645488063f391391b89.pdf
18. Rocher, S.: Querying Existential Rule Knowledge Bases: Decidability and Complexity.
(Interrogation de Bases de Connaissances avec Règles Existentielles : Décidabilité et
Complexité). Ph.D. thesis, University of Montpellier, France (2016),
https://tel.archivesouvertes.fr/tel-01483770
19. Thomazo, M.: Conjunctive Query Answering Under Existential Rules - Decidability,
Complexity, and Algorithms. Ph.D. thesis, Montpellier 2 University, France (2013),
https://tel.archives-ouvertes.fr/tel-00925722