发现者的异常行为



以下内容看起来很不寻常:

?- findall(X, member(X, [1, 2, 3]), X).
X = [1, 2, 3].

痕迹更是如此

?- trace, findall(X, member(X, [1, 2, 3]), X).
^  Call: (11) findall(_100058, member(_100058, [1, 2, 3]), _100058) ? creep
^  Exit: (11) findall([1, 2, 3], user:member([1, 2, 3], [1, 2, 3]), [1, 2, 3]) ? creep
X = [1, 2, 3]

从语义的角度思考findall这没有什么意义。这是怎么回事?

为了扩展我的评论,也许这可能会有所帮助:

?- findall(X, member(X, [1, 2, 3]), Xs).
Xs = [1, 2, 3].

如果你仔细观察,你会发现Prolog(在这种情况下是SWI)没有打印X的替代品。这意味着查询成功时不绑定X。事实上:

?- findall(X, member(X, [1, 2, 3]), Xs), var(X).
Xs = [1, 2, 3].

这并不意味着在执行查询永远不会绑定X

?- findall(X, ( member(X, [1, 2, 3]), writeln(X) ), Xs), var(X).
1
2
3
Xs = [1, 2, 3].

但是,在生成所有解决方案后,X是未绑定的,并且可以绑定到其他值,例如解决方案列表。这将适用于任何符合Prolog的标准,因为该标准明确指出,findall仅在创建解决方案列表后尝试统一其第三个参数。它甚至包含一个在模板和实例列表之间共享的示例:

findall(X, (X=1;X=2), [X, Y]).
Succeeds, unifying X with 1, and Y with 2.

那么这种绑定和解绑是如何工作的呢?使用故障驱动的循环,正如 rajashekar 在 SWI-Prolog 实现中的回答中所引用的那样。通常,后续谓词绑定一些变量。当稍后的某个时间点失败时(或者,等效地,用户在顶级提示时按;),就会发生回溯:它取消绑定变量以允许它们采用新值,然后重试某个目标。

findall内部发生的事情与编写以下内容时发生的情况相同:

?- ( member(X, [1, 2, 3]), writeln(X), false ; true ), var(X).
1
2
3
true.

因此,虽然findall非常不纯洁,但它并没有不纯洁到完全不像Prolog。事实上,我们可以自己写:

:- dynamic my_findall_bag/1.
my_findall(Template, Goal, Instances) :-
% initialization
retractall(my_findall_bag(_)),
asserta(my_findall_bag([])),

% collect solutions
(   call(Goal),
copy_term(Template, NewSolution),
retract(my_findall_bag(PreviousSolutions)),
asserta(my_findall_bag([NewSolution | PreviousSolutions])),
% failure-driven loop: after saving the solution, force Goal to
% generate a new one
false
;   true ),
% cleanup and finish; the saved solutions are in reversed order (newest
% first), so reverse them
retract(my_findall_bag(AllSavedSolutions)),
reverse(AllSavedSolutions, Instances).

这将按预期运行:

?- my_findall(X, member(X, [1, 2, 3]), Xs).
Xs = [1, 2, 3].

甚至:

?- my_findall(X, member(X, [1, 2, 3]), X).
X = [1, 2, 3].

这样做的一个小问题是应该检查Goal的实例化。这样做的一个主要问题是所有my_findall呼叫共享同一个包,因此从my_findall内部(或并行)呼叫my_findall会让您不高兴。可以使用某种gensym机制来修复此问题,以使每个my_findall将其唯一密钥运行到数据库中。

至于跟踪输出,这是想要在一行上表达"你的目标通过某某绑定成功"的不幸结果。在成功的时候,findall(X, ..., X)成功了X = [1, 2, 3]也确实成功了,因此目标的成功实例是findall([1, 2, 3], ..., [1, 2, 3])的。

考虑:

forty_two(FortyTwo) :-
var(FortyTwo),
FortyTwo = 42.
my_call(Goal) :-
format('about to call ~w~n', [Goal]),
call(Goal),
format('success: ~w~n', [Goal]).

例如:

?- my_call(forty_two(X)).
about to call forty_two(_2320)
success: forty_two(42)
X = 42.

所以forty_two(42)forty_two(X)的继任实例。即使forty_two(42)没有成功:

?- forty_two(42).
false.

在具有X = 42打印的环境中打印术语forty_two(X)合乎逻辑forty_two(42)。我认为问题在于,这种逻辑行为在这里发生的所有非逻辑事物中都很奇怪。

我做了一些代码潜水来尝试弄清楚发生了什么。在 swi-prolog 中,listing(findall, [source(true)]).给出了以下代码:

findall(Templ, Goal, List) :-
findall(Templ, Goal, List, []).
findall(Templ, Goal, List, Tail) :-
setup_call_cleanup(
'$new_findall_bag',
findall_loop(Templ, Goal, List, Tail),
'$destroy_findall_bag').

相应文件中的findall_loop如下:

findall_loop(Templ, Goal, List, Tail) :-
(   Goal,
'$add_findall_bag'(Templ)   % fails
;   '$collect_findall_bag'(List, Tail)
).

在查阅了 C 源文件后,我发现findall/4正在 C-source ('$new_findall_bag') 中设置一个全局变量,并且当Goal成功(使用'$add_findall_bag'(Templ))时,findall_loop/4Templ推送到它。当Goal失败时Templ未实例化,因此即使ListTempl是同一变量,最终子句'$collect_findall_bag'(List, Tail)也会成功。

我们可以在跟踪中看到Templ通常是未实例化的。

?- trace, findall(X, member(X, [1, 2, 3]), Xs).
^  Call: (11) findall(_28906, member(_28906, [1, 2, 3]), _28916) ? creep
^  Exit: (11) findall(_28906, user:member(_28906, [1, 2, 3]), [1, 2, 3]) ? creep
Xs = [1, 2, 3].

因此,查找Templ的所有实例化以使Goal成功的过程与将所有这些实例化收集到变量List中的过程是分开的,因此我们可以使用相同的变量而不会引起和错误。但是写这样一个子句的语义对我来说没有多大意义。

编辑:类似的情况发生在gprolog,其中收集解决方案的过程和检索它们的过程是分开的。相关Yap代码看起来也很相似,但我无法安装它进行检查。

最新更新