The fastest way to illustrate my confusion is this minimal contrived example I've cooked up:
connected(a,b).
connected(b,c).
step(From, To) :- connected(From, To).
step(To, From) :- connected(From, To).
path(From, To, Steps) :- step(From, To), Steps = [(From, To)].
path(From, To, [(From, Middle) | Rest]) :-
step(From, Middle),
\+ member((From, Middle), Rest),
% without the above line, ?- path(a,c,Steps). Steps = [(a,b),(b,c)]; etc...
% but with the above line, ?- path(a,c,Steps). false.
path(Middle, To, Rest).
Of course, if I implement a predicate like not_member, like so:
not_member(_, []).
not_member(X, [Y | Ys]) :- dif(X, Y), not_member(X, Ys).
and use that instead of \+ member, the results will be found. My question is not about solving this contrived example, but rather deepening my understanding of the \+ operator, and perhaps also understanding how Prolog goes about exploring the solution space.
Without the \+ member condition, Prolog is able to find solutions for path(a,c,Steps), I take it that Prolog does get around to considering solutions like:
From=a, To=c, Middle=b, Rest=[(b,c)]
For which I would assume then, when I uncomment the \+ member check, then when it goes to try to prove member((a,b), [(b,c)]) it will fail, continuing over \+ member and finding a suitable solution.
However, if I trace. the execution with the \+ member call I get:
[trace] ?- path(a,c,Steps).
Call: (12) path(a, c, _46240) ? creep
Call: (13) step(a, c) ? creep
Call: (14) connected(a, c) ? creep
Fail: (14) connected(a, c) ? creep
Redo: (13) step(a, c) ? creep
Call: (14) connected(c, a) ? creep
Fail: (14) connected(c, a) ? creep
Fail: (13) step(a, c) ? creep
Redo: (12) path(a, c, _46240) ? creep
Call: (13) step(a, _54058) ? creep
Call: (14) connected(a, _54058) ? creep
Exit: (14) connected(a, b) ? creep
Exit: (13) step(a, b) ? creep
Call: (13) lists:member((a, b), _54052) ? creep
Exit: (13) lists:member((a, b), [(a, b)|_58132]) ? creep
Redo: (13) step(a, _54058) ? creep
Call: (14) connected(_54058, a) ? creep
Fail: (14) connected(_54058, a) ? creep
Fail: (13) step(a, _54058) ? creep
Fail: (12) path(a, c, _46240) ? creep
false.
It seems to be considering:
lists:member((a, b), [(a, b)|_58132])
and then failing the search entirely.
What's going on here? Why is it considering [(a, b)|_58132] for Rest e.g. instead of considering [(b,c)] as it does when I comment out the \+ member check?
Clearly I am missing a lot of understanding of how Prolog works internally, so answers that are indirect and point me to more resources for learning rather than addressing the question directly would still be appreciated.
I am using swi-prolog, if it matters.
Edit:
It would probably help for me to write out my full understanding of what I expect the Prolog engine to do:
path(a, c, Steps)pathstep(a, c), Steps = [(a, c)].step(a, c).step predicate: connected(a, c) failsstep: connected(c, a), also failspath:step(a, Middle), \+ member((a, Middle), Rest), path(Middle, c, Rest).step(a, Middle)connected(a,b) gives a success with Middle=b.step(a, b), \+ member((a, b), Rest), path(b, c, Rest).member((a,b), Rest) I believe should fail because Rest is uninstantiated, so Prolog cannot prove member((a,b), Rest) at this point, so \+ member((a,b), Rest) should pass.path(b, c, Rest) is a recursive call.path(b, c, Steps) :- step(b, c), Steps = [(b, c)].Rest=[(b,c)].path(a, c, Steps) succeeds with Steps = [(a, b), (b, c)].Clearly something here is wrong because this isn't what the engine does. Where am I off?
Edit 2: I think I get it now. In step 12 where \+ member((a,b), Rest) is called, Rest is uninstantiated, but that doesn't mean \+ member((a,b), Rest) passes, what it means is Prolog immediately goes about trying to satisfy it, it tries first by binding Rest to [(a,b)|_58132], which is enough to satisfy member((a,b), Rest) immediately and so \+ member((a,b), Rest) fails.
Your question boils down to the following two simpler questions:
\+?- \+ member((a,b), Rest).
false. % why-oh-why?
?- member((a,b), Rest).
Rest = [(a,b)|_A]
; Rest = [_A,(a,b)|_B]
; ... .
?- not_member((a,b), Rest).
Rest = [] % this is expected
; ... .
While not_member/2 does find answers as expected, the version with (\+)/1 fails. So what is this (\+)/1? It is commonly called not — the standard calls it in 8.15.1 more accurately not provable. But even that name could be refined to its actual meaning not provable at this point in time of execution.
From a logical viewpoint one could call it a negation with dynamical (voir quasiment random) changes of quantification of the variables involved. To see this a bit better, consider
?- Rest = [], \+ member((a,b), Rest).
Rest = [].
?- \+ member((a,b), Rest), Rest = [].
false. % again, unexpected
So this version agrees with not_member/2 in the first query, and disagrees with it in the second. As a consequence, commutativity1 does not hold. You can imagine how brittle such a construct is as you have to keep track how it is used exactly.
What to do in such a situation?
One possibility would be to use pure versions as your not_member/2 (which is more commonly called non_member/2 or simply maplist(dif(X),Xs)). This is still a developing area see library(reif).
The other possibility is to check that the query is sufficiently instantiated and to produce an error otherwise. See when_si/2. But then, this reduces the applicability of your program. It's like when you are forced to downgrade from using clpfd/clpz to (is)/2 and the related comparison built-ins.
But there is another problem in your program! Termination. So lets consider the version with not_member/2. It does not terminate for your query!
?- path(a,c,Steps). Steps = [(a,b),(b,c)] ; loops.
So when asking for the next solution, Prolog loops. In fact, even the following failure-slice does not terminate!
?- path(a,c,Steps). loops. connected(a,b).connected(b,c) :- false. step(From, To) :- connected(From, To).step(To, From) :- false, connected(From, To).path(From, To, Steps) :- false, step(From, To), Steps = [(From, To)]. path(From, To, [(From, Middle) | Rest]) :- step(From, Middle), not_member((From, Middle), Rest), false,path(Middle, To, Rest).not_member(_, []) :- false. not_member(X, [Y | Ys]) :- dif(X, Y), not_member(X, Ys), false.
Note how few lines are left. In particular, there is no longer a cycle, since step/2 has been reduced to a single clause. In order to remove that problem you need to change the visible part somehow. See path/4 for a generic solution.
Ah, and there is another thing to note. You have seen it yourself. You used this tracer in SWI and were not able to draw any conclusions out of it, because it produced much too much detail (and worse, it is even buggy itself for more complex programs). Tracers or d-buggers may help with highly procedural code, but the purer your programs are, the lesser their value. Even for procedural problems as non-termination above. The reason is us humans cannot process these walls of text tracers produce. Just like you are not able to follow the electrons that are swirling around in your computer. It is key for a programmer to understand this limitation and search for means to attack it nevertheless effectively. The slicing technique above is one of such means.
1 commutativity modulo non-termination, errors, and resource consumption