Prolog - why does the following code generate the solution X=root forever?

83 Views Asked by At
black(root). 
black(v1). 
black(v3). 
black(v4). 

edge(root,root).
edge(v1,root). 
edge(v2,v1). 
edge(v3,v1). 
edge(v4,v3). 
edge(v5,v2). 
edge(v5,v4). 
edge(v6,v5). 

foo(root). 
foo(X) :- edge(X,Y), black(Y), foo(Y).

Then I type foo(X) and only get X=root.

I really can't figure out why. We get the first root because of the first part of foo. Then we are supposed to go the the second part, we then proceed to find the edge (root,root). black(root) returns true and so does foo(root) so we get another root solution. Why don't we then go to the edge (v1,root)? What am I missing?

2

There are 2 best solutions below

0
Scott Hunter On BEST ANSWER

Because looking for the 3rd solution starts with retrying foo(Y) when Y=root, and you've already established there are at least 2 distinct ways to prove foo(root). (But, as @WillemVanOnsem points out, it is much worse than that.)

0
false On

Here is a fragment that is responsible for non-termination called a . You need to modify the remaining part somehow in order to avoid that loop.

black(root).
black(v1) :- false. 
black(v3) :- false. 
black(v4) :- false. 

edge(root,root).
edge(v1,root) :- false. 
edge(v2,v1) :- false. 
edge(v3,v1) :- false. 
edge(v4,v3) :- false. 
edge(v5,v2) :- false. 
edge(v5,v4) :- false. 
edge(v6,v5) :- false. 

foo(root) :- false. 
foo(X) :- edge(X,Y), black(Y), foo(Y), false.

The easiest way to solve this is to reuse closure0/3.

edgeb(X, Y) :-
   edge(X, Y),
   black(Y).

foo(X) :-
   closure0(edgeb, X, root).

... or change your facts. The failure-slice above showed us that the edge(root,root). was part of the problem. What, if we just remove that very fact? Or turn it into

edge(root,root) :- false.

Now foo(X) terminates:

?- foo(X).
   X = root
;  X = v1
;  X = v2
;  X = v3
;  X = v4
;  X = v5
;  false.

To avoid hammering ; or SPACE so many times, your carpal tunnels recommend:

?- foo(X), false.
false.

By that we have proven that your program will terminate always. There cannot be any special case lurking around.