Почему этот предикат Prolog работает?

Question

У меня есть следующий код: Имейте в виду, что, хотя этот код работает в списках, эти списки представляют собой множества, поэтому [1,1,2,2,3,3] и [1,2,3] должны быть эквивалентными ,

%contains(L1, L2), returns true if L1 contains L2 
contains(_, []). 
contains(L1, [Head|Tail]) :- member(Head, L1), contains(L1, Tail). 
%equals(L1, L2), returns true if L1 is equal to L2 
equals([X|L1],[X|L2]) :- equals(L1, L2). 
equals(L1, L2) :- contains(L1, L2), contains(L2, L1). 

Идея состоит в том, что равенства ([1,2,3], [1,2,1,3]) должны возвращать значение true. Однако, исходя из приведенного выше определения, я бы предположил, что следующее:

1. равно ([1,2,3], [1,2,1,3]) соответствует первому правилу и вызывает равна ([2,3], [2,1,3]]).
2. equals ([2,3], [2,1,3]]) соответствует второму правилу и содержит ссылки ([2,3], [2,1,3]), содержит ([2,1 , 3], [2,3]).
3. содержит ([2,3], [2,1,3]) выходит из строя, и равна возвращается No.

И все же он до сих пор работает. И другие попытки запутать его. Может кто-нибудь, пожалуйста, объясните мне это?

(реализация Пролог: SWI-Prolog версии 2.7.12)

Answer 1

Пролог использует метод, называемый "откат".

Взгляните на первый шаг, ваш шаг 1.

Пролог имеет два правила можно использовать здесь, если он использует правило, которое вы выбрали в своем объяснении, он всегда будет терпеть неудачу. Но как только он потерпит неудачу, Prolog вернется и попробует альтернативное правило:

равно ([1,2,3], [1,2,1,3]): - содержит ([1,2,3] , [1,2,1,3]), содержит ([1,2,1,3], [1,2,3])

Повторно обратный поиск после нахождения ложных ответов, в конечном итоге Prolog находит решение, которое истинно, и, следовательно, он знает, что ответ верен.

Если при попытке использовать все возможные способы применения правил, не найдя истинного ответа, ответ должен быть ложным.

Это очень фундаментальная часть Пролога. Я удивлен, что вы так далеко дошли, не понимая этого.

Answer 2

Ваш код очень странный, однако я могу порекомендовать вам использовать предикат трассировки для целей тестирования. Вот пример:

4 ?- trace([equals,contains]). 
%   equals/2: [call, redo, exit, fail] 
%   contains/2: [call, redo, exit, fail] 
true. 

[debug] 5 ?- equals([1,2,3],[1,2,1,3]). 
T Call: (7) equals([1, 2, 3], [1, 2, 1, 3]) 
T Call: (8) equals([2, 3], [2, 1, 3]) 
T Call: (9) equals([3], [1, 3]) 
T Call: (10) contains([3], [1, 3]) 
T Fail: (10) contains([3], [1, 3]) 
T Fail: (9) equals([3], [1, 3]) 
T Redo: (8) equals([2, 3], [2, 1, 3]) 
T Call: (9) contains([2, 3], [2, 1, 3]) 
T Call: (10) contains([2, 3], [1, 3]) 
T Fail: (10) contains([2, 3], [1, 3]) 
T Fail: (9) contains([2, 3], [2, 1, 3]) 
T Fail: (8) equals([2, 3], [2, 1, 3]) 
T Redo: (7) equals([1, 2, 3], [1, 2, 1, 3]) 
T Call: (8) contains([1, 2, 3], [1, 2, 1, 3]) 
T Call: (9) contains([1, 2, 3], [2, 1, 3]) 
T Call: (10) contains([1, 2, 3], [1, 3]) 
T Call: (11) contains([1, 2, 3], [3]) 
T Call: (12) contains([1, 2, 3], []) 
T Exit: (12) contains([1, 2, 3], []) 
T Exit: (11) contains([1, 2, 3], [3]) 
T Exit: (10) contains([1, 2, 3], [1, 3]) 
T Exit: (9) contains([1, 2, 3], [2, 1, 3]) 
T Exit: (8) contains([1, 2, 3], [1, 2, 1, 3]) 
T Call: (8) contains([1, 2, 1, 3], [1, 2, 3]) 
T Call: (9) contains([1, 2, 1, 3], [2, 3]) 
T Call: (10) contains([1, 2, 1, 3], [3]) 
T Call: (11) contains([1, 2, 1, 3], []) 
T Exit: (11) contains([1, 2, 1, 3], []) 
T Exit: (10) contains([1, 2, 1, 3], [3]) 
T Exit: (9) contains([1, 2, 1, 3], [2, 3]) 
T Exit: (8) contains([1, 2, 1, 3], [1, 2, 3]) 
T Exit: (7) equals([1, 2, 3], [1, 2, 1, 3]) 
true