arXiv 1401.48402014-01cs.DB

不经意追逐的终止是不可判定的

Termination of oblivious chase is undecidable

Tomasz Gogacz, Jerzy Marcinkowski

摘要：

我们证明了所有的情况下，追逐的终止是不可判定的。更确切地说，对于由元组生成规则（Tuple Generating principles）（也称为“$\cal T$”）组成的给定集合$\cal T$，数据库$^\exists$程序），是否对每个有限数据库实例$D$终止$D$上的$\cal T$ -chase。我们的方法适用于不经意的追逐，半不经意的追逐和-经过轻微的修改-也适用于标准追逐。这意味着我们给出了一个（负）解决方案的所有实例终止问题的所有版本的追逐，通常被认为是。我们的不可判定性证明所需的元数是3。我们还表明，这个问题是EXPSPACE难的二进制签名，但这种情况下的可判定性是开放的。三进制和二进制签名的证明都很容易。一旦你了解他们。

英文摘要：

We show that all--instances termination of chase is undecidable. More precisely, there is no algorithm deciding, for a given set $\cal T$ consisting of Tuple Generating Dependencies (a.k.a. Datalog$^\exists$ program), whether the $\cal T$-chase on $D$ will terminate for every finite database instance $D$. Our method applies to Oblivious Chase, Semi-Oblivious Chase and -- after a slight modification -- also for Standard Chase. This means that we give a (negative) solution to the all--instances termination problem for all version of chase that are usually considered. The arity we need for our undecidability proof is three. We also show that the problem is EXPSPACE-hard for binary signatures, but decidability for this case is left open. Both the proofs -- for ternary and binary signatures -- are easy. Once you know them.

机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。

阅读原文

阅读 PDF ↗

arXiv 页面 ↗HTML 原文 ↗

本文内容

摘要英文摘要相关论文

机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。

继续探索

相关论文

线性概率规则的半不经意追踪终止：实验研究

Semi-Oblivious Chase Termination for Linear Existential Rules: An Experimental Study

University of Milan（米兰大学）；University of Western Ontario（西安大略大学）；University of Edinburgh（爱丁堡大学）；University of Cyprus（塞浦路斯大学）

Chase过程是数据库中的一个基本算法工具，它允许我们在大量的应用程序中对约束进行推理，例如存在规则。它接受一个数据库和一组约束作为输入，并根据约束的规定迭代地完成数据库。然而，一个关键的挑战是它可能不会终止，这导致了在给定数据库和一组约束的情况下检查它是否终止的问题。在这项工作中，我们专注于半遗忘版本的追逐，这是非常适合于实际的实现，和线性存在规则，一个中央类的约束与几个应用程序。在这种情况下，有一个成熟的理论工作，提供了句法特征时，追逐终止，算法检查追逐终止，精确的复杂性结果，以及最坏情况下的最佳界限的大小追逐的结果（每当是有限的）。我们的主要目标是通过实验评估现有的追逐终止算法，目的是了解哪些输入参数会影响它们的性能，澄清它们是否可以在实践中使用，并揭示它们的性能限制。

2023-03-22cs.AIcs.DB

潜在规则的不经意和半不经意有界性

Oblivious and Semi-Oblivious Boundedness for Existential Rules

CNRS（法国国家科学研究中心）；Univ. Lille（里尔大学）；Inria（法国国家信息与自动化研究所）；Univ. Montpellier（蒙彼利埃大学）

我们研究的概念有界性的背景下，积极存在的规则，即是否存在一个上限的追逐程序的深度，这是独立于初始实例。通过将注意力集中在不经意和半不经意的追逐变体上，我们给出了有界性的一个表征，即FO-可重写性和追逐终止性。我们表明，它是可判定的，以认识到，如果一组规则是有界的几个类，并概述了问题的复杂性。本报告包含在IJCAI 2019上发表的论文和带有完整证明的附录。

2020-06-15cs.AIcs.CCcs.DB

显微镜下的数据交换追逐

The data-exchange chase under the microscope

在本文中，我们仔细看看最近的发展追逐程序，并提供额外的结果。我们的分析使我们能够创建一个分类的追逐变化和他们满足的属性。关于追逐的两个最核心的问题是终止，以及发现保证追逐终止的依赖集的受限类。搜索受限类的动机是最近的一个结果，该结果表明，确定具有给定依赖集的追逐是否会在给定实例上终止是不可判定的。这里有一个小的不协调，因为一直在寻求依赖集的类，保证在所有实例上的追逐的终止，即使后一个问题并不知道是不可判定的。我们在本文中解决的不和谐表明，确定是否与一组给定的依赖关系的追逐终止在所有的实例是核心完成。对于硬度的证明，我们使用的减少从字重写系统，从而也显示了密切的联系之间的追逐和字重写。同样的约简也给我们带来了前面提到的依赖实例的RE完备性结果作为副产品。对于保证终止所有实例的限制类之一，分层集依赖，我们提供了新的复杂性测试问题的结果是否一组给定的依赖属于it.These结果纠正了一些以前的索赔，已发生在文献中。

2014-07-08cs.DB

如果评估联接查询会终止吗？一个并不简单决定这个问题

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

Inria, DI ENS, ENS, CNRS, PSL University（法国国家信息与自动化研究所，巴黎高等师范学院，法国国家科学研究中心，巴黎文理研究大学）；LIRMM, Inria, University of Montpellier, CNRS（蒙彼利埃大学与法国国家科学研究中心联合实验室，法国国家信息与自动化研究所，蒙彼利埃大学，法国国家科学研究中心）

研究探讨了在支持可决定查询蕴含的规则类中，抽象规则类是否能变得具体，发现基于经典追逐变种终止性和有限树宽集的规则类并不满足这一条件。

2026-05-12cs.DB

追逐的解剖

Anatomy of the chase

由于Chase过程在数据集成、数据交换、查询优化、对等数据交换和数据通信等方面的有用性，最近围绕Chase过程进行了大量的研究活动。随着一些研究小组和作者对追逐进行了研究和进一步发展，出现了许多追逐的变体，并获得了相关的结果。由于该地区的异质性，往往难以核实每项成果的范围。在本文中，我们仔细研究了最近的发展，并提供了额外的结果。我们的分析使我们能够创建一个分类的追逐变化和他们满足的属性。关于追逐的两个最核心的问题是终止，以及发现保证追逐终止的依赖集的受限类。搜索受限类的动机是最近的一个结果，该结果表明，确定具有给定依赖集的追逐是否会在给定实例上终止是不可判定的。这里有一个小的不协调，因为一直在寻求依赖集的类，保证在所有实例上的追逐的终止，即使后一个问题并不知道是不可判定的。我们在本文中解决的不和谐表明，确定是否与一组给定的依赖关系的追逐终止在所有的实例是核心完成。我们的约简也给了我们前面提到的依赖实例的RE完备性结果作为副产品。对于其中一个限制类，分层集依赖，我们提供了新的复杂性测试问题的结果是否一组给定的依赖属于it.These结果纠正了一些以前的索赔，已经发生在文献中。

2013-03-26cs.DB

非一致终止追踪：规模和复杂性

Non-Uniformly Terminating Chase: Size and Complexity

University of Trento（特伦托大学）；University of Oxford（牛津大学）；University of Edinburgh（爱丁堡大学）；University of Cyprus（塞浦路斯大学）

追逐过程，最初介绍了检查数据库约束的含义，后来用于计算数据交换的解决方案，最近已成为一个中央算法工具，基于规则的本体论推理。在这种情况下，一个关键的问题是不一致的追逐终止：数据库的追逐w.r.t.一个基于规则的本体终止？如果是这样的话，追逐的结果是什么？我们专注于守护元组生成依赖关系（TGD），形成一个强大的基于规则的本体语言，并研究上述中心问题的半遗忘版本的追逐。我们的主要发现之一是，非均匀的半遗忘追逐终止的保护TGD是可行的多项式时间w.r. t。数据库和追逐结果的大小（无论何时是有限的）是线性的。数据库对我们的结果有关的非均匀追逐终止，我们表明，基本的技术，如简化和线性化，最初介绍了本体查询回答的背景下，可以安全地应用到追逐终止问题。

2022-04-26cs.AIcs.DB

更多相关论文收起更多论文

停止追逐

Stop the Chase

Chase过程是25年前提出的一种算法，用于修复数据库实例中的约束冲突，已成功应用于各种环境，如查询优化、数据交换和数据集成。然而，它的实用性受到这样一个事实的限制：对于任意的约束集，它可能不会终止;更糟糕的是，追逐终止通常是一个不可判定的问题。作为回应，数据库社区在保证任何数据库实例上的追踪终止的约束之上提出了足够的限制。在本文中，我们提出了一个新的充分终止条件，称为归纳限制，它严格推广了以前的条件，但可以有效地检查。此外，我们激励和研究的问题，数据依赖的追逐终止，并作为一个关键的结果，提出了充分的终止条件w.r.t.固定实例。它们严格地比归纳限制更一般，并且可能保证终止，尽管追逐在一般情况下不会终止。

2009-05-06cs.DB

势规则的k-有界性

On the k-Boundedness for Existential Rules

University of Montpellier（蒙彼利埃大学）；LIRMM（蒙彼利埃计算机信息、机器人与微电子实验室）；CNRS（法国国家科学研究中心）；Inria（法国国家信息与自动化研究所）

追逐是存在主义规则的基本工具。已知几种chase变体，它们在如何处理可能由引入空值引起的冗余方面有所不同。给定一个追逐变体，停机问题将一组存在规则作为输入，并询问这组规则是否确保对任何事实库的追逐的终止。众所周知，这个问题是不可判定的所有已知的追逐变种。有界性的相关问题是问一组给定的存在规则是否有界，即，是否有一个预定义的上限的数量（宽度优先）步骤的追逐，独立于任何factbase。这个问题在数据库规则的特定情况下已经是不可判定的。然而，如果边界是未知的，那么知道一组规则对于某些Chase变体是有界的在实践中没有多大帮助。因此，在本文中，我们研究的k-有界性问题，它要求是否一组给定的规则是有界的整数k的可判定性。我们证明了k-有界性是可判定的三个追逐变体，即遗忘，半遗忘和限制追逐。

2018-10-22cs.AIcs.DB

关于多头线性受限追查终止问题

About the Multi-Head Linear Restricted Chase Termination

TU Dresden（德累斯顿工业大学）；Inria, DI ENS, ENS, CNRS, PSL University（法国国家信息与自动化研究所, 巴黎高等师范学院计算机科学系, 巴黎高等师范学院, 法国国家科学研究中心, 巴黎文理研究大学）；University of Wrocław（弗罗茨瓦夫大学）

本文证明了在多头线性规则下，所有实例受限追查终止性是可判定的，解决了该问题的开放性挑战。

2025-09-23cs.DBcs.LO

全限制追踪终止

All-Instances Restricted Chase Termination

Chase过程是数据库理论中的一个基本算法工具，具有多种应用。关于追逐过程的一个关键问题是所有实例的终止：对于一组给定的元组生成依赖（TGD），追逐是否对每个输入数据库都终止？鉴于这个问题是不可判定的，很自然地要问，已知的行为良好的TGD类是否确保可判定性。我们在这里考虑的主要范式，导致强大的基于TGD的形式主义，即，guardedness和粘性。虽然所有实例终止对于不经意的追逐版本来说是很好理解的，但更微妙的限制（也称为标准）追逐是相当未探索的。我们发现，所有的情况下，限制追逐终止守卫和粘性单头TGD是可判定的。

2019-07-05cs.DBcs.LO

论超越分层的追逐终结

On Chase Termination Beyond Stratification

University of Freiburg（弗赖堡大学）

我们研究的终止问题的追逐算法，在各种数据库问题，如约束蕴涵问题，合取查询优化，重写查询使用视图，数据交换和数据集成的中心工具。追踪的基本思想是，给定一个数据库实例和一组约束作为输入，修复数据库实例中的约束冲突。众所周知，对于任意一组约束，追逐不一定会终止（一般来说，追逐是否终止甚至是不可判定的）。为了解决这个问题，我们审查现有的充分终止条件的追逐和开发新的技术，使我们能够建立较弱的充分条件的局限性。特别是，我们引入了两个新的终止条件称为安全和归纳限制，并使用它们来定义所谓的T-层次的终止条件。然后，我们研究我们的终止条件与以前的条件和检查我们的条件的复杂性的相互关系。这种分析导致一个算法，检查成员在一个级别的T-层次结构和帐户的复杂性的终止条件。作为另一个贡献，我们研究了数据依赖的追逐终止问题，并给出了充分的终止条件w.r.t.固定实例。它们可能保证终止，尽管追逐在一般情况下不会终止。作为我们的技术超出那些已经提到的应用程序，我们将我们的结果转移到查询回答领域的知识基础上的追逐底层数据库可能不会终止，使现有的算法适用于更广泛的类的约束。

2009-09-17cs.AIcs.DB

论概念依赖下追逐时对数据大小的依赖

On the dependency on the size of the data when chasing under conceptual dependencies

概念依赖（CD）是一种特殊类型的关键依赖（KD）和包含依赖（ID），它们精确地描述了根据语义关系（ER）模型的主要特征建模的关系模式。这种模式的实例可能是不一致的（数据违反依赖关系）和不完整的（数据构成一条正确的信息，但不一定是所有相关的信息）。虽然在一般的KD和ID下是不可判定的，但已知在不完整数据下的查询应答对于CD是可判定的。已知的技术是基于chase --一种特殊的实例，按深度层次组织，它代表了满足依赖关系并包括初始实例的所有实例。虽然追逐通常具有无限大小，但是可以通过在追逐的有限初始部分上提出查询（或其重写）来解决查询应答。与以前的说法相反，我们表明，这样的初始部分的最大水平不能由一个常数，不依赖于初始实例的大小的界限。

2013-12-09cs.DB

势规则的保守扩张

Conservative Extensions for Existential Rules

University of Hildesheim（希尔德斯海姆大学）；University of Bremen（不来梅大学）；University of Wrocław（弗罗茨瓦夫大学）

我们研究的问题来决定，给定T1，T2的元组生成依赖（TGD），也称为存在规则，T2是否是T1的保守扩展。我们考虑两个自然的概念保守的扩展，一个有关的答案，数据库的合取查询和一个追逐数据库之间的同态。我们的主要结果是，这些问题是不可判定的线性TGD，不可判定的守护TGD，即使当T1是空的，和可判定的前沿一TGD。

2022-02-11cs.AIcs.DBcs.LO

潜在规则的无环性概念及其在本体查询中的应用

Acyclicity Notions for Existential Rules and Their Application to Query Answering in Ontologies

University of Oxford（牛津大学）

在知识表示和数据库中，基于存在规则扩展的事实集的合取查询是一个突出的问题。这个问题可以使用chase算法来解决，该算法用新的事实扩展给定的事实集以满足规则。如果追踪终止，则CQ可以直接在结果事实集中进行评估。然而，追逐并不一定会终止，并且检查追逐是否在给定的一组规则和事实上终止是不可判定的。许多非循环概念被提出作为追逐终止的充分条件。在本文中，我们提出了两个新的无环性概念称为模型忠实无环性（MFA）和模型概括无环性（MSA）。此外，我们调查的景观已知的非周期性概念，并建立一个完整的分类所有的概念，我们知道。最后，我们表明，MFA和MSA概括了这些概念。潜在规则与OWL 2本体语言的Horn片段密切相关;此外，几个著名的OWL 2推理机通过使用追逐来实现所有相关事实的CQ回答。为了避免终止问题，这些系统中的许多只处理OWL 2的OWL 2 RL配置文件;此外，一些系统超越了OWL 2 RL，但没有任何终止保证。在本文中，我们还探讨了各种非周期性的概念是否可以提供一个原则和实际的解决方案，这些问题。在理论方面，我们表明，查询回答非循环本体是较低的复杂性比一般的本体。在实践方面，我们表明，许多常用的OWL 2本体是MSA，并且通过物化获得的事实的数量并不太大。因此，我们的研究结果表明，基于物化的OWL 2推理机的原则性发展实际上是可行的。

2014-02-04cs.AIcs.DB