在 Prolog 中,统一X = [1|X]
是获得无限列表的明智方法吗?SWI-Prolog 没有任何问题,但 GNU Prolog 只是挂起。
我知道在大多数情况下,我可以将列表替换为
one(1).
one(X) :- one(X).
但我的问题是明确地是否可以X = [1|X], member(Y, X), Y = 1
在“理智的”Prolog 实现中使用该表达式。
在 Prolog 中,统一X = [1|X]
是获得无限列表的明智方法吗?SWI-Prolog 没有任何问题,但 GNU Prolog 只是挂起。
我知道在大多数情况下,我可以将列表替换为
one(1).
one(X) :- one(X).
但我的问题是明确地是否可以X = [1|X], member(Y, X), Y = 1
在“理智的”Prolog 实现中使用该表达式。
在 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.
所以有时有一些简单的方法可以避免不终止。但往往没有。
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.
如果您想使用无限列表,您也可以选择恢复为惰性列表。他们也有一个共同的阅读。这是一个简单的 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 民间传说。