为什么这个Prolog程序没有终止？

Question

我是 Prolog 新手，我想编写一个简单的谓词来检查给定值是否在列表中。

我不知道我所学的列表方式是否正确。我被告知这是一个 car/cdr 或 head/tail 关系（熟悉 LISP/Haskell），与

[X|Xs]

“匹配”。

我第一次尝试使用这个程序：

in([ ], _) :- false.
in([X|_], X).
in([_|Xs], X) :- in(Xs, X).

现在，如果输入任何应返回

true.

的查询（例如

?- in([1, 2], 2).

），该程序不会终止。相反，它确实打印出

true

（没有句点），然后挂起。

我认为，也许在

in([X|_], X).

处遇到统一规则后，Prolog 会继续搜索与

in([_|Xs], X)

统一的其他值。我不清楚为什么这不会终止，因为递归下降总是减少参数。尽管如此，我还是尝试了这个程序：

in([ ], _) :- false.
in([X|_], X).
in([X|Xs], Y) :- in(Xs, Y), X \= Y.

我希望这会阻止 Prolog 下降到另一个规则，但这保留了之前的行为。然后我想起规则中谓词的顺序很重要，所以我尝试这样做：

in([ ], _) :- false.
in([X|_], X).
in([X|Xs], Y) :- X \= Y, in(Xs, Y).

这种行为占了上风。沮丧和怀疑我完全误解了 Prolog 评估，我尝试颠倒所有条款，达到了最奇怪的效果：

in([X|Xs], Y) :- X \= Y, in(Xs, Y).
in([X|_], X).
in([ ], _) :- false.

现在这会导致 Prolog 终止 如果列表为空或在头部找到该元素，所以：

?- in([ ], 10).
false.

?- in([1, 2], 1).
true.

?- in([1, 2], 2).
true 

然后它就挂了。

我不明白这种行为是如何发生的。 Prolog 在做什么？

我正在使用 SWI-Prolog 9.1.10

Answer 1

这是预期行为；此时按

?

（问号），SWI Prolog 将向您显示选项：

  Possible actions:
  ; (n,r,space,TAB): redo              | t:         trace&redo
  *:                 show choicepoint  | c (a,RET): stop
  w:                 write             | p:         print
  b:                 

分号、空格是继续搜索（“重做”）的。

c

和

a

bort 和 RETurn 将在那里停止。

如果确实如此，还有什么其他解决方案？

你知道没有更多了，但它没有——它不聪明。如果它可以完成搜索整个代码，它只能报告找不到更多解决方案。尝试

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

，然后尝试

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

，看看他们如何找到多个解决方案。