Will My Favorite Chases Terminate If Evaluating Conjunctive Queries Does? One Does Not Simply Decide This

1 Introduction

One of the main tasks in knowledge representation and reasoning is ontology-based data access (OBDA). In OBDA, an ontology is used to enrich a database with domain knowledge, enabling the inference of new information that is not explicitly stored in the database. Existential rules (also known as Datalog±, or tuple-generating dependencies) are a prominent formalism to represent ontologies in OBDA [Fagin, 2018]. A fundamental reasoning task in OBDA is the Boolean conjunctive query (BCQ) entailment problem, which consists in deciding whether a BCQ is entailed by a database and an ontology of interest. Unfortunately, with ontologies expressed as sets of existential rules, BCQ entailment is undecidable in general [Beeri and Vardi, 1981; Calì et al., 2012]. To ensure decidable BCQ entailment, three main properties have been proposed.

First, the chase procedure [Maier et al., 1979] is a materialization-based algorithm that, given a database and a set of existential rules, iteratively applies the rules to the database to produce a (possibly infinite) universal model of the input. If finite, this universal model can then be queried using regular BCQ evaluation techniques to decide entailment. Many variants of the chase procedure exist, differing in the way rules are applied and redundancies are handled. In this paper, we consider the oblivious [Calì et al., 2013], semi-oblivious (a.k.a. Skolem) [Marnette, 2009], restricted (a.k.a. standard) [Fagin et al., 2005a], and core chase variants [Deutsch et al., 2008]. Guaranteed termination of the chase thus implies decidable BCQ entailment, but this property is also desirable in data exchange settings, where one is interested in translating data from a source schema to a target schema while preserving certain properties [Fagin et al., 2005b]. It also enables computing aggregates, which otherwise make little sense on infinite models [Afrati and Kolaitis, 2008], and ensures finite controllability, i.e. only considering finite models does not impact query answers.

Second, query rewriting techniques aim at rewriting the input BCQ into a first-order query that can be directly evaluated over the input database. Rule sets for which such a rewriting exists (and is computable) are called fus, for finite unification set [Baget et al., 2009]. Again, fus rule sets have benefits beyond decidability of BCQ entailment, as they allow answering the rewritten query over any database. In particular, this allows answering queries even without edit access, or answering queries efficiently in streaming settings [Ronca et al., 2018].

Third, bounded treewidth sets (bts) [Calì et al., 2013] are classes of existential rules that ensure that, for any database, the universal model produced by the chase has bounded treewidth. This property renders BCQ entailment decidable by using Courcelle's theorem [Courcelle, 1990], which states that any property definable in monadic second-order logic can be decided in linear time over structures of bounded treewidth. In particular, this helps with efficient answer counting [Feier et al., 2023].

Deciding whether a given set of existential rules has any of these properties (i.e. whether it guarantees termination of a certain chase variant, is fus, or is bts) is, here again, undecidable in general. The classes of such sets of rules are thus called abstract, as opposed to concrete classes for which membership is decidable. Efforts have been devoted to proving that, when restricting to some concrete classes of existential rules, membership in the abstract classes presented above becomes decidable. This is especially the case for chase termination: oblivious and semi-oblivious chase termination have been proven decidable for guarded and for sticky rules [Calautti et al., 2015;

Calautti and Pieris, 2019], while core chase termination is decidable for guarded rules [Hernich, 2012] but remains open for sticky rules. Restricted chase termination appears more difficult: its decidability has been proven for single-head guarded and sticky rules [Gogacz et al., 2020], but remains open in the multi-head case for both classes. The multi-head case for linear rules, a subclass of guarded rules, has been solved only recently [Gerlach et al., 2025].

These approaches vary greatly and often require sophisticated constructions, but they all share two properties: the considered concrete class always enjoys decidable BCQ entailment, and termination of the considered variant of the chase is always proved decidable. This raises the following question: do we get decidable chase termination (or fus membership? or bts membership?) for free when considering concrete classes of rules with decidable BCQ entailment? For fus, the answer is known to be negative, as shown by [Gaifman et al., 1993], who proved that boundedness of Datalog (which coincides with fus membership here) is undecidable. Surprisingly, for chase termination and bts membership, the question remains open. We answer it negatively in this paper:

Theorem 1. There exists a concrete class 𝒞 of sets of existential rules such that:

1. Chase termination is undecidable in 𝒞 for the oblivious, semi-oblivious, restricted, and core chases,
2. 𝑏𝑡𝑠 membership is undecidable in 𝒞, and
3. BCQ entailment is decidable in 𝒞.

This paper is dedicated to proving Theorem 1 by explicitly constructing such a class 𝒞, in Section 3, made of sets of rules that simulate Minsky machines. We then establish the negative results regarding chase termination and bts membership in Section 4, before proving decidability of BCQ entailment in Section 5. Our simulation of Minsky machines is inspired from [Gogacz and Marcinkowski, 2014], a paper interested in termination of the oblivious, semi-oblivious and restricted chases. We modify their construction in non-trivial ways to also support the core chase and to introduce a flooding mechanism that is instrumental in achieving the properties regarding bts membership and BCQ entailment. Detailed proofs can be found in the appendix of the extended version [Larroque and Manière, 2026].

2 Preliminaries

We mostly follow [Carral et al., 2022] for the preliminaries and assume some basic knowledge of first-order logic.

First-Order Logic (FOL) We define Preds, Consts, and Vars to be mutually disjoint, countably infinite sets of predicates, constants, and variables, respectively. Every P ∈ Preds has an arity ar(P) ≥ 0. Let Terms = Consts ∪ Vars be the set of terms. We write lists 𝑡1, . . . , 𝑡𝑛 of terms as ¯ 𝑡 and often treat them as sets. For a formula or set thereof 𝜙, let Preds(𝜙), Consts(𝜙), Vars(𝜙), and Terms(𝜙) be the sets of all predicates, constants, variables, and terms that occur in 𝜙, respectively.

A (P-)atom is a FOL formula P(¯ 𝑡) with P a |¯ 𝑡|-ary predicate and ¯ 𝑡 ∈ Terms. For a formula 𝜙, 𝜙[¯𝑥] indicates that ¯𝑥 contains all free variables that occur in 𝜙.

Definition 2. An (existential) rule 𝑅 is a FOL formula

where ¯𝑥, ¯ 𝑦, and ¯ 𝑧 are pairwise disjoint lists of variables; and 𝐵 and 𝐻 are (finite) non-empty conjunctions of constant-free atoms, called the body and the head of 𝑅, respectively. The set ¯ 𝑦 is the frontier of 𝑅, denoted with fr(𝑅). If ¯ 𝑧 is empty, then 𝑅 is a Datalog rule.

We usually omit universal quantifiers in rules.

An instance ℐ is an existentially closed conjunction of atoms. Its active domain adom(ℐ) is the set of all terms occurring in ℐ. A Boolean conjunctive query (BCQ) has the same form as an instance, and we often identify both notions. A knowledge base (KB) 𝒦 is a tuple ⟨ℛ, ℐ⟩ with ℛ a rule set and ℐ an instance. We often identify rule bodies, rule heads, and instances with sets of atoms.

Given atom sets ℐ and ℐ ′ , a homomorphism ℎ from ℐ to ℐ ′ is a function with domain Vars(ℐ) such that ℎ(ℐ) ⊆ ℐ ′ ; ℎ is an isomorphism from ℐ to ℐ ′ if additionally, ℎ is injective and ℎ-1 is a homomorphism from ℐ to ℐ ′ . A homomorphism ℎ from ℐ to ℐ ′ is a retraction if ℎ is the identity over Vars(ℐ)∩Vars(ℐ ′ ).

We identify logical interpretations with atom sets. An atom set ℐ satisfies a rule 𝑅 = 𝐵 → ∃¯ 𝑧 𝐻 if, for every homomorphism ℎ from 𝐵 to ℐ, there is an extension ˆℎ of ℎ with ˆℎ(𝐻) ⊆ ℐ; equivalently, ℐ is a model of 𝑅. An atom set ℳ is a model of an instance ℐ if there is a homomorphism from ℐ toℳ, and it is a model of a KB ⟨ℛ, ℐ⟩ if it is a model of ℐ and satisfies all rules in ℛ. Given KBs or atom sets 𝐴 and 𝐵, 𝐴 entails 𝐵, written 𝐴 |= 𝐵, if every model of 𝐴 is a model of 𝐵; 𝐴 and 𝐵 are equivalent if 𝐴 |= 𝐵 and 𝐵 |= 𝐴. Given atom sets ℐ and ℐ ′ , it is known that ℐ |= ℐ ′ iff there is a homomorphism from ℐ ′ to ℐ. A model ℳ of a KB 𝒦 is universal if there is a homomorphism fromℳ to every model of 𝒦.

Every KB 𝒦 admits some (possibly infinite) universal model [Deutsch et al., 2008]. Hence, 𝒦 |= 𝑞 for any BCQ 𝑞 iff there is a homomorphism from a universal model of 𝒦 to 𝑞. The BCQ entailment problem takes as input a KB 𝒦 and a BCQ 𝑞 and asks if 𝒦 |= 𝑞; it is undecidable [Beeri and Vardi, 1981].

The chase The chase is a family of procedures that repeatedly apply rules until a fixpoint is reached.

Definition 3 (Triggers and derivations). Given an instance ℐ, a trigger 𝑡 on ℐ is a tuple ⟨𝑅, 𝜋⟩ with 𝑅 = 𝐵 → ∃¯ 𝑧 𝐻 a rule and 𝜋 a homomorphism from 𝐵 to ℐ. Let supp(𝑡) = 𝜋(𝐵) and out(𝑡) = 𝜋𝑅(𝐻), where 𝜋𝑅 extends 𝜋 by mapping all 𝑧 ∈ ¯ 𝑧 to the fresh variable 𝑧𝑡 that is unique for 𝑧 and 𝑡. A derivation from a KB ⟨ℛ, ℐ⟩ is a sequence 𝒟 = (∅, ℐ0), (𝑡1, ℐ1), . . . such that:

1. Every ℐ𝑖 in 𝒟 is an instance; moreover, ℐ0 = ℐ.
2. Every 𝑡𝑖 in 𝒟 is a trigger ⟨𝑅, 𝜋⟩ on ℐ𝑖-1 such that 𝑅 ∈ ℛ, out(𝑡𝑖) ̸⊆ ℐ𝑖-1, and ℐ𝑖 = ℐ𝑖-1 ∪ out(𝑡𝑖).

The result res(𝒟) of 𝒟 is the union of all instances in 𝒟, and trigs(𝒟) is the set of all triggers in 𝒟.

Different chase variants build specific derivations according to different criteria of trigger applicability. Below, the letters O, SO, R, and E respectively refer to the oblivious, semioblivious, restricted, and equivalent 1 variants.

Definition 4 (Applicability). A trigger 𝑡 = ⟨𝑅, ℎ⟩ on an instance ℐ is O-applicable on ℐ if out(𝑡) ̸⊆ ℐ; SO-applicable on ℐ if out(𝑡′ ) ̸⊆ ℐ for every trigger 𝑡′ = (𝑅, 𝜋′ ) with 𝜋(fr(𝑅)) = 𝜋′ (fr(𝑅)); R-applicable on ℐ if there is no retraction from ℐ ∪ out(𝑡) to ℐ; E-applicable on ℐ if there is no homomorphism from ℐ ∪ out(𝑡) to ℐ.

Example 1. Consider the KB 𝒦 = ⟨ℛ, ℐ⟩ with ℛ = {𝑅 = P(𝑥, 𝑦) → ∃𝑧 P(𝑦, 𝑧), P(𝑧, 𝑧)} and ℐ = {P(𝑎, 𝑎)} for some 𝑎. The trigger 𝑡1 = (𝑅, {𝑥 ↦→ 𝑎, 𝑦 ↦→ 𝑎}), whose output is out(𝑡1) = {P(𝑎, 𝑧𝑡1 ), P(𝑧𝑡1 , 𝑧𝑡1 )}, is O and SO-applicable on ℐ but not R or E-applicable, since there is a retraction from ℐ ∪ out(𝑡1) to ℐ that maps 𝑧𝑡1 to 𝑎.

Definition 5 (X-Chase). For an X ∈ {O, SO,R, E}, an Xderivation from a KB 𝒦 = ⟨ℛ, ℐ⟩ is a derivation 𝒟 such that every trigger 𝑡𝑖 ∈ trigs(𝒟) is X-applicable on ℐ𝑖. An X-derivation 𝒟 is fair if for every ℐ𝑖 occurring in 𝒟 and Xapplicable trigger 𝑡 on ℐ𝑖, there is some 𝑗 > 𝑖 such that 𝑡 is not X-applicable on ℐ𝑗. An X-derivation is terminating if it is fair and finite.

The result of any fair X-derivation is a universal model of the KB, for X ∈ {O, SO,R}, and has a retraction to a universal model for X = E. Therefore, we obtain:

Proposition 6. Consider a BCQ 𝑞, a KB 𝒦, and some fair Xderivation 𝒟 from 𝒦 where X ∈ {O, SO, R, E}. Then, 𝒦 |= 𝑞 iff res(𝒟) |= 𝑞.

These chase variants induce abstract classes, whose relationship is summarized in [Carral et al., 2022].

Definition 7 (Chase-Terminating Sets). For an X ∈ {O, SO,R, E}, let CTX∀ (resp. CTX∃ ) be the set of all rule sets ℛ such that every (resp. some) fair X-derivation from every KB ⟨ℛ, ℐ⟩ is finite.

Proposition 8. For all X ∈ {O, SO, E}, CTX∀ = CTX∃ , and CTO∀ ⊂ CTSO ∀ ⊂ CTR∀ ⊂ CTR∃ ⊂ CTE∀ .

Example 2. Consider the KB 𝒦 = ⟨ℛ, ℐ⟩ from Example 1. All fair O- or SO-derivations from 𝒦 are infinite. The only fair R and E-derivation from 𝒦 is 𝒟 = (∅, ℐ). Any fair Rderivation from a KB with ℛ is finite and hence, ℛ ∈ CTR∀ (and thus ℛ ∈ CTE∀ ).

bts The class bts is defined from the notion of treewidth and contains CTX𝑄 for all X ∈ {O, SO, R, E} and 𝑄 ∈ {∃, ∀} [Calì et al., 2013]. We only introduce a sufficient condition for a rule set not to be bts. Given a binary predicate P, the P-graph of an instance ℐ is the directed graph (adom(ℐ), 𝐸) where (𝑎, 𝑏) ∈ 𝐸 if and only if P(𝑎, 𝑏) ∈ ℐ.

Proposition 9. If there is an infinite clique in the P-graph of res(𝒟) for some binary predicate P and derivation 𝒟 from 𝒦 = ⟨ℐ, ℛ⟩, then ℛ is not bts.

1 The equivalent chase, like the better-known core chase, halts exactly when the KB has a finite universal model [Delivorias et al., 2021], while being monotonic (∀𝑖, ℐ𝑖 ⊆ ℐ𝑖+1).

2.1 Three-Counter Machines

A three-counter machine (3CM) ℳ is essentially a twocounter automaton augmented with a strictly increasing time counter. Formally, it is a tuple ⟨𝑄, 𝑞1, 𝛿⟩ where 𝑄 is a finite set of states including the initial state 𝑞1, and 𝛿 : 𝑄× {0, 1}2 → 𝑄 × {-1, 0, 1}2 is a transition function. A configuration of ℳ is a tuple ⟨𝑞, 𝑣1, 𝑣2, 𝑡⟩ where 𝑞 ∈ 𝑄 is the current state and 𝑣1, 𝑣2, 𝑡 ∈ N are the values of the three counters. The initial configuration of ℳ is ⟨𝑞1, 0, 0, 0⟩. Given a configuration 𝐶 = ⟨𝑞, 𝑣1, 𝑣2, 𝑡⟩, we define next(𝐶) = ⟨𝑞′ , 𝑣′1 , 𝑣′2 , 𝑡+1⟩ where 𝛿(𝑞, 𝑏1, 𝑏2) = ⟨𝑞′ , 𝑑1, 𝑑2⟩ where 𝑏𝑖 = 0 if 𝑣𝑖 = 0 and 𝑏𝑖 = 1 otherwise, and 𝑣′𝑖 = max(𝑣𝑖 + 𝑑𝑖, 0) for 𝑖 ∈ {1, 2}. Note that next is a partial function since 𝛿 may be undefined for some inputs. A 3CMℳhalts if there is a finite sequence of configurations 𝐶0, . . . , 𝐶𝑛 such that 𝐶0 is the initial configuration, 𝐶𝑖+1 = next(𝐶𝑖) for every 0 ≤ 𝑖 < 𝑛, and next(𝐶𝑛) is undefined. The halting problem for 3CMs is undecidable [Minsky, 1967].

3 The Rule Set

We define the class 𝒞 = {ℛℳ | ℳa 3CM}, using the rule set ℛℳ given in Figure 1. As it is recognizable in linear time, it is indeed a concrete class. The rule set ℛℳ is a adapted from the one used to prove Theorem 1 in [Gogacz and Marcinkowski, 2014], stating that all-instance chase termination is undecidable for the oblivious chase. It provides a reduction from the halting problem for 3CMs to chase termination.

Roughly speaking, the chase on KB ⟨{End(𝑤)},ℛℳ⟩ looks like a sequence of elements connected through a binary predicate S, ending in the "well of positivity" 𝑤. Each element in the chase runs its own private computation of ℳ, and is only allowed to generate a predecessor if the simulation of ℳgoes on for long enough. Consequently, this chain of elements is infinite if and only if ℳdoes not halt. To elaborate, we first need to explain howℳ can be simulated by a sequence of natural numbers.

Following Section 3.3 in [Gogacz and Marcinkowski, 2014], there is a way to encode configurations of a 3CMℳ as natural numbers using prime factorization. Let 𝑝1, 𝑝2, . . . be the sequence of prime numbers, and 𝑄 = {𝑞1, . . . , 𝑞𝑚}. Then, a configuration ⟨𝑞𝑖, 𝑣1, 𝑣2, 𝑡⟩ of ℳ is encoded as the natural number

In particular, the initial configuration ⟨𝑞1, 0, 0, 0⟩ is encoded as 2 = 𝑝1. Let 𝑝 = 𝑝1 . . . 𝑝𝑚+3.

Proposition 10. There exist natural numbers 𝑞𝑖, 𝑟𝑖 for all 1 ≤ 𝑖 ≤ 𝑝 such that 𝑞𝑖 𝑟𝑖 is irreducible, and for any configuration 𝐶 of ℳ such that 𝑖 = enc(𝐶) mod 𝑝, if next(𝐶) is defined, then enc(next(𝐶)) = 𝑞𝑖 𝑟𝑖 · enc(𝐶), and 𝑞𝑖 𝑟𝑖 · enc(𝐶) = enc(𝐶) otherwise.

For further details, we refer the reader to Theorem 5 in [Gogacz and Marcinkowski, 2014]. Let 𝑔 be the function defined as 𝑔(𝑛) = 𝑞𝑛 mod 𝑝 𝑟𝑛 mod 𝑝 · 𝑛. Then, next(𝐶) is defined if and only if 𝑔(enc(𝐶)) ̸= enc(𝐶), and in that case enc(next(𝐶)) = 𝑔(enc(𝐶)). Let 𝒢 = {𝑔𝑖 (2) | 𝑖 ∈ N}.

Figure 1: Rules in ℛℳ for all 𝑖 < 𝑝. In Rule 𝑅R,𝑖, R𝑝 is interpreted as R0. S𝑛 (𝑥, 𝑦) denotes an S-path of length 𝑛 from 𝑥 to 𝑦.

Since the third counter always increases when a subsequent configuration exists, we get the following.

Proposition 11. ℳhalts iff 𝒢 is bounded.

Then, as mentioned earlier, the chase is shaped as a sequence of elements that form a chain connected by predicates S, where S(𝑥, 𝑦) means that 𝑦 thinks it is the successor of 𝑥. The use of "thinks" is intentional, as we run a simulation of ℳ from the point of view of each element. All predicates used for the simulation (G, R𝑖 and T𝑖) feature this element in first position, which thinks itself as 0. The atom G(𝑥, 𝑦) signifies that from the point of view of 𝑥, the number represented by 𝑦 belongs to 𝒢. This relation is computed according to Proposition 10, using Rules 𝑅init G and 𝑅step G,𝑖 . Specifically, the initial configuration is encoded by 2, represented by the second successor of each element (Rule 𝑅init G ). Rule 𝑅step G,𝑖 then implements the transition to the next configuration using predicates R𝑖 and T𝑖. The atom R𝑖(𝑥, 𝑦) indicates that, from 𝑥's perspective, the number represented by 𝑦 has a remainder of 𝑖 modulo 𝑝, as generated by Rule 𝑅R,𝑖. Similarly, T𝑖(𝑥, 𝑦, 𝑧) implies that 𝑦𝑧 = 𝑟𝑖 𝑞𝑖 from 𝑥's perspective. This is ensured by Rule 𝑅T,𝑖, which implements multiplication by successive additions. These predicates are initialized for each element 𝑥 by Rule 𝑅∃. This rule allows an element 𝑦 to create a predecessor 𝑥 (specifically S0(𝑥, 𝑦), which implies S(𝑥, 𝑦) via Rule 𝑅S) if the simulation of ℳ from 𝑦 reaches the well of positivity 𝑤 (i.e., when G(𝑦, 𝑧) and End(𝑧) hold for some 𝑧). This process is illustrated in Figure 2 for predicate T𝑖.

The reduction described so far mirrors the one in [Gogacz and Marcinkowski, 2014]. However, the same reduction does not work here. First, it applies only to the oblivious chase; the restricted and equivalent chases always terminate, even ifℳdoes not halt. Second, arguing that BCQ entailment is decidable is difficult (and likely false) because the predicates R𝑖, T𝑖, and G lack structure. We introduce two modifications to address these issues.

First, to accommodate all chase variants, we introduce predicates S0 and End, which derive S via Rules 𝑅S and 𝑅End S . In particular, S0 has no self-loop over the well of positivity 𝑤 (where End(𝑤) holds, at the end of the chain), preventing any attempt at homomorphically embedding the whole chain into 𝑤. Thus, even the equivalent chase is forced to create an infinite chain if ℳ does not halt.

Second, to make BCQ entailment decidable, we employ a flooding mechanism using the predicate Flood, with Rules 𝑅gen flood and 𝑅prop flood . This ensures that once the simulation from 𝑥 reaches 𝑤 and generates a predecessor, 𝑥 connects to all its successors via R𝑖, T𝑖, and G. As a result, all elements whose simulation reaches the well of positivity show the same behavior regarding BCQ answering, except for predicates S0, S and End which are easier to handle.

4 Undecidability of Chase Termination and bts-Recognition

This section is devoted to Points 1 and 2 of Theorem 1, which are the negative properties of our class: chase termination for all chase variants and bts are both undecidable in 𝒞. Regarding Oblivious and Semi-Oblivious chase termination, this is mostly guaranteed by construction, as we adapted the class proposed in [Gogacz and Marcinkowski, 2014] that already had these properties. Remarkably, our set of rules also exhibits this behavior for the equivalent chase. To prove this, we make use of Proposition 8 as much as possible. More precisely, we show that ifℳdoes not halt, then the equivalent chase does not terminate on ℛℳ and some specific instance ℐE (Theorem 14), and that ifℳdoes halt, then the oblivious chase terminates on the so-called critical instance, and thus on all instances (Theorem 16). These two results, along with Proposition 8 and the undecidability of the halting problem for 3CMs entail that chase termination is undecidable for 𝒞. The undecidable bts recognition is then a consequence of the above, joint with our freshly added flooding mechanism.

In this section, X always denotes an element of {O, SO, R, E}. We denote the result of some fair X-derivation from ℐ,ℛwith ChX(ℐ,ℛ). Note that this object is not unique in general, as different derivations may produce different results. This is however not an issue for our purpose, since we do not really consider the restricted chase in proofs, and it is the only variant for which the order of application of triggers matters. It will also be convenient to consider the chase as an alternation of closing under Datalog rules and then under non-Datalog rules. We define ChX0 (ℐ) = ChX(ℐ,ℛ∀ℳ) and for all 𝑖 ≥ 0, ChX𝑖+1 (ℐ) = ChX(ChX(ChX𝑖 (ℐ),ℛ∃ℳ),ℛ∀ℳ), where ℛ∀ and ℛ∃ denote the sets of Datalog and non-Datalog rules in ℛ, respectively. Note that this process still induces a fair derivation.

4.1 Non-Termination of the Chase

We first prove that if ℳdoes not halt, then ℛℳ /∈ CTX𝑄 for 𝑄 ∈ {∀, ∃}, by considering only the instance ℐE = {End(𝑤)}. Before proving this, we need two lemmas about the structure of the chase.

Lemma 12. For all 𝑛 > 0, if ChX𝑛 (ℐE) ̸= ChX𝑛-1 (ℐE), then adom(ChX𝑛 (ℐE)) = {𝑡0, . . . , 𝑡𝑛-1,𝑤} for some terms 𝑡0, . . . , 𝑡𝑛-1, and the S0-atoms of ChX𝑛 (ℐE) are exactly { S0(𝑡𝑖, 𝑡𝑖+1) | 0 ≤ 𝑖 < 𝑛 } where 𝑡𝑛 = 𝑤.

Proof sketch. By induction on 𝑛. Both the base case and inductive step follow from the fact that there is a single existential rule, and thus the only way for ChX𝑛 (ℐE) to be different from ChX𝑛-1 (ℐE) is for Rule 𝑅∃ to be applied. This rule features a single frontier variable, which has to be mapped to the term created at the previous step.

In the following lemma, proven by a simple induction, we refer to terms of ChX𝑛 (ℐE) as 𝑡0, . . . , 𝑡𝑛-1 as in Lemma 12. We also use 𝑡𝑖 for 𝑖 ≥ 𝑛 to refer to 𝑤. Note that even for such 𝑖's, S(𝑡𝑖, 𝑡𝑖+1) ∈ ChX𝑛 (ℐE).

• (i) R𝑖(𝑡0, 𝑡𝑘) ∈ ChX𝑛 (ℐE) if and only if 𝑘 = 𝑖 mod 𝑝;
• (ii) T𝑖(𝑡0, 𝑡𝑘, 𝑡𝑙) ∈ ChX𝑛 (ℐE) if and only if there is 𝑚 such that 𝑘 =𝑚𝑟𝑖 and 𝑙 =𝑚𝑞𝑖;
• (iii) For all 𝑘 ∈ N, G(𝑡0, 𝑡𝑔𝑘 (2)) ∈ ChX𝑛 (ℐE);
• (iv) If 𝒢 is bounded by 𝑛-1, then for all 𝑙 such that G(𝑡0, 𝑡𝑙) ∈ ChX𝑛 (ℐE), there is 𝑘 such that 𝑙 = 𝑔𝑘 (2).

Theorem 14. If ℳ does not halt, there is no terminating X-chase sequence from ⟨{End(𝑤)},ℛℳ⟩.

Proof sketch. We simply prove by induction on 𝑛 that if ℳ does not halt and ChX𝑛 (ℐE) ̸= ChX𝑛-1 (ℐE), then Rule 𝑅∃ is Eapplicable on ChX𝑛 (ℐE). In this case, ChX𝑛 (ℐE) is as described in Lemma 12. Then, by Proposition 11, 𝒢 is unbounded, so G(𝑡0,𝑤) ∈ ChX𝑛 (ℐE) by Item (iv) of Lemma 13. As the S0-atoms of ChX𝑛 (ℐE) are exactly { S0(𝑡𝑖, 𝑡𝑖+1) | 0 ≤ 𝑖 < 𝑛 }, there is no way to homomorphically map the result of applying 𝑅∃ into ChX𝑛 (ℐE), so this rule is indeed E-applicable.

4.2 Termination of the Chase

To prove that the X-chase terminates ifℳhalts (Theorem 16), it suffices to prove that in this case, the oblivious chase terminates on the so-called critical instance. The critical instance is the instance containing a single constant 𝑤, and in which all possible facts over the schema of the rule set are present. Indeed, if the oblivious chase terminates on the critical instance, it terminates on all instances [Marnette, 2009], and thus all chase variants terminate too via Proposition 8. Let 𝒥 be the critical instance for the schema of ℛℳ, and 𝒥𝑛 = ChX𝑛 (𝒥).

Proof sketch. By induction on 𝑛. The base case is obtained using Rules 𝑅End S , 𝑅prop flood and 𝑅gen flood . For the inductive step, the additional S0-atom of 𝒥𝑛 can only produce S(𝑤, 𝑤), which already belongs to 𝒥. Thus, both instances feature the same applicable triggers.

Theorem 16. If ℳ halts, then the X-chase terminates on ⟨ℐ,ℛℳ⟩ for all instances ℐ.

Proof sketch. If ℳ halts, then 𝒢 is bounded by 𝑛 and by Items (iii) and (iv) of Lemma 13, G(𝑡0,𝑤) /∈ 𝒥𝑛+1. Thus, Rule 𝑅∃ is not applicable on 𝒥𝑛+1, which entails the result as discussed before Lemma 15.

4.3 Treewidth

We then prove that bts-membership in 𝒞 is undecidable.

Theorem 17. ℛℳ is bts if and only if ℳhalts.

If ℳhalts, then by Theorem 16, the X-chase terminates, so the rule set is clearly bts. The converse direction is a direct consequence of the flooding mechanism.

Lemma 18. Ifℳdoes not halt, then there is an infinite clique in the R0-graph of ChX({End(𝑤)}, ℛℳ).

Proof. Assumeℳdoes not halt. By Theorem 14, for all 𝑛, ChX𝑛 (ℐE) ̸= ChX𝑛-1 (ℐE), so by Lemma 12, there is an infinite sequence of terms 𝑢0, 𝑢1, . . . such that 𝑢0 = 𝑤, and for all 𝑖 ≥ 0, S(𝑢𝑖+1, 𝑢𝑖) ∈ ChX({End(𝑤)}, ℛℳ). By Rule 𝑅prop flood , for all 𝑖, 𝑗 ≥ 0, Flood(𝑢𝑖) ∈ ChX({End(𝑤)},ℛℳ), so by Rule 𝑅gen flood , R0(𝑢𝑖, 𝑢𝑗) is also in the chase result, so the R0graph contains an infinite clique.

Lemma 18 and Proposition 9 conclude the proof.

5 Decidability of BCQEntailment

We now turn to decidability of BCQ entailment, that is Point 3 of Theorem 1. Consider an instance ℐ, a set of rules ℛℳ from our class 𝒞 constructed in Section 3, and a BCQ 𝑞. To decide whether ⟨ℐ,ℛℳ⟩ |= 𝑞, our algorithm computes the result of the semi-oblivious chase up to depth 𝑀 := 2 |𝑞| + 1, that is ChSO 𝑀 (ℐ), and then checks whether ChSO 𝑀 (ℐ) |= 𝑞. This clearly terminates as we only require to apply finitely many rules in the first step, and then evaluate a usual BCQ on a finite instance in the second step. It remains to prove the correctness:

The rest of this section is devoted to proving the above. We first define ℐ𝑛 := ChSO 𝑛 (ℐ) for all 𝑛, and ℐ∞ := ⋃︀𝑛≥0 ℐ𝑛. The successive ℐ𝑛 again induce a fair derivation, therefore ℐ∞ is a universal model of ⟨ℐ,ℛℳ⟩. Thus, Lemma 19 can be rephrased as ℐ∞ |= 𝑞 iff ℐ𝑀 |= 𝑞 using Proposition 6. With this formulation, the 'if' direction is the easiest one: indeed, if ℐ𝑀 |= 𝑞, we get ℐ∞ |= 𝑞 from the fact that ℐ∞ contains ℐ𝑀.

We now turn to proving the 'only-if' direction of Lemma 19. Assume ℐ∞ |= 𝑞. Compactness guarantees that there exists 𝑁 such that ℐ𝑁 |= 𝑞. If 𝑁 ≤ 𝑀, we are done since ℐ𝑁 ⊆ ℐ𝑀. Otherwise, if 𝑁 > 𝑀, consider a homomorphism ℎ from 𝑞 to ℐ𝑁. We want to construct a homomorphism ℎ′ : 𝑞 → ℐ𝑀 based on ℎ. Our main issue is atoms that ℎ maps to ℐ𝑁 ∖ ℐ𝑀, for which we need to find replacements within ℐ𝑀.

Intuitively, we distinguish between the End-atoms (which cannot be introduced during the chase), the S0-atoms, the Satoms, and the others. Indeed, apart fromwithin the original instance ℐ, the S0- and S-atoms form chains ending on some element from adom(ℐ). Therefore, if ℎ involves such S0- and S-atoms from ℐ𝑁 ∖ ℐ𝑀, we know they lie along a chain, say at distance ℓ to ℐ. We can then prove that a sufficient part of this chain already belongs to ℐ𝑀, due to 𝑀 ≥ 2 |𝑞|. To build ℎ′ , we can thus 'shift' ℎ by ℓ -𝑀 atoms to use instead this part of the chain. Furthermore, we can establish that every term from ℐ𝑁 lies on such a chain, therefore, when we shift our homomorphism along the chain, due to the combination of Rules 𝑅prop flood and 𝑅gen flood , all the P-atoms are present for P /∈ {End, S0, S}. The only exception is when such a P-atom features a term 𝑡 that is the starting point of a chain (thus Rule 𝑅prop flood may not trigger on 𝑡) and that ℓ ≤ 𝑀 (so that we don't shift). But ℓ ≤ 𝑀 guarantees the atom already belongs to ℐ𝑀 .

We summarize considerations on S0- and S-atoms in the next lemma, whose proof is a simple induction:

Lemma 20. For all 𝑛 ≥ 0 and 𝑎 ∈ adom(ℐ), there exist integers 0 ≤ 𝑚𝑎 ≤ 𝑛 s.t.: (i) the domain of ℐ𝑛 consists of distinct terms 𝑎𝑖 with 𝑎 ∈ adom(ℐ) and 0 ≤ 𝑖 ≤ 𝑚𝑎, and where 𝑎0 = 𝑎; and (ii) S0 atoms of ℐ𝑛 are exactly:

and, as a corollary, the S atoms of ℐ𝑛 are exactly:

Note that the above echoes Lemma 12, except that the end point can now be any element from the original instance ℐ. Notice that using the semi-oblivious chase also prevents branching: each element from adom(ℐ) can only be the end point of one such chain of fresh elements. The result of the chase is depicted in Figure 3.

We now clarify that, as the chase progresses, new facts either stem from the flooding mechanism or involve one of the freshly introduced starting points of a chain.

Lemma 21. Let 𝑛 ≥ 0 and P(𝑡1, . . . , 𝑡𝑚) an atom. If P(𝑡1, . . . , 𝑡𝑚) ∈ ℐ𝑛+1 ∖ ℐ𝑛 then one of the following holds:

1. 𝑡1 ∈ adom(ℐ𝑛+1) ∖ adom(ℐ𝑛) and there are 𝑘2,. . . , 𝑘𝑚 ≥ 0 s.t. S𝑘2 (𝑡1, 𝑡2), . . . , S𝑘𝑚 (𝑡1, 𝑡𝑚) ∈ ℐ𝑛+1, where S𝑘 (𝑥, 𝑦) denotes an S-path of size 𝑘 from 𝑥 to 𝑦.
2. for every 1 ≤ 𝑖 ≤𝑚, we have Flood(𝑡𝑖) ∈ ℐ𝑛+1.

Proof sketch. Apart from Rules 𝑅prop flood and 𝑅gen flood that relate to the flooding, notice that the first term occurring in an atom of some head also appears as the first term in an atom from the body. The rest follows by induction.

The above guarantees that any element 𝑎𝑖, as described in Lemma 20, appears exactly at depth 𝑖 in the chase:

Lemma 22. Let 𝑎𝑖 be a term from adom(ℐ𝑛) as described in Lemma 20, thus with 𝑖 ≤ 𝑛. We have 𝑎𝑖 ∈ adom(ℐ𝑖).

Proof sketch. We proceed by induction on 𝑖. For 𝑎0, the claim is trivial as 𝑎0 ∈ adom(ℐ). For 𝑎𝑖+1, we know it is introduced by applying Rule 𝑅∃ on 𝑎𝑖 (mapping 𝑦 to 𝑎𝑖), thus relying on an atom G(𝑎𝑖, 𝑒) to be satisfied for some End(𝑒) ∈ ℐ. Using Lemma 21, one can establish that G(𝑎𝑖, 𝑒) ∈ ℐ𝑖, thus 𝑎𝑖+1 is introduced at step 𝑖 + 1.

To proceed with the construction of homomorphism ℎ′ : 𝑞 → ℐ𝑀 as previously sketched. We thus decompose the homomorphism ℎ : 𝑞 → ℐ𝑁 to identify which parts of 𝑞 are mapped along S0-S-chains. To do so, we define the {S0, S}- graph of an instance 𝒥 : its nodes are elements of adom(𝒥 ) and there is an edge from 𝑎 to 𝑏 if and only if S0(𝑎, 𝑏) or S(𝑎, 𝑏) belongs to 𝒥 . We denote this graph by 𝐺𝒥S,S0 . We then consider weakly connected components (WCC) of this graph. Two terms 𝑎 and 𝑏 are in the same WCC if there is an undirected path from 𝑎 to 𝑏 in 𝐺𝒥S,S0 .

We now come back to defining ℎ′ . Let 𝑉1, . . . , 𝑉ℓ be the WCCs of 𝐺𝑞S,S0 . We apply Lemma 20 to ℐ𝑁 and obtain the terms as described in its statement. For each 1 ≤ 𝑙 ≤ ℓ, let 𝑑𝑙 be the minimum 𝑑 such that ℎ(𝑣) = 𝑎𝑑 for some 𝑣 ∈ 𝑉𝑙 and 𝑎 ∈ adom(ℐ). We define the mapping ℎ′ : Vars(𝑞) → adom(ℐ𝑀) by 'shifting' each WCC forward along the chain it lies on, unless it is already close to ℐ:

We first verify that ℎ′ indeed maps elements within adom(ℐ𝑀). Consider a variable 𝑣 of 𝑞 and let 𝑉𝑙 be its WCC in 𝐺𝑞S,S0 . Let 𝑣𝑚𝑖𝑛 be the variable of 𝑉𝑙 that realizes 𝑑𝑙, for which ℎ(𝑣𝑚𝑖𝑛) = 𝑎𝑑𝑙 for some 𝑎 ∈ adom(ℐ). By definition of 𝑉𝑙, there exists an undirected (simple) path in 𝐺𝑞S,S0 from 𝑣 to

𝑣𝑚𝑖𝑛, whose length is at most |𝑞|. From ℎ being a homomorphism, the atoms that form this path are mapped via ℎ on atoms described by Lemma 20. It is thus clear that ℎ(𝑣) is some 𝑎𝑖 for 𝑎 ∈ adom(ℐ) and 0 ≤ 𝑖 ≤ 𝑑𝑙 + |𝑞|. Now, if 𝑑𝑙 ≤ |𝑞|, then ℎ′ (𝑣) = ℎ(𝑣) = 𝑎𝑖 and we have 𝑖 ≤ 2 |𝑞|. Otherwise ℎ′ (𝑣) = 𝑎𝑖-𝑑𝑙 and 𝑖 - 𝑑𝑙 ≤ |𝑞| ≤ 2 |𝑞|. In both cases, Lemma 22 warrants ℎ′ (𝑣) ∈ adom(ℐ𝑀).

We now claim that ℎ′ is a homomorphism from 𝑞 to ℐ𝑀. Let us denote the restriction of ℐ𝑁 to adom(ℐ𝑛) for some 𝑛 ≤ 𝑁 by ℐ𝑁|𝑛. We actually prove that ℎ′ is a homomorphism from 𝑞 to ℐ𝑁|𝑀-1. This is sufficient as all atoms from ℐ𝑁 that only involve terms from adom(ℐ𝑀-1) are already in ℐ𝑀. This is stated in the following lemma, whose proof is by induction and heavily relies on the previous lemmas:

Lemma 23. For every 𝑛 ≥ 𝑀, ℐ𝑛|𝑀-1 = ℐ𝑀|𝑀-1. In particular, for 𝑛 = 𝑁 we have ℐ𝑁|𝑀-1 = ℐ𝑀|𝑀-1.

We finally prove that ℎ′ is a homomorphism from 𝑞 to ℐ𝑁|𝑀-1. Since End-atoms cannot be introduced during the chase, any End-atom End(𝑡) is mapped through ℎ to an atom of ℐ, and thus ℎ′ (𝑡) = ℎ(𝑡), so End(ℎ′ (𝑡)) ∈ ℐ𝑁|𝑀-1. The case of S0- and S-atoms is also easy: consider an atom P(𝑡, 𝑡′ ) ∈ 𝑞 for P ∈ {S0, S}. By definition, 𝑡 and 𝑡′ belong to a same WCC 𝑉𝑙. If ℎ and ℎ′ coincide on 𝑉𝑙 (that is the case if 𝑑𝑙 ≤ |𝑞|), then P(ℎ′ (𝑡), ℎ′ (𝑡′ )) immediately belongs to ℐ𝑀 via Lemma 23. Otherwise, ℎ(𝑡) = 𝑎𝑖 and ℎ(𝑡′ ) = 𝑎𝑗 for some 𝑎 ∈ adom(ℐ) and 𝑖, 𝑗 such that 𝑖 = 𝑗 + 1 or 𝑖 = 𝑗 - 1 by Lemma 20. Thus, ℎ′ (𝑡) = 𝑎𝑖-𝑑𝑙 and ℎ′ (𝑡′ ) = 𝑎𝑗-𝑑𝑙 , and 𝑖-𝑑𝑙 and 𝑗-𝑑𝑙 satisfy the same relation and are smaller than 𝑀, so P(ℎ′ (𝑡), ℎ′ (𝑡′ )) belongs to ℐ𝑀.

It remains to treat the case of atoms based upon other predicates. Consider an atom P(𝑡1, . . . , 𝑡𝑚) ∈ 𝑞 for some P /∈ {S0, S} of arity 𝑚. Since ℎ is a homomorphism, we have P(ℎ(𝑡1), . . . , ℎ(𝑡𝑚)) ∈ ℐ𝑁. If all ℎ(𝑡𝑖) ∈ adom(ℐ), then all ℎ′ (𝑡𝑖) = ℎ(𝑡𝑖) and we are done. Otherwise, we can apply Lemma 21. In the case where ℎ(𝑡𝑖) are all flooded, then so are the ℎ′ (𝑡𝑖) and Rule 𝑅gen flood concludes. Otherwise, all ℎ(𝑡𝑖) belong to the same WCC 𝑉𝑙. Again, if 𝑑𝑙 ≤ |𝑞|, then ℎ′ and ℎ coincide on 𝑉𝑙 and we are done. Otherwise, all 𝑡𝑖's map to some 𝑎𝑘𝑖 for 𝑎 ∈ adom(ℐ) and 𝑘𝑖 < 𝑚𝑎, since 𝑎𝑘𝑖+𝑑𝑙 ∈ adom(ℐ𝑁). Thus, by Rule 𝑅prop flood , ℎ′ (𝑡𝑖) is flooded, and thus again Rule 𝑅gen flood concludes.

6 Conclusion

We have shown that decidable BCQ entailment does not imply the decidability of bts membership or chase termination for concrete classes of existential rules. This explains the necessity of diverse, class-specific techniques for proving termination, as BCQ entailment offers no systematic tool for this purpose. Future work includes proving that entailment of recursive C2RPQs is also decidable for the class presented here. Conversely, it remains an open problem to identify a homomorphism-closed query language whose decidable entailment is sufficient to guarantee the decidability of chase termination.

Acknowledgments

This work has been partially supported by ANR grant EXPAND (ANR-25-CE23-1215). The authors would like to thank David Carral who hinted this topic and provided useful insights. He still has not played Celeste, though.