is_list/1和自由变量

Question

这是第一个观察:

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

这是另一个观察:

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

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

?- is_list(_).
false.

要么

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

何时_可以清楚地统一列表？这不是逻辑上更健全的true吗？

在SWI-Prolog的文档中is_list/1,注释说: 

在5.0.1之前的版本中,is_list/1只检查[]或[_|_]与proper_list/1有电流的作用is_list/1.目前的定义符合事实上的标准.

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

Answer 1

正如您所正确观察的那样,它is_list/1是不健全的,或者说是不完整的,因为它错误地表示在提出最常见的查询时没有任何解决方案.

?- is_list(Ls).
false.

没有列表？来吧!

这个不幸的特点是所有的遗传类型检查的谓词如共享atom/1,integer/1 等等,其不正确很明显已经当这些谓词被设想尚未通过标记后,那些谁正确反对他们建议的语义为"纯粹主义者"(其中,在那个时候,缺乏推这个词自获得后的免费角色).

例如:

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

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

清楚地说明从这种非单调测试的逻辑观点来看,某些事情从根本上被打破了."Prolog (,)/2是不合逻辑的",是的,如果您在代码中首先使用不合逻辑的谓词.否则,(,)/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易于使用,是迈向更正确的逻辑程序的良好的第一步.其他结构也出现在地平线上,我希望其他人对当前状态发表评论.

现在对于实际的措辞:抛开上面概述的基本问题,SWI文档中提到的争论是,检查最外面的函子是否足以将术语视为列表,或者列表是否必须实际符合归纳定义一个列表,它是:

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

请注意,在最近的SWI版本中,[]甚至不是原子,所以它再次打破了这个概念.