冻结/ 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 : global stack in use = 108   MB
(AMD64) B-Prolog       8.1   : stack+heap   in use = 145   MB
(i386)  Ciao Prolog    1.14.2: global stack in use =  36   MB (~72 MB w/AMD64)
(AMD64) SWI-Prolog     7.3.1 : global stack in use =   0.5 MB
(AMD64) YAProlog       6.2.2 : global stack in use =  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超过一个数量级？

我的直觉倾向于"归因变量"与"垃圾收集"的相互作用.与其他Prolog处理器相比,SWI-Prolog和YAProlog有(共享？)不同的属性变量API和实现......然后,它可能会完全不同.谢谢!

Answer 1

TL;DR：SWI 中的错误不再存在！

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

所以考虑一下就足够了freeze(_,false)。

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

p :-
   false.

q :-
   freeze(_,false).

然而，从程序上来说，第一个目标失败了，而第二个目标成功了。在这种情况下，区分解决方案和答案是关键。当 Prolog 成功时，它会产生一个答案 - 最常见的是，这在 Prolog 中称为无约束答案替换，其中答案替换始终包含一个或无限多个解决方案¹。在存在约束或粗略协同的情况下，答案现在可能包含冻结的目标或约束，必须考虑这些目标或约束才能理解实际描述了哪些解决方案。

在上述情况下，解决方案的数量为零。当系统现在垃圾收集这些冻结的目标时，它实际上改变了程序的含义。

在 SICStus 中显示如下：

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

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

PS：过去曾对各种有关GC和约束的系统进行过比较，SICStus是当时唯一通过所有测试的系统。与此同时，一些系统得到了改进。

我首先查看了 SICStus 数字：每次冻结 216 字节！共有 27 个单词，其中 13 个单词代表目标。所以只需 14 个字就可以冻结。还不错。

PPS：冻结的目标是throw/2，本来应该是throw/1

^{细则 1：一些示例：答案替换X = 1仅包含一个解决方案，并且X = [_A]包含无限多个解决方案X = [a]，例如很多很多其他解决方案。在约束的背景下，所有这一切都变得更加复杂。}