prolog - 卡住/2个目标阻止已变得无法访问的变量

Question

我制作了以下小程序来确定内存是否用于 freeze(X,Goal) 之类的目标回收时 X变得无法访问:

%:- use_module(library(freeze)). % Ciao Prolog needs this

freeze_many([],[]).
freeze_many([_|Xs],[V|Vs]) :-
   freeze(V,throw(error(uninstantiation_error(V),big_freeze_test/3))),
   freeze_many(Xs,Vs).

big_freeze_test(N0,N,Zs0) :-
   (  N0 > N
   -> true
   ;  freeze_many(Zs0,Zs1),
      N1 is N0+1,
      big_freeze_test(N1,N,Zs1)
   ).

让我们运行以下查询...

?- statistics, length(Zs,1000), big_freeze_test(1,500,Zs), statistics.

...使用不同的 Prolog 处理器并查看内存消耗。
有什么不同!

(AMD64) SICStus Prolog 4.3.2:使用中的全局堆栈 = 108 MB
(AMD64) B-Prolog 8.1:使用中的堆栈 + 堆 = 145 MB
(i386) Ciao Prolog 1.14.2:使用中的全局堆栈 = 36 MB(~72 MB w/AMD64)
(AMD64) SWI-Prolog 7.3.1:使用中的全局堆栈 = 0.5 MB
(AMD64) YAProlog 6.2.2:使用中的全局堆栈 = 16 MB

使用 ?- length(Zs,1000), big_freeze_test(1,10000,Zs). 运行更多迭代时，我做了以下观察:

Ciao Prolog 报告 {ERROR: Memory allocation failed [in Realloc()]}流产前。

sicstus-prolog和 b-prolog分配越来越多，直到机器卡住。

swi-prolog在 3.554 秒内执行所有迭代。

yap也执行所有迭代，但需要 36.910 秒。

任何想法 为什么它适用于 SWI-Prolog 和 YAProlog，但 不和其他的？

考虑到运行时间，为什么 SWI-Prolog 比 YAProlog 高出一个数量级？

我的直觉倾向于“属性变量”与“垃圾收集”的交互。 SWI-Prolog 和 YAProlog 具有(共享？)与其他 Prolog 处理器不同的属性变量 API 和实现......而且，再一次，它可能是完全不同的东西。
谢谢!

Answer 1

TL;博士:bug in SWI不再!

您正在创建 500,000 个随后无法实现的卡住目标。这些目标意味着什么？ Prolog 系统不会分析目标的语义相关性(在实际执行之前)。所以我们必须假设目标可能在语义上是相关的。由于目标已经断开连接，它们可能具有的唯一语义影响是错误的，从而使下一个答案成为错误。

所以考虑freeze(_,false)就足够了反而。

在语义上，谓词 p/0和 q/0是等价的:

p :-
   false.

q :-
   freeze(_,false).

然而，在程序上，第一个目标失败而第二个目标成功。在这种情况下区分 是关键。解决方案 和 答案 .当 Prolog 成功时，它会产生一个答案——最常见的就是 答案替换 在没有约束的 Prolog 中，答案替换总是包含一个或无限多个解1。在存在约束或粗略协调的情况下，答案现在可能包含卡住的目标或约束，必须考虑这些目标或约束以了解实际描述了哪些解决方案。

在上面的例子中，解的数量是 零 .当系统现在垃圾收集那些卡住的目标时，它实际上改变了程序的含义。

在 SICStus 中，如下所示:

| ?- q.
prolog:freeze(_A,user:false) ? ;
no

在 SWI 和 YAP 中，默认情况下不会显示这些目标，因此很可能尚未发现此类错误。

PS:以前有过 a comparison SICStus 是当时唯一通过所有测试的系统。与此同时，一些系统得到了改进。

我首先查看了 SICStus 数字:每次卡住 216 字节!那是 27 个单词，其中 13 个单词仅用于表示目标的术语。因此，卡住只需 14 个字。没那么糟糕。

PPS:卡住目标是 throw/2 ，应该是 throw/1

精美打印
1:一些例子:答案替换 X = 1只包含一个解，以及 X = [_A]包含无限多个解，如 X = [a]还有很多很多。所有这些 gets much more complex在约束条件下。