Why does prolog create choice points in the simple classic member/2 implementation?

Question

The following is a classic textbook example of the member/2 function.

member(X,[X|_]).
member(X,[_|T]) :- member(X,T).

This specific one is from the seminal Learn Prolog Now.

When the following query is issued

?- member(1, [1,2,3]).

The result is:

?- member(1, [1,2,3]).
true ;
false.

Q. Why is the result not just true, but true and then false? What is causing prolog to backtrack after the successful match with the first (non-recursive) rule?

The SWI-Prolog MacOS implementation, and the online SWISH implementation both give the above result.

Answer 1

Because member(1,[1,1,1]). should not be just a single true.

?- member(1,[1,1,1]).
true ;
true ;
true.

Remember Prolog uses Unficiation so you have to think about how the code needs to work if all variables are used.

You might prefer memberchk(1,[1,1,1]).

?- memberchk(1,[1,1,1]).
true.

Answer 2

Why does prolog create choice points in the simple classic member/2 implementation?

The other answers are telling you that it's correct, but I think they aren't answering why it happens. And NB. Prolog is not aware that this is a "simple classic" and special casing it, it's the same proof search as other plain[1] Prolog code: whenever it makes a choice, it leaves a choicepoint so it can come back later, know where it has been and where is still unexplored.

1. member(X,[X|_]).
2. member(X,[_|T]) :- member(X,T).

Your query ?- member(1, [1,2,3]). unifies with rule 1; Prolog chooses rule 1 and sets a choicepoint saying "there are more member rules I haven't searched yet" and now it would continue with the rest of your query only there isn't any more, so that's it, there's a solution, no need to search any more; it answers true and waits for you at the toplevel.

If you are happy with the solution it has found, you can stop the search and it will not search anymore. If, instead, you ask it to continue searching for other solutions, the trail of choicepoints says that there is unexplored space to search, and they are the record of where it should try next. Prolog will go back to the most recent choicepoint and try to find another way forward, it tries the next member predicate, rule 2, follows the recursive chain and finds no more solutions, and has now run out of choices, so it answers false, no more solution found.

This specific one is from the seminal Learn Prolog Now.

That has a page on the proof search: Learn Prolog Now page on Proof Search but it is, paradoxically, eyewarteringly dry so I'm going to not read it and will instead just search for something to quote so I can pretend I did read it; it says:

Points in the search where there are several alternative ways of unifying a goal against the knowledge base are called choice points. Prolog keeps track of choice points it has encountered, so that if it makes a wrong choice it can retreat to the previous choice point and try something else instead. This process is called backtracking, and it is fundamental to proof search in Prolog.

[1] other search strategies are available, and so are optimisations which let Prolog systems tell that some rules will not apply without actually trying them.

Answer 3

Why is the result not just true, but true and then false?

The definition of member/2 may succeed further times. To decide this, it is necessary to explore the remaining list. This costs in proportion to the size of (the longest list prefix of) the list argument. Consider:

?- member(1,[1,2,3|Es]).
   true
;  Es = [1|_A]
;  Es = [_A,1|_B]
;  Es = [_A,_B,1|_C]
;  ... .
?- member(E,[1,2,3|Es]).
   E = 1
;  E = 2
;  E = 3
;  Es = [E|_A]
;  Es = [_A,E|_B]
;  Es = [_A,_B,E|_C]
;  ... .

Both questions produce redundancy in their answers. The first answer together with the 2nd Es = [1|_A] (in the first question) and the 4th Es = [E|_A] (in the second question) may hold simultaneously.

?- member(1,[1,2,3,1]).
   true
;  true.  % same as 1st answer
?- member(E,[1,2,3,1]).
   E = 1
;  E = 2
;  E = 3
;  E = 1. % same as 1st answer

A clean way out of this situation is to use a better definition of member/2 called memberd/2.

?- memberd(1,[1,2,3,1]).
   true.
?- memberd(1,[1,2,3,1|Es]).
   true.
?- memberd(E,[1,2,3,1]).
   E = 1
;  E = 2
;  E = 3
;  false.
?- memberd(E,[1,2,3|Es]).
   E = 1
;  E = 2
;  E = 3
;  Es = [E|_A], dif:dif(E,1), dif:dif(E,2), dif:dif(E,3)
;  Es = [_A,E|_B], dif:dif(E,_A), dif:dif(E,1), dif:dif(E,2), dif:dif(E,3)
;  ... .

The price for this definition is that constraints dif/2 are needed to exclude redundancies in certain situations.

Answer 4

Indexing is primarily done on the first argument: https://www.swi-prolog.org/pldoc/man?section=jitindex

... which is why member/3 in swi-prolog is defined as:

?- listing(member).
lists:member(El, [H|T]) :-
    member_(T, El, H).

?- listing(member_).
lists:member_(_, El, El).
lists:member_([H|T], El, _) :-
    member_(T, El, H).

... which prevents a dangling choicepoint after checking the last entry in the list.

To boil your question down to the simplest example:

?- member(1, [1, 2]).
true ;
false.

The first answer is simply true, because 1 = 1, and there is no other useful information to show, e.g. no variable involved.

The second answer is false, because 1 cannot unify with the other elements in the list, i.e. [2]. So, false means that, after checking, there are no further successes.

This is shown better with (using swi-prolog's https://www.swi-prolog.org/pldoc/man?predicate=member/2 ):

?- X = 1, member(X, [1, 2]).
X = 1 ;
false.

?- X = 2, member(X, [1, 2]).
X = 2.

Prolog supports multiple answers, which is closer to real-life than imperative languages :-)

If you really want to avoid a choicepoint, then there are several options, e.g. !, once/1 and memberchk/2.