prologprolog-findall

Unusual behaviour of findall


The following looks very unusual :

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

The trace even more so

?- trace, findall(X, member(X, [1, 2, 3]), X).
^  Call: (11) findall(_100058, member(_100058, [1, 2, 3]), _100058) ? creep
^  Exit: (11) findall([1, 2, 3], user:member([1, 2, 3], [1, 2, 3]), [1, 2, 3]) ? creep
X = [1, 2, 3]

Thinking in terms of semantics of findall this makes little sense. What is going on?


Solution

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

    So while 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].
    

    Or even:

    ?- 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]).

    Consider:

    forty_two(FortyTwo) :-
        var(FortyTwo),
        FortyTwo = 42.
    
    my_call(Goal) :-
        format('about to call ~w~n', [Goal]),
        call(Goal),
        format('success: ~w~n', [Goal]).
    

    For example:

    ?- my_call(forty_two(X)).
    about to call forty_two(_2320)
    success: forty_two(42)
    X = 42.
    

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