prolog - 为什么 prolog 在简单的经典 member/2 实现中创建选择点？

Question

下面是member/2函数的经典教科书示例。

member(X,[X|_]).
member(X,[_|T]) :- member(X,T).

这个特定的来自开创性的立即学习 Prolog。

发出以下查询时

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

结果是:

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

问。为什么结果不仅为真，而且为真然后为假？是什么导致序言在与第一个(非递归)规则成功匹配后回溯？

SWI-Prolog MacOS 实现和在线 SWISH 实现都给出了上述结果。

Answer 1

Why does prolog create choice points in the simple classic member/2 implementation?

其他答案告诉您这是正确的，但我认为他们没有回答为什么会这样。还有注意。 Prolog 不知道这是一个“简单经典”和特殊外壳，它与其他普通 [1] Prolog 代码相同的证明搜索:每当它做出选择时，它都会留下一个选择点所以它以后可以回来，知道它去过哪里，哪里还没有探索。

1. member(X,[X|_]).
2. member(X,[_|T]) :- member(X,T).

您的查询 ?- member(1, [1,2,3]). 与规则 1 统一； Prolog 选择规则 1 并设置一个选择点说“还有更多我还没有搜索的成员规则”，现在它会继续你的查询的其余部分，只是没有了，就是这样，有一个解决方案，没有需要再搜索；它回答 true 并在顶层等待您。

如果您对它找到的解决方案感到满意，您可以停止搜索，它将不再搜索。相反，如果您要求它继续搜索其他解决方案，则选择点的踪迹表明还有未探索的搜索空间，它们是下一步应该尝试的记录。 Prolog 将返回到最近的选择点并尝试寻找另一条前进的道路，它尝试下一个成员谓词，规则 2，遵循递归链并找不到更多的解决方案，现在已经用完了选择，所以它回答 false，没有找到更多的解决方案。

This specific one is from the seminal Learn Prolog Now.

证明搜索上有一个页面:Learn Prolog Now page on Proof Search但自相矛盾的是，它枯燥得令人眼花缭乱，所以我不会去读它，而是会搜索一些可以引用的东西，这样我就可以假装我读过它；它说:

Points in the search where there are several alternative ways of unifying a goal against the knowledge base are called choice points. Prolog keeps track of choice points it has encountered, so that if it makes a wrong choice it can retreat to the previous choice point and try something else instead. This process is called backtracking, and it is fundamental to proof search in Prolog.

[1] 其他搜索策略可用，优化也可以让 Prolog 系统告诉某些规则在没有实际尝试的情况下将不适用。