Search code examples
prolog

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


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.


Solution

  • 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.