java - 统一 - 结果无限

Question

我正在开发（在 Java 中），为了好玩，一个使用统一算法的应用程序。

我选择我的统一算法返回所有可能的统一。例如，如果我尝试解决

添加（X，Y）=成功（成功（0））

它返回

{X = succ(succ(0)), Y = 0}, {X = succ(0), Y = succ(0)}, {X = 0, Y = succ(succ(0))}

然而，在某些情况下，可能存在无限多的统一（例如 X > Y = true）。

有人知道算法允许确定是否可能遇到无限数量的统一吗？

提前致谢

Answer 1

在 Prolog 的上下文中，当您说“统一”时，通常是指句法统一。因此，add(X, Y) 和 succ(succ(0)) 并不统一（作为术语），因为它们的函子和数量不同。您似乎指的是统一模理论，其中 add(X, Y) 和 succ(succ(0)) 等不同的术语可以统一，只要满足一些额外的方程或谓词。句法统一是可确定的，如果在应用最一般的统一词之后，两个术语中仍然存在变量，则可能的统一词的数量是无限的。统一模理论通常是不可判定的。要看到已经基本的问题可能很难考虑例如统一问题 N > 2, X^N + Y^N = Z^N 在整数上，如果您可以轻松地通过算法确定是否存在解决方案（即, 项是否是统一的模整数算术), 将立即解决费马大定理。还要考虑 Matiyasevich 定理和类似的不可判定性结果。

Answer 2

在某些约束逻辑编程系统中，您可以轻松查看解决方案集是否无限。例如，在某些 CLP(FD) 实现中（即 SWI-Prolog、Jekejeke Minlog，其他实现如 GNU Prolog 和 B-Prolog 则不是，因为它们假设一个有限的上限/下限），无限整数集的某种程度的推理是因此得到支持。这可以从区间符号中看到，例如 (SWI-Prolog)：

?- use_module(library(clpfd)).
true.

?- X #\= 2.
X in inf..1\/3..sup.

但是这些集合有一个缺点，它们不能用于 CLP(FD) 标记，其中枚举集合的元素并进一步尝试求解实例化方程。如果通常可以做一些事情来决定 CLP(FD) 查询，它也会与以下结果背道而驰：

“1900 年，鉴于其深度，大卫希尔伯特提出了所有丢番图问题的可解性作为他著名问题的第十个。1970 年，数学逻辑中的一个新结果，称为 Matiyasevich 定理，消极地解决了这个问题：一般来说，丢番图问题是无解。” （来自关于丢番图方程的维基百科）

另一个通常也可以处理无限解集的约束逻辑编程是 CLP(R)。方程之间的推理在那里要强一些。例如 CLP(FD) 没有检测到以下不一致（取决于系统，这是 SWI-Prolog 的结果，在 Jekejeke Minlog 中，您将立即看到第二个查询的 No，并且 GNU Prolog 将循环大约 4 秒然后说不）：

?- X #> Y.
Y#=<X+ -1.

?- X #> Y, Y #> X.
X#=<Y+ -1,
Y#=<X+ -1.

另一方面，CLP(R) 会发现：

?- use_module(library(clpr)).

?- {X > Y}.
{Y=X-_G5542, _G5542 > 0.0}.

?- {X > Y, Y > X}.
false.

约束系统通过实现数论、线性代数、分析等算法来工作。取决于它们建模的领域，即符号 CLP(*) 中 * 表示的内容。这些算法可以达到量词消除。

再见