Table of Contents
Fetching ...

Chase Termination Beyond Polynomial Time

Philipp Hanisch, Markus Krötzsch

TL;DR

This work proposes a new criterion that explicitly allows some such cycles in the chase process, and yet ensures termination of the standard chase under reasonable conditions, which leads to new decidable fragments of tgds that are not only syntactically more general but also strictly more expressive than the fragments defined by prior acyclicity conditions.

Abstract

The chase is a widely implemented approach to reason with tuple-generating dependencies (tgds), used in data exchange, data integration, and ontology-based query answering. However, it is merely a semi-decision procedure, which may fail to terminate. Many decidable conditions have been proposed for tgds to ensure chase termination, typically by forbidding some kind of "cycle" in the chase process. We propose a new criterion that explicitly allows some such cycles, and yet ensures termination of the standard chase under reasonable conditions. This leads to new decidable fragments of tgds that are not only syntactically more general but also strictly more expressive than the fragments defined by prior acyclicity conditions. Indeed, while known terminating fragments are restricted to PTime data complexity, our conditions yield decidable languages for any k-ExpTime. We further refine our syntactic conditions to obtain fragments of tgds for which an optimised chase procedure decides query entailment in PSpace or k-ExpSpace, respectively.

Chase Termination Beyond Polynomial Time

TL;DR

This work proposes a new criterion that explicitly allows some such cycles in the chase process, and yet ensures termination of the standard chase under reasonable conditions, which leads to new decidable fragments of tgds that are not only syntactically more general but also strictly more expressive than the fragments defined by prior acyclicity conditions.

Abstract

The chase is a widely implemented approach to reason with tuple-generating dependencies (tgds), used in data exchange, data integration, and ontology-based query answering. However, it is merely a semi-decision procedure, which may fail to terminate. Many decidable conditions have been proposed for tgds to ensure chase termination, typically by forbidding some kind of "cycle" in the chase process. We propose a new criterion that explicitly allows some such cycles, and yet ensures termination of the standard chase under reasonable conditions. This leads to new decidable fragments of tgds that are not only syntactically more general but also strictly more expressive than the fragments defined by prior acyclicity conditions. Indeed, while known terminating fragments are restricted to PTime data complexity, our conditions yield decidable languages for any k-ExpTime. We further refine our syntactic conditions to obtain fragments of tgds for which an optimised chase procedure decides query entailment in PSpace or k-ExpSpace, respectively.
Paper Structure (11 sections, 39 theorems, 13 equations, 2 figures, 1 algorithm)

This paper contains 11 sections, 39 theorems, 13 equations, 2 figures, 1 algorithm.

Key Result

lemma 1

If $n_1\stackrel{y}{\twoheadrightarrow}n_2$ in $\text{\sf{chase}}(\Sigma,\mathcal{D})$ for nulls $n_1,n_2\in\mathbf{N}$, then there is an edge $\text{\sf{var}}(n_1)\stackrel{y}{\to}\text{\sf{var}}(n_2)$ in $\text{\sf{LXG}}(\Sigma)$.

Figures (2)

  • Figure 1: Dependency cycle in $\text{\sf{LXG}}(\Sigma)$ (left) and corresponding chain of derived nulls in $\text{\sf{chase}}(\Sigma,\mathcal{D})$ (right); $H_0$, $H_1$, and $H_2$ denote variants of a tgd head to illustrate propagation
  • Figure 2: Example graph $\text{\sf{LXG}}(\Sigma)$ (left) and chain of derived nulls in $\text{\sf{chase}}(\Sigma,\mathcal{D})$ (right) from Figure \ref{['fig_chain_intuition']}, with nulls partitioned according to Definition \ref{['def_fac_null_forest']} for the set $\hat{E} = \{ v_\ell\stackrel{y_0}{\to} v_0 \}$

Theorems & Definitions (61)

  • definition 1
  • definition 2
  • example 1
  • lemma 1
  • lemma 2
  • example 2
  • definition 3
  • example 3
  • lemma 3
  • definition 4
  • ...and 51 more