统一 - 无限的结果
为了好玩，我正在开发（用Java）一个使用统一算法的应用程序。
我选择我的统一算法返回所有可能的统一。例如，如果我尝试求解
add(X,Y) = succ(succ(0))
它会返回
{X = succ(succ(0)), Y = 0}, {X = succ(0), Y = succ(0)}, {X = 0, Y = succ(succ(0))}
但是，在某些情况下，存在无限多个可能的统一 (例如X>Y＝真)。
有人知道算法可以确定是否可能遇到无限数量的统一吗？
提前致谢
I'm developing (in Java), for fun, an application which uses an unification algorithm.
I have chosen that my unification algorithm returns all the possible unifications. For example, if I try to solve
add(X,Y) = succ(succ(0))
it returns
{X = succ(succ(0)), Y = 0}, {X = succ(0), Y = succ(0)}, {X = 0, Y = succ(succ(0))}
However, in some cases, there exists an infinite number of possible unifications
(e.g. X > Y = true).
Does someone know am algorithm allowing to determine if an infinite number of unifications may be encountered?
Thanks in advance
如果你对这篇内容有疑问，欢迎到本站社区发帖提问 参与讨论，获取更多帮助，或者扫码二维码加入 Web 技术交流群。
绑定邮箱获取回复消息
由于您还没有绑定你的真实邮箱，如果其他用户或者作者回复了您的评论，将不能在第一时间通知您！
发布评论
评论（2）
在 Prolog 的上下文中，当你说“统一”时，你通常指的是语法统一。因此，add(X, Y) 和 succ(succ(0)) 不统一（作为术语），因为它们的函子和元数不同。您似乎指的是统一模理论，其中如果满足一些附加方程或谓词，则可以统一诸如 add(X, Y) 和 succ(succ(0)) 等不同术语。句法统一是可判定的，并且如果在应用最通用的统一词之后，两个术语中仍然有变量，则可能的统一词的数量是无限的。统一模理论通常是不可判定的。看到已经很基本的问题可能很难考虑，例如统一问题 N > 。 2、整数上的 X^N + Y^N = Z^N，如果您可以轻松地通过算法确定是否存在解决方案（即，这些项是否是统一的模整数算术），将立即解决费马大定理。还要考虑马蒂亚塞维奇定理和类似的不可判定性结果。
In the context of Prolog, when you say "unification", you usually mean syntactic unification. Therefore, add(X, Y) and succ(succ(0)), do not unify (as terms), because their functors and arities differ. You seem to be referring to unification modulo theories, where distinct terms like add(X, Y) and succ(succ(0)) can be unified provided some additional equations or predicates are satisfied. Syntactic unification is decidable, and the number of possible unifiers is infinite if, after applying the most general unifier, you still have variables in both terms. Unification modulo theories is in general not decidable. To see that already basic questions can be hard consider for example the unification problem N > 2, X^N + Y^N = Z^N over the integers, which, if you could easily algorithmically decide whether or not a solution exists (i.e., whether the terms are unifiable modulo integer arithmetic), would immediately settle Fermat's Last Theorem. Consider also Matiyasevich's theorem and similar undecidability results.
在某些约束逻辑编程系统中，您可以轻松查看解集是否是无限的。例如，在一些 CLP(FD) 实现中（即 SWI-Prolog、Jekejeke Minlog，其他实现如 GNU Prolog 和 B-Prolog 则不然，因为它们假设有限的上/下界）无限整数集的一定程度的推理是从而得到支持。这可以通过间隔符号（例如（SWI-Prolog））看出：
但这些集合有一个缺点，它们不能用于枚举集合元素的 CLP（FD）标记以及进一步尝试求解实例化方程被制成。如果一般可以采取一些措施来决定 CLP(FD) 查询，它也会与以下结果背道而驰：
另一种通常也可以处理无限解集的约束逻辑编程是CLP(R)。那里方程之间的推理更强一些。例如，CLP(FD) 不会检测到以下不一致（取决于系统，这是 SWI-Prolog 的结果，在 Jekejeke Minlog 中，您将立即看到第二个查询的“否”，并且 GNU Prolog 将循环大约 4 秒然后说“否”）：
另一方面，CLP(R) 会发现：
约束系统通过实现数论、线性代数、分析等算法来工作。取决于它们建模的领域，即 CLP 符号中 * 表示什么(*)。这些算法可以达到量词消除。
再见
In certain constraint logic programming systems you can easily see if the solution set is infinite or not. For example in some CLP(FD) implementations (i.e. SWI-Prolog, Jekejeke Minlog, other implementations such as GNU Prolog and B-Prolog not, since they assume a finite upper/lower bound) a certain degree of reasoning with infinite integer sets is thus supported. This is seen by interval notations such as (SWI-Prolog):
But there is a disadvantage of those sets, they cannot be used in CLP(FD) labeling where the elements of the set are enumerated and a further attempt to solve the instantiated equations is made. It would also run counter to the following result, if something could be done in general to decide CLP(FD) queries:
Another constraint logic programming that can usually also deal with infinite solution sets is CLP(R). The reasoning among equations is a little stronger there. For example CLP(FD) does not detect the following inconsistency (depends on the system, this is the result for SWI-Prolog, in Jekejeke Minlog you will immediately see a No for the second query, and GNU Prolog will loop for around 4 secs and then say No):
On the other hand CLP(R) will find:
Constraint systems work by implementing algorithms from number theory, linear algebra, analysis, etc.. depending on the domain they model, i.e. what * denotes in the notation CLP( * ). These algorithms can go as far as quantifier elimination.
Bye