is_list/1 和自由变量

Question

这是第一个观察结果：

?- is_list([]), is_list([_,_,_]).
true.

这是另一个观察结果：

?- [] = _, [_,_,_] = _.
true.

因此，为什么 is_list/1 会这样实施

?- is_list(_).
false.

或

?- is_list([_|_]).
false.

什么时候_可以清楚的统一一个列表？ true 在逻辑上不是更合理吗？

在 SWI-Prolog's documentation for is_list/1 中，一条注释说：

In versions before 5.0.1, is_list/1 just checked for [] or [_|_] and proper_list/1 had the role of the current is_list/1. The current definition conforms to the de facto standard.

为什么这是事实上的标准？

Answer 1

如您所见，is_list/1 不合理，或者 不完整，因为它 不正确 说当提出最一般的查询时 没有任何解决方案。

?- is_list(Ls).
false.

不存在列表？拜托！

所有遗传类型检查谓词（如 atom/1、integer/1 等）都具有这种不幸的特征，这些谓词的不正确性在构思这些谓词时就已经很明显了，但在标记了那些正确反对的人之后才得以通过他们建议的语义为 "purists"（在那个时候，缺少该词后来获得的补充字符）。

案例如下：

?- is_list(Ls), Ls = [].
false.

?- Ls = [], is_list(Ls).
Ls = [].

通过此类 non-monotonic 测试，从逻辑的角度清楚地说明某些东西从根本上被破坏了。 "Prolog's (,)/2 is not logical conjunction"，是的，如果您在代码中首先使用不合逻辑的谓词。否则，(,)/2 始终是目标的逻辑合取。

一个干净且逻辑上正确的方法是在无法确定的情况下抛出 实例化错误。

library(error)，尤其是 must_be/2 在继承的不合逻辑谓词的不正确性变得难以忍受后，甚至对于 Prolog 的临时用户来说，进入了一个合理的方向：

?- must_be(list, X).
Arguments are not sufficiently instantiated

?- must_be(list, [_|_]).
Arguments are not sufficiently instantiated

?- must_be(list, [a,b,c]).
true.

must_be/2 易于使用，是朝着更正确的逻辑程序迈出的良好第一步。 horizon上也出现了其他构造，希望其他人对当前状态发表评论。

现在是实际的措辞：撇开上面概述的基本问题不谈，SWI 文档中提到的争论是检查最外层的函子 是否足以 将一个术语视为列表，或者列表是否必须真正符合列表的归纳定义，即：

原子 [] 是一个列表。
如果 Ls 是一个列表，那么 '.'(_, Ls) 也是一个列表。

请注意，在最近的 SWI 版本中，[] 甚至不是一个原子，因此它再次打破了这个概念。

is_list/1 和自由变量

is_list/1 and free variables

list

prolog

unification

logical-purity