How does backtracking in recursion not cause an infinite loop?

Question

Assume the member/2 predicate is defined as:

member(X,[X|R]).
member(X,[Y|R]) :- member(X,R).

My query is:

member(X, [1, 2, 3]).

Once prolog unifies X with 1, how does prolog get the other possible unifications if I type ;? Wouldn't Prolog backtrack and then re-read my file containing the definition of member from top to bottom and evaluate member(X,[X|R]). again which would unify X with 1 again?

Answer 1

How about this

Note the following:

• The program is read once and then stays in memory, waiting for the user to enter a query (same as for a database scenario)
• As it executes it builds a "search tree" in memory
  • An OR node for every predicate encountered: ANY of the branches (which correspond to clauses of that predicate) must be made TRUE
  • An AND node for every clause body encountered: all the branches (which correspond to the calls made in the clause body that are seprated by ,) must be made TRUE
• The program SUCCEEDS when it can "exit at the bottom of the tree" and
  • Below any AND node, all the branches are TRUE
  • Below any OR node, at least one of the branches are TRUE (In Prolog, there is only every exactly ONE "active branch" below an OR node)
• The program eventually FAILS if no such tree can be found (which may take some time).
• On program success, the tree is kept alive in case the user ask for "more solutions"
• If you ask for "more solutions", the tree is re-entered at the bottom and alternative branches are tried.

And:

• Variable names are local to a clause
• Variable content (which is either a term or a cell with no content if the "variable is unbound" as they say) is always global. If a node deep in the tree "refines" the content of one of its variable, this change is visible at the topmost node of the tree (albeit under another name or part of another term).