解释为什么 append/3 在这些情况下会产生无限数量的解决方案

Question

我无法理解有关 Prolog 的这个问题。问题如下：

选择以下所有具有无限数量解决方案的目标。

以下是可能的答案：

append([a,b,c,d], Y, Z)
append(X, Y, X)
append(X, [a,b,c,d], Z)
append(X, Y, [a,b,c,d])

显然，正确答案是2和3，但我不知道为什么1不是也是正确的-不会有对无限的可能性Z，因此也Y？另外，为什么 2 是正确的，因为第一个参数和第三个参数（“结果”）是相同的？听起来Y可能只是[]。

非常感谢！

Answer 1

append(X, Y, X)只能是正确的Y == []（这是一个“免费定理”\xc3\xa0 la Wadler），但在该约束下，X可以是无限种可能性中的任何一种：

\n

SWI-Prolog 发现了Y == []列表的内容，但对此不置可否X，仅将其作为未绑定变量的列表给出：

\n

?- append(X,Y,X).\nX = Y, Y = [] ;   % alternative writing of X = [], Y = []\nX = [_6696],\nY = [] ;\nX = [_6696, _7824],\nY = [] ;\nX = [_6696, _7824, _8952],\nY = [] ;\nX = [_6696, _7824, _8952, _10080],\nY = [] ;\nX = [_6696, _7824, _8952, _10080, _11208],\nY = [] \n...\n

\n

你是对的，append([a,b,c,d], Y, Z)应该被列为承认无限数量的解决方案。

\n

有趣的是，在这种情况下，SWI-Prolog 不会枚举模板/占位符变量/候选者列表，而是吐出本质上重写的约束append([a,b,c,d], Y, Z)，即它的行为比情况 1 更具有定理证明性：

\n

?- append([a,b,c,d],Y,Z).\nZ = [a, b, c, d|Y].\n

\n

（这是 Prolog 的歧义：它什么时候枚举，什么时候不枚举？如果有一个Prolog 表示法“未指定内容的 N 个值的列表，N 是 0 和 +oo 之间的整数”，则可以使用这种表示法作为输出append(X,Y,X)。 ）

\n

此处未选择的替代方案是：

\n

?- append([a,b,c,d],Y,Z).\nY = [], \nZ = [a,b,c,d] ;\nY = [_1], \nZ = [a,b,c,d,_1] ;\nY = [_1,_2], \nZ = [a,b,c,d,_1,_2] ;\n...\n

\n

是否有任何 Prolog 可以执行上述操作？可能有。

\n

\n