在这些情况下为什么append / 3会产生无数个解的解释

问题描述

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

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

这是可能的答案：

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

显然，正确答案是2和3，但是我不明白为什么1也不正确-Z以及Y都没有无限可能吗？另外，由于第一个参数和第三个参数（“结果”）相同，为什么2是正确的？听起来Y可能就是[]。

非常感谢！

解决方法

SELECT default_version,installed_version FROM pg_available_extensions WHERE name = 'timescaledb'; default_version | installed_version -----------------+------------------- 1.6.1 | 1.4.2 仅适用于append(X,Y,X)（这是“免费的定理”àWadler），但在此约束下，Y == []可以是无限的可能性之一：

SWI-Prolog发现X，并且对Y == []列表的内容一无所知，仅将其作为未绑定变量的列表来提供：

X

您是正确的，?- append(X,X). X = Y,Y = [] ; % alternative writing of X = [],Y = [] X = [_6696],Y = [] ; X = [_6696,_7824],_7824,_8952],_8952,_10080],_10080,_11208],Y = [] ... 应该被列为允许无限数量的解决方案。

有趣的是，在这种情况下，SWI-Prolog不会枚举模板/占位符变量列表/候选对象，但会吐出本质上是对约束append([a,b,c,d],Z)的重写，即与第一种情况相比，它表现出更多的定理证明：

append([a,Z)

（这是Prolog的歧义：何时枚举，什么时候不枚举？如果在”列表中有 个Prolog表示法，其中N个值未指定，N为0到+之间的整数oo“ 这样的表示法可以用作?- append([a,Z). Z = [a,d|Y]. 的输出。）

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

append(X,X)

有没有做上述事情的序言？可能有。

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

,

如果您想精确地谈论Prolog，有必要区分（至少）查询的答案和解决方案。 answer 是一种过程概念，它是每次查询成功时Prolog生成的变量的替代。 解决方案是变量的替换，查询成功进行。每个答案替换都是一个解决方案，但这并不能使这些概念成为同义词。

考虑该谓词：

foo(a).
foo(a).

这有两个答案（碰巧看起来一样）：

?- foo(X).
X = a ;
X = a.

它有一个解决方案：只有替换X = a才能成功，Prolog甚至可以证明这一点：

?- X = a,foo(X).
X = a ;
X = a.

?- dif(X,a),foo(X).
false.

在这种情况下，答案多于解决方案。相反也可能：

bar(f(_X)).

这里的查询bar(T)有一个答案，但是有多个解决方案（实际上是无限多个）：

?- bar(T).
T = f(_708).

?- T = f(1),bar(T).
T = f(1).

?- T = f(2),bar(T).
T = f(2).

现在让我们看一下问题中的第一个查询：

?- append([a,d|Y].

使用上面的定义，它只有一个 answer 。但是正如您所指出的，我们可以用无数个不同的值代替变量，从而得到无数个 solutions ，例如：

?- Y = [1],append([a,Z).
Y = [1],1].

?- Y = [1,2],Z).
Y = [1,1,2].

现在，坏消息是您的老师似乎没有使用与我在此处使用的约定相同的约定。使用上面定义的术语，老师在询问答案时，而您在思考解决方案时。知道他们是否理解这种区别，以及对于这些截然不同的概念使用了哪些术语，将会很有趣。如果它们真的是 answers 的意思，那么他们对这个查询没有无限多个是正确的。如果它们真的意味着解决方案，那么您是正确的，那就是确实有很多解决方案。

第二个查询：

?- append(X,Y = [] ;
X = [_818],Y = [] ;
X = [_818,_824],_824,_830],Y = [] .

您是正确的，Y只能是[]，但这仍然为X留下了无限数量的解决方案。在这里，Prolog还产生了无限多个描述这些解决方案的答案。