SWI-Пролог: Проверьте членство элементов в нескольких списках

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. 

Теперь каждое решение имеет две переменные привязки.

Если у вас есть проблемы со зрением, как Пролог идет о попытке найти доказательство последнего запроса, вы можете даже смотреть на фактическое доказательство дерева:

?- 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.