About the Multi-Head Linear Restricted Chase Termination

TL;DR

The paper tackles the termination problem of the restricted chase for linear multi-headed TGDs, a long-standing open question in database theory. It develops a three-layer strategy: (i) relate infinite restricted derivations to mixed oblivious/restricted derivations, (ii) introduce omega-sensitivity path derivations to capture derivation order constraints, and (iii) reduce the problem to a Monadic Second Order logic formulation on trees, enabling decidability. The authors prove that all-instances restricted termination is decidable for linear multi-headed rules, encapsulated in the class CT_∀∀. The approach relies on a forest-based representation, blocking and fairness analyses, and MSO decidability, with prospects for extending to guarded multi-headed cases and highlighting the potential for practical decision procedures.

Abstract

The chase is a ubiquitous algorithm in database theory. However, for existential rules (aka tuple-generating dependencies), its termination is not guaranteed, and even undecidable in general. The problem of termination becomes particularly difficult for the restricted (or standard) chase, for which the order of rule application matters. Thus, decidability of restricted chase termination is still open for many well-behaved classes such as linear or guarded multi-headed rules. We make a step forward by showing that all-instances restricted chase termination is decidable in the linear multi-headed case.

Figures (2)

• Figure 1: Section \ref{['sec:mixed']} in one picture. You can see a border trigger $\pi=(\rho, u)$: address $u$ is still in $\mathbb{R}_{}$ while both $u\rho_\iota$ are right behind the border. The pair $(v_1,v_2)$ of addresses in $\mathbb{R}_{}$ is a blocking team for $\pi$, and $v_\iota=btr(u\rho_\iota)$. One can also see that the tree rooted in $v_\iota$ contains (possibly among other addresses) a copy of the tree rooted in $u\rho_\iota$ (as Lemma \ref{['lem:prettier2']}(B) postulates).
• Figure 2: A visual guide to condition (ii) of Statement 2 from \ref{['th:mixed-to-properties-on-thetree']}. Node $w$ appears in $\mathsf{fragile}(u)$ and trigger $\pi_w = (\rho, w)$ is blocked by a team of nodes $(v,v')$ represented with red dashed edges. Bold-blue path represents $\mathbb{P}^{\textnormal{\tiny 0}}$, blue square nodes are $\mathsf{bfr}(w)$, red diamond nodes are $\mathsf{any}(u)$.

Theorems & Definitions (56)

• Example 1
• Example 2
• Definition 4: Addresses
• Definition 5: Forests
• Definition 6: Rule application
• Definition 7
• Definition 8: Materialization
• Definition 9
• Definition 10: Triggers
• Definition 11: Trigger blocking