0
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?

false
  • 10,264
  • 13
  • 101
  • 209
איתן לוי
  • 433
  • 1
  • 3
  • 9
  • 1
    You made an infinte loop, since for `foo(root)`, it can each time also take the recurive case, unify with `edge(root, root)`, and thus find another solution. Prolog searches *depth-first*, not *breadth-first*. – Willem Van Onsem Feb 21 '20 at 16:02

2 Answers2

1

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.

false
  • 10,264
  • 13
  • 101
  • 209
0

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

Scott Hunter
  • 48,888
  • 12
  • 60
  • 101