Why does this Prolog predicate works?

Question

I have the following code: Bear in mind that while this code works on lists, these lists represent sets, so [1,1,2,2,3,3] and [1,2,3] should be equivalent.

%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).

The idea is that equals([1,2,3],[1,2,1,3]) should return true. However, based on the above definition what I would expect to happen is the following:

1. equals([1,2,3],[1,2,1,3]) matches the first rule, and invokes equals([2,3],[2,1,3]]).
2. equals([2,3],[2,1,3]]) matches the second rule and invokes contains([2,3], [2,1,3]), contains([2,1,3], [2,3]).
3. contains([2,3], [2,1,3]) fails, and equals returns No.

And yet it still works. And so do other attempts to confuse it. Can someone please explain it to me?

(Prolog implementation: SWI-Prolog Version 2.7.12)

Answer 1

Prolog uses a technique called "backtracking".

Take a look at the first step, your step 1.

Prolog has two rules it can use here, if it uses the rule you chose in your explanation, it will always fail. But once it has failed, Prolog will backtrack and try the alternative rule:

equals([1,2,3],[1,2,1,3]) :- contains([1,2,3],[1,2,1,3]), contains([1,2,1,3],[1,2,3])

By repeatedly backtracking after finding false answers, eventually Prolog finds a solution which is true, and thus it knows the answer is true.

If if tried every possible way of applying the rules, without finding a true answer, the answer must be false.

This is a very fundamental part of Prolog. I am surprised you got this far without understanding it.

Answer 2

Your code is very strange, however I can recommend you to use trace predicate for testing purposes. Here is the example:

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