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 = 真)。

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

提前致谢

Answer 1

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