💻 computer science

Non-Termination of Logic Programs Using Patterns

本文通过引入一种能够生成代表无限有限重写序列模式的新型展开技术，将一种用于检测非循环非终止的项重写方法应用于逻辑编程，并使用 NTI 工具对其进行了实验评估。

原作者： Etienne Payet

发布于 2026-08-10

📖 1 分钟阅读☕ 轻松阅读

原作者： Etienne Payet

原始论文采用 CC BY 4.0 许可（http://creativecommons.org/licenses/by/4.0/）。 ✨ 这是对下方论文的AI生成解释。它不是由作者撰写或认可的。如需技术准确性，请参阅原始论文。阅读完整免责声明

想象一下，你正在观察一个机器人尝试解决谜题。有时，机器人会陷入一个循环：它执行步骤 A，然后执行步骤 B，接着又执行步骤 A，如此循环往复，永无止境。这就像仓鼠在转轮上奔跑；它在移动，但哪儿也没去。在计算机科学的一个被称为**逻辑编程（Logic Programming）**的领域中，这些机器人就是试图通过遵循一套规则来回答问题的程序。如果一个程序陷入循环，它就永远无法完成任务，这通常是程序员想要捕捉到的漏洞（bug）。

但有一种更棘手的类型。有时，程序并不会陷入一个整齐的、重复的圆圈。相反，它走了一步，然后是略有不同的一步，接着是看起来几乎一样但不完全一样的另一部，并以此持续进行下去，永不停歇，且从未重复过完全相同的模式。这就像一位舞者，她从未重复过同一个动作，但也从未停止跳舞。这被称为非循环非终止（non-looping non-termination）。由于没有明显的“循环”可以指认，这种现象极难被发现。检测这些无限的、非重复的序列是计算机科学家面临的一大挑战，他们希望能够证明一个程序最终会停止，或者找到导致其永不停歇的具体起始点。

这篇论文介绍了一种巧妙的新方法，用来捕捉这些难以捉摸的、非重复性的无限循环。作者埃蒂安·帕耶（Etienne Payet）构建了一个名为 NTI 的工具，它就像是一个针对逻辑程序的超级侦探。该工具并没有尝试观察程序如何一步步运行（因为那会耗时永远），而是使用了一种叫做**展开（unfolding）**的技术。把“展开”想象成将一只复杂的折纸鹤压平，以观察底层的折痕模式。通过展开程序的规则，该工具创建了“模式（patterns）”——即抽象的蓝图，它们描述的不只是某一条特定的路径，而是一系列可能的路径构成的无限家族。

该论文的主要发现是，通过使用这些蓝图，特别是被称为“简单模式（simple patterns）”的简化版本，该工具可以从数学上证明一个程序将会永远运行下去，且不会陷入简单的循环。作者在 41 个已知具有挑战性的逻辑程序上对该工具进行了测试。该工具成功识别了其中许多程序中的无限、非重复路径，其中包括四个此前没有任何现有工具能够证明其为非终止状态的程序。然而，论文也诚实地说明了它的局限性：该工具并没有解决所有的案例，对于某些程序，它在运行 10 秒后便卡住或超时了。作者指出，虽然他们的方法是侦探工具箱中一个强大的新成员，但它还不是能解决所有谜团的魔杖。他们计划在未来使该工具变得更加聪明，希望能捕捉到更多这类棘手的、非重复性的无限循环。

技术摘要：使用模式检测逻辑程序的非终止性

问题陈述
本文研究了逻辑程序（LPs）中非终止性的自动检测。虽然现有的大量研究侧重于检测“循环”（即可以无限重复的有限重写序列），但本研究的目标是“非循环非终止性”。这类序列是既不包含任何循环的无限重写序列，具有本质上的非周期性且难以检测。作者指出，此类序列可能由简单的逻辑程序产生，然而标准的循环检测方法往往无法识别它们。其动机包含两个方面：理论层面（研究显著形式的无限序列）以及实践层面（帮助程序员识别运行永不停止的查询）。

方法论
作者将 Emmes 等人（2012）最初为项重写系统引入的方法适配到了逻辑编程领域。核心方法涉及定义一种新的展开技术，用于生成描述潜在无限有限重写集合的“模式”（patterns）。

模式定义：
- 模式替换（Pattern Substitutions）： 定义为对 $\theta = (\sigma, \mu)$ ，记作 $\sigma \star \mu$ ，描述了一组替换集合 $\{\theta(n) = \sigma^n\mu \mid n \in \mathbb{N}\}$ 。
- 模式项（Pattern Terms）： 对 $(s, \theta)$ ，描述了集合 $\{s\theta(n) \mid n \in \mathbb{N}\}$ 。
- 模式规则（Pattern Rules）： 模式项对 $(p, q)$ ，描述了二元规则集合 $\{(p(n), q(n)) \mid n \in \mathbb{N}\}$ 。
正确性与展开：
- 若一个模式规则相对于程序 $P$ 是正确的，则意味着它所描述的规则集是 $P$ 的二元展开（$binunf(P)$）的一个子集。
- 作者引入了一种新的展开算子 $T^\pi_{P,B}$ ，用于从程序 $P$ 和一组正确的基准模式规则 $B$ 中计算模式规则。该算子通过使用模式项的合一算法来组合规则，从而比传统的二元展开更快速地“展开”程序，通过有限表示捕捉 $binunf(P)$ 的无限子集。
简单模式与合一：
- 为了使该方法具有自动化能力，作者将定义域限制在简单模式项（simple pattern terms）内，其中替换遵循涉及一元上下文（unary contexts）的特定结构。
- 文中提供了一种针对此类简单项的合一算法。该算法将简单模式项映射到基于专门签名 $\Upsilon$ 的项（使用一元符号 $c_{a,b}$ 表示重复嵌入），并应用经典的合一算法（如 Robinson 或 Martelli-Montanari）。
- 该算法被证明是部分正确的：如果它成功终止，则会产生输入模式序列的最一般合一子（mgu）。
非终止判定标准：
- 通用标准（定理 3）： 借鉴自 Emmes 等人，该定理指出，如果模式展开包含形式为 $(u \star \sigma \star \mu, u\sigma^a \star \sigma^b\sigma' \star \mu\mu')$ 的规则，其中 $\sigma'$ 与 $\sigma$ 及 $\mu$ 可交换，则存在无限链。
- 特殊标准（定理 5）： 对于特殊模式规则（简单规则的一个子集）而言，这是一个更容易检查的条件。如果展开中存在此类规则，本文证明了从该规则左手边（LHS）的特定实例出发，存在一条无限链。

主要贡献
本文提出了四个主要贡献：

新的展开技术： 一种生成正确模式规则的逻辑编程方法，提供了比项重写中使用的九个推理规则更紧凑的表示，并消除了对复杂应用策略的需求。
简单模式项与合一： 定义了一种受限形式的模式项（“简单模式”）以及一个被证明是正确的对应合一算法。
可自动化的充分条件： 一个易于检查的条件（定理 5），用于检测来自简单模式规则的非循环非终止性。
实现（NTI）： 将该方法实现在名为 NTI 的工具中。

实验结果
作者在源自终止问题数据库（TPDB）中非循环非终止项重写系统（TRSs）的 41 个逻辑程序上评估了 NTI。

成功： 该工具成功证明了 36 个程序的非终止性。值得注意的是，它成功处理了 4 个程序（在表中以 † 标记），这些程序在截至 2024 年的国际终止竞赛中，尚未被任何其他 TRS 分析器证明为非终止。
失败： 该方法在 5 个程序上失败，主要原因是使用项代表的“自然选择”（如示例 12 所讨论）时的合一算法不完备，或者是由于对简单模式的限制（示例 9）。
性能： 执行时间普遍较低（成功案例通常在 300ms 以下），尽管某些复杂情况会导致超时。

意义与声明
作者声称，其方法是唯一能够证伪逻辑程序终止性的参与国际终止竞赛的工具。作者指出，虽然 Payet (2024) 存在另一种用于证明非循环非终止性的方法，但该方法处理的是不同类型的非循环性，且无法证伪本文测试的特定程序（表 1 和表 2）。相反，Payet (2024) 的方法可以证伪本文方法失效的程序。因此，这两种方法被视为互补关系。

论文以谦逊的态度结束，承认目前的合一算法尚不完备，且对简单模式的限制限制了其适用范围（例如，在需要带有变量的一元上下文时会失败）。未来的工作计划解决完备性问题，扩展初始模式生成（命题 2），并将该方法适配到 TRS 以便与 Emmes 等人 (2012) 进行直接比较。

类似论文