この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. equals（[1,2,3]、[1,2,1,3]）が最初のルールに一致し、 （[2,3]、[2,1,3]]）と等しくなります。
2. equals（[2,3]、[2,1,3]]）は第2の規則と一致し、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はそれはそれはあなたがあなたの説明で選択したルールを使用している場合、それは常に失敗します、ここで使用できる2つのルールがあります。しかし、一旦それが失敗すると、Prologは代替ルールを取り戻して試してみるでしょう：

は（[1,2,3]、[1,2,1,3]）と等しいです： - （[1,2,3] [1,2,1,3]）は、（[1,2,1,3]、[1,2,3]）を含みます。

偽の回答を見つけた後、繰り返して後戻りすることによって、最終的にPrologはそれは答えが真であることを知っている。

本当の答えを見つけることなく、ルールを適用する可能性のある方法を試した場合、答えは偽でなければなりません。

これは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