Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Restricted Chase Termination: You Want More than Fairness

David Carral, Lukas Gerlach, Lucas Larroque, Michaël Thomazo

TL;DR

The paper addresses the fundamental problem of universal termination for the restricted chase under existential rules, showing that the problem sits at the high end of the analytical hierarchy with $\Pi_1^1$-hardness due to the fairness condition. It develops a TM-based reduction framework that encodes computation in a knowledge base using emergency brakes and bow-tie structures to relate infinite TM runs to nonterminating chase derivations. The main contributions establish $\Pi_1^1$-completeness for both knowledge-base and rule-set termination under the restricted chase, and propose a breadth-first derivation criterion as a finitely verifiable alternative to fairness that preserves semi-decidability. The findings have significant implications for the theory of chase termination and for practical reasoning under complex constraints, guiding both theoretical understanding and design of termination checks.

Abstract

The chase is a fundamental algorithm with ubiquitous uses in database theory. Given a database and a set of existential rules (aka tuple-generating dependencies), it iteratively extends the database to ensure that the rules are satisfied in a most general way. This process may not terminate, and a major problem is to decide whether it does. This problem has been studied for a large number of chase variants, which differ by the conditions under which a rule is applied to extend the database. Surprisingly, the complexity of the universal termination of the restricted (aka standard) chase is not fully understood. We close this gap by placing universal restricted chase termination in the analytical hierarchy. This higher hardness is due to the fairness condition, and we propose an alternative condition to reduce the hardness of universal termination.

Restricted Chase Termination: You Want More than Fairness

TL;DR

The paper addresses the fundamental problem of universal termination for the restricted chase under existential rules, showing that the problem sits at the high end of the analytical hierarchy with -hardness due to the fairness condition. It develops a TM-based reduction framework that encodes computation in a knowledge base using emergency brakes and bow-tie structures to relate infinite TM runs to nonterminating chase derivations. The main contributions establish -completeness for both knowledge-base and rule-set termination under the restricted chase, and propose a breadth-first derivation criterion as a finitely verifiable alternative to fairness that preserves semi-decidability. The findings have significant implications for the theory of chase termination and for practical reasoning under complex constraints, guiding both theoretical understanding and design of termination checks.

Abstract

The chase is a fundamental algorithm with ubiquitous uses in database theory. Given a database and a set of existential rules (aka tuple-generating dependencies), it iteratively extends the database to ensure that the rules are satisfied in a most general way. This process may not terminate, and a major problem is to decide whether it does. This problem has been studied for a large number of chase variants, which differ by the conditions under which a rule is applied to extend the database. Surprisingly, the complexity of the universal termination of the restricted (aka standard) chase is not fully understood. We close this gap by placing universal restricted chase termination in the analytical hierarchy. This higher hardness is due to the fairness condition, and we propose an alternative condition to reduce the hardness of universal termination.

Paper Structure

This paper contains 20 sections, 20 theorems, 11 equations, 3 figures, 1 table.

Table of Contents

  1. Introduction
  2. Preliminaries
  3. First-Order Logic
  4. The Chase
  5. Turing Machines
  6. Computability Theory
  7. $\Pi_1^1$-complete Turing Machine Problems for Reductions
  8. Non-Recurrence on the Empty Word
  9. Reductions between Turing Machine Problems
  10. Related Work
  11. Novel Notation
  12. Chase Termination in the General Case
  13. Chase Termination of Syntactic Fragments
  14. Knowledge base termination
  15. Schema
  16. ...and 5 more sections

Key Result

lemma 1

Checking if a computable $\omega$-tree is well founded is $\Pi_1^1$-complete.

Figures (3)

  • Figure 1: Three Different Restricted Chase Sequences for the KB $\textnormal{${\mathcal{K}}$}\xspace_1$ from \ref{['example:example-bicycle']}
  • Figure 2: An Infinite Restricted Chase Sequence of $\langle \Sigma\xspace_M, D_{0}\rangle$ where $M$ is the machine from \ref{['example:kb-reduction']}, and $\mathtt{AllPreds}\xspace_{\geq2}$ above is a shortcuts for "$\mathtt{F}$, $\mathtt{R}$, $\mathtt{\textnormal{${q_0}$}\xspace}$, $\mathtt{\textnormal{${q_r}$}\xspace}$, $\mathtt{0}$, $\mathtt{1}$, $\mathtt{\textnormal{${\mathtt{B}}$}\xspace}$, $\mathtt{C_R}$, $\mathtt{C_L}$, $\mathtt{nextBr}$".
  • Figure 3: First three steps of the restricted chase from $\textnormal{${\langle \textnormal{${\mathcal{R}}$}\xspace_M,D \rangle}$}\xspace$ as defined in \ref{['ex:rule_set_term_non_standard_db']}. The predicate $\mathtt{F}\xspace$ and the brakes are not represented for the sake of readability, but terms are connected through the future predicate to an element on the same line at the previous step. Unlabeled arrows represent $\mathtt{R}\xspace$-atoms.

Theorems & Definitions (38)

  • definition 1
  • definition 2
  • definition 3
  • definition 4
  • definition 5
  • definition 6
  • lemma 1: RogersArithmeticalHierarchy, Theorem 16
  • definition 7
  • lemma 2: pi_one_one_problems, Corollary 5.3
  • proposition 1
  • ...and 28 more