SWI-Prolog：检查多个列表中的元素成员资格

Question

所以我有一个隶属函数，它告诉我X 何时不在L 中：

not_in(X, L) :- not(member(X,L)).

根据需要工作：

83 ?- not_in(5,[3,4]).
true.

但是，我也有一个生成许多列表的函数：

84 ?- manyLists(_,L).
L = [5, 11] ;
L = [3, 4] ;
L = [16, 22] ;
false.

我要做的是检查X 是否不在任何列表中：

manyLists(_,L), not_in(X,L).

但是，这会返回：

85 ?- manyLists(_,L), not_in(32,L).
L = [5, 11] ;
L = [3, 4] ;
L = [16, 22] ;
false.

即它应该返回 true，因为 32 不在这些列表中。

我做错了什么？

Answer 1

你没有做错任何事，但你可能没有正确解释你得到的解决方案。

首先，当您有一个成功多次的谓词时，这被称为（有点误导）非确定性行为：一个查询返回多个解决方案。

假设你问，“1 到 3 之间是哪个数字？”：

?- between(1, 3, X).
X = 1 ;
X = 2 ;
X = 3.

你得到三个解决方案。每个都有一个变量绑定：X = 1、X = 2 和 X = 3。

?- between(1, 3, X), succ(X, Y).
X = 1, Y = 2 ;
X = 2, Y = 3 ;
X = 3, Y = 4.

现在每个解决方案都有两个变量绑定。

?- between(1, 3, X), X rem 2 =:= 0.
X = 2 ;
false.

如果您无法了解 Prolog 如何尝试为最后一个查询找到证明，您甚至可以查看实际的证明树：

?- trace(between/3), trace('=:='/2).
%         between/3: [call,redo,exit,fail]
%         (=:=)/2: [call,redo,exit,fail]
true.

[debug]  ?- between(1, 3, X), X rem 2 =:= 0.
 T Call: (8) between(1, 3, _G1248)
 T Exit: (8) between(1, 3, 1)
 T Call: (8) 1 rem 2=:=0
 T Fail: (8) 1 rem 2=:=0
 T Redo: (8) between(1, 3, _G1248)
 T Exit: (8) between(1, 3, 2)
 T Call: (8) 2 rem 2=:=0
 T Exit: (8) 2 rem 2=:=0
X = 2 ;
 T Redo: (8) between(1, 3, _G1248)
 T Exit: (8) between(1, 3, 3)
 T Call: (8) 3 rem 2=:=0
 T Fail: (8) 3 rem 2=:=0
false.

对于您的问题：您想表明对于列表的所有可能绑定，该列表中没有一个数字。

您的原始查询，已简化：

?- ( L = [5,11] ; L = [3,4] ; L = [16,22] ), \+ member(32, L).
L = [5, 11] ;
L = [3, 4] ;
L = [16, 22].

将其包装在 SWI-Prolog 谓词 forall/2 中：

?- forall( ( L = [5,11] ; L = [3,4] ; L = [16,22] ), \+ member(32, L) ).
true.

?- forall( ( L = [5,11] ; L = [3,4] ; L = [16,22] ), \+ member(3, L) ).
false.

如果你查看forall/2的帮助，你会看到forall(Cond, Action)的语义是\+ ( Cond, \+ Action )，即：“没有条件不能证明动作。”

?- \+ ( ( L = [5,11] ; L = [3,4] ; L = [16,22] ), \+ \+ member(32, L) ).
true.