为什么这个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]]）与第二个规则匹配并调用contains（[2,3]，[2,1,3]）， contains（[2,1 ，3]，[2,3]）。
3. 包含（[2,3]，[2,1,3]）失败，等于收益号

然而它仍然有效。其他尝试混淆它也是如此。有人可以向我解释吗？

（Prolog的实现：SWI-Prolog的版本2.7.12）

Answer 1

Prolog使用一种称为 “回溯” 技术。

看看第一步，您的第1步

Prolog有两个规则也可以在这里使用，如果使用你在解释选择的规则，它总是会失败。但是一旦失败，Prolog会回溯并尝试其他规则：

等于（[1,2,3]，[1,2,1,3]）： - contains（[1,2,3] ，[1,2,1,3]），包含（[1,2,1,3]，[1,2,3]）

通过找到错误答案后反复回溯，最终Prolog找到了一个解决方案是真的，因此它知道答案是真的。

如果尝试应用规则的各种可能方式，而没有找到真正的答案，答案肯定是错误的。

这是Prolog的一个非常基础的部分。我很惊讶，你没有理解它就有这么远。

Answer 2

你的代码很奇怪，但是我可以推荐你使用trace谓词来进行测试。下面是这个例子：

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