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

Question

我无法理解这个关于 Prolog 的问题。问题如下:

Select all of the following goals that have an infinite number of solutions.

以下是可能的答案:

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 == [] (这是一个“免费定理”à la Wadler)但在这个约束下，X可以是任何无限的可能性:
SWI-Prolog 发现 Y == []并且对 X 的内容不置可否列表，仅将其作为未绑定(bind)变量的列表给出:

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

你是对的 append([a,b,c,d], Y, Z)应该被列为承认无限数量的解决方案。
有趣的是，在这种情况下，SWI-Prolog 没有枚举模板/占位符变量/候选列表，而是吐出本质上是对约束 append([a,b,c,d], Y, Z) 的重写。 ，即它比情况 1 表现得更能证明定理:

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

(这是 Prolog 的歧义:什么时候枚举，什么时候不枚举？如果有 是 一个 Prolog 符号，用于“未指定内容的 N 个值的列表，N 是 0 和 +oo 之间的整数”，这样的符号可能是用作 append(X,Y,X) 的输出。)
此处未选择的替代方法是:

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

是否有执行上述操作的 Prologs？可能有。