CODEWITHSUNDEEP
prologfailure-slice
איתן לוי
איתן לוי

Reputation: 443

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

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?

Upvotes: 0

Views: 79

Answers (2)

false
false

Reputation: 10142

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.

Upvotes: 1

Scott Hunter
Scott Hunter

Reputation: 49920

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

Upvotes: 0

Related Questions