list - 无限的列表是否合理？

Question

在 Prolog 中，统一X = [1|X]是获得无限列表的明智方法吗？SWI-Prolog 没有任何问题，但 GNU Prolog 只是挂起。

我知道在大多数情况下，我可以将列表替换为

one(1).
one(X) :- one(X).

但我的问题是明确地是否可以X = [1|X], member(Y, X), Y = 1在“理智的”Prolog 实现中使用该表达式。

Answer 1

在 Prolog 中，统一X = [1|X]是获得无限列表的明智方法吗？

这取决于您是否认为生成一个无限列表是明智的。在 ISO-Prolog 中，类似的统一X = [1|X]会受到发生检查 (STO) 的影响，因此是未定义的。也就是说，一个符合标准的程序不能执行这样的目标。为了避免这种情况发生，有unify_with_occurs_check/2, subsumes_term/2。为了防止接口接收无限项，有acyclic_term/1.

所有当前的实现都终止于X = [1|X]. GNU Prolog 也终止：

| ?- X = [1|X], acyclic_term(X).

no

但是对于更复杂的情况，需要合理的树统一。repeat 1 == repeat 1将此与导致ghci冻结的 Haskell 进行比较 。

至于在常规 Prolog 程序中使用有理树，这在开始时非常有趣，但扩展性不是很好。例如，在 1980 年代初期的一段时间里，人们相信语法将使用有理树来实现。唉，人们对单独的 DCG 感到满意。这没有离开研究的一个原因是，因为 Prolog 程序员认为存在的许多概念，对于有理树来说并不存在。以词典术语排序为例，它对有理树没有扩展。也就是说，存在无法使用标准术语顺序进行比较的有理树。（实际上，这意味着您会得到准随机结果。）这意味着您无法生成包含此类术语的排序列表。这再次意味着许多内置插件像bagof/3不再以无限项可靠地工作。

对于您的示例查询，请考虑以下定义：

memberd(X, [X|_Xs]).
memberd(E, [X|Xs]) :-
   dif(E,X),
   memberd(E, Xs).

?- X = 1, Xs=[1|Xs], memberd(X,Xs).
X = 1,
Xs = [1|Xs] ;
false.

所以有时有一些简单的方法可以避免不终止。但往往没有。

Answer 2

You don't get an infinite number of ones, of course, but what's called a rational or cyclic term. Not all Prolog systems support cyclic terms, however. Systems that provide some support for rational terms include CxProlog, ECLiPSe, SICStus, SWI-Prolog, and YAP. But be aware that there are differences between them regarding the computations that you can perform with rational terms.

A query such as:

X = [1|X], member(Y, X), Y = 1.

requires support for coinduction. You have a portable implementation of coinduction in Logtalk, which you can use with all the systems mentioned above. Coinduction requires that the Prolog system can create rational terms (using a query such as X = [1|X]), that can unify rational terms, and that can print bindings with rational terms in a non-ambigouos way.

For an example about enumerating (or testing) the elements of a rational list, see:

https://github.com/LogtalkDotOrg/logtalk3/blob/master/examples/coinduction/lists.lgt

Two sample queries for this example:

?- {coinduction(loader)}.
...
% (0 warnings)
true.
?- X = [1|X], lists::comember(Y, X), Y = 1.
X = [1|X],
Y = 1 ;
false.

?- X = [1, 2, 3| X], lists::comember(Y, X).
X = [1, 2, 3|X],
Y = 1 ;
X = [1, 2, 3|X],
Y = 2 ;
X = [1, 2, 3|X],
Y = 3 ;
false.

If you're interested in rational terms and coinduction, Logtalk's coinduction example includes several individual examples and bibliographic references.

Answer 3

如果您想使用无限列表，您也可以选择恢复为惰性列表。他们也有一个共同的阅读。这是一个简单的 Haskell 类 Prolog 中的 take 谓词，它将评估惰性列表 [Head|TailClosure] 的初始段：

take(0, _, R) :- !, R = [].
take(N, C, [H|R]) :-
  call(C, [H|T]),
  M is N-1,
  take(M, T, R).

这是此框架中列表的定义：

 one([1|one]).

如您所见，您可以扩展共归纳定义：

 Welcome to SWI-Prolog (threaded, 64 bits, version 7.7.1)
 SWI-Prolog comes with ABSOLUTELY NO WARRANTY. This is free software.

 ?- take(5,one,L).
 L = [1, 1, 1, 1, 1]. 

使这项工作的要求远低于理性条款的情况。您只需要一个支持ISO 核心标准要求的call/n的 Prolog 系统，在其勘误 2 中。另一方面，不需要有理项。

可以通过这种方式定义非理性列表，也可以对组合不同流的流处理器进行编码。关于某些应用的文献越来越多，例如 Coq、HOL/Isabelle 等精确实数和定理证明器可以推理此类流。

进一步阅读：

Markus Triska - Prolog Streams
https://www.metalevel.at/various/prost

Dexter Kozen 和 Alexandra Silva - 实用共感应
https://www.cs.cornell.edu/~kozen/Papers/Structural.pdf

编辑 14.08.2018：
必须说 Markus Triska 的 prost 和我在这里的帖子都没有通过高阶调用发明惰性列表。我们在这里找到了 1983 年 Richard O'Keefe 的片段lazy.pl，其中使用了 apply/2，它是 call/n 的前身。所以我猜它几乎属于 Prolog 民间传说。