统一 - 结果的无限

Question

我正在开发(在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 =真).

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

提前致谢

Answer 1

在Prolog的背景下,当你说"统一"时,你通常意味着句法统一.因此,添加(X,Y)和succ(succ(0)),不统一(作为术语),因为它们的仿函数和arities不同.你似乎指的是统一模理论,其中可以统一诸如add(X,Y)和succ(succ(0))之类的不同术语,只要满足一些额外的方程或谓词.句法统一是可判定的,并且如果在应用最通用的统一者之后,在两个术语中仍然存在变量,则可能的统一者的数量是无限的.统一模理论一般不具有决定性.要看到已经基本的问题可以很难考虑,例如统一问题N> 2,X ^ N + Y ^ N = Z ^ N整数,如果你可以很容易地在算法上决定是否存在解(即,这些术语是否是统一的模整数运算),将立即解决费马的最后定理.还要考虑Matiyasevich的定理和类似的不可判定性结果.