To expand on my comments, maybe this might help:
?- findall(X, member(X, [1, 2, 3]), Xs). Xs = [1, 2, 3].
If you look closely, you will see that Prolog (SWI, in this case) did not print a substitution for
X. This means that
X is not bound when the query succeeds. Indeed:
?- findall(X, member(X, [1, 2, 3]), Xs), var(X). Xs = [1, 2, 3].
This does not mean that
X is never bound while the query executes:
?- findall(X, ( member(X, [1, 2, 3]), writeln(X) ), Xs), var(X). 1 2 3 Xs = [1, 2, 3].
But after all solutions have been generated,
X is unbound and can be bound to some other value — such as the list of solutions. This will work in any standard conforming Prolog, as the standard says explicitly that
findall only tries to unify its third argument after it has created the list of solutions. It even contains an example with sharing between the template and the list of instantiations:
findall(X, (X=1;X=2), [X, Y]). Succeeds, unifying X with 1, and Y with 2.
So how does this binding and unbinding work? With a failure-driven loop, as quoted in rajashekar’s answer from the SWI-Prolog implementation. In general, succeeding predicates bind some variables. When at some later point something fails (or, equivalently, the user presses ; when prompted by the toplevel), backtracking takes place: It unbinds variables to allow them to take new values, then retries some goal.
What goes on inside
findall is the same as goes on when you write the following:
?- ( member(X, [1, 2, 3]), writeln(X), false ; true ), var(X). 1 2 3 true.
findall is very impure, it is not so impure as to be completely un-Prolog-like. In fact, we can write our own:
:- dynamic my_findall_bag/1. my_findall(Template, Goal, Instances) :- % initialization retractall(my_findall_bag(_)), asserta(my_findall_bag()), % collect solutions ( call(Goal), copy_term(Template, NewSolution), retract(my_findall_bag(PreviousSolutions)), asserta(my_findall_bag([NewSolution | PreviousSolutions])), % failure-driven loop: after saving the solution, force Goal to % generate a new one false ; true ), % cleanup and finish; the saved solutions are in reversed order (newest % first), so reverse them retract(my_findall_bag(AllSavedSolutions)), reverse(AllSavedSolutions, Instances).
This behaves as expected:
?- my_findall(X, member(X, [1, 2, 3]), Xs). Xs = [1, 2, 3].
?- my_findall(X, member(X, [1, 2, 3]), X). X = [1, 2, 3].
A minor problem with this is that the instantiation of
Goal should be checked. A major problem with this is that all
my_findall calls share the same bag, so calling
my_findall from inside a
my_findall (or in parallel) will make you unhappy. This could be fixed using some sort of
gensym mechanism to give each
my_findall run its unique key into the database.
As for the trace output, it is an unfortunate consequence of wanting to express “your goal succeeded with such-and-such bindings” on one line. At the point of success, it is true that
findall(X, ..., X) succeeded, and it is true that
X = [1, 2, 3], and hence it is true that the successful instance of the goal is
findall([1, 2, 3], ..., [1, 2, 3]).
forty_two(FortyTwo) :- var(FortyTwo), FortyTwo = 42. my_call(Goal) :- format('about to call ~w~n', [Goal]), call(Goal), format('success: ~w~n', [Goal]).
?- my_call(forty_two(X)). about to call forty_two(_2320) success: forty_two(42) X = 42.
forty_two(42) is a succeeding instance of
forty_two(X). Even though
forty_two(42) does not succeed:
?- forty_two(42). false.
It is logical that printing the term
forty_two(X) in an environment with
X = 42 prints
forty_two(42). I think the problem is that this logical behavior sticks out as strange among all the non-logical stuff going on here.
CLICK HERE to find out more related problems solutions.