Yuval Simon
Yuval Simon

Reputation: 335

No termination of predicate

I have some program about a graph with black and white vertices:

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

vertex(X) :- edge(X,_).
vertex(X) :- edge(_,X).

white(X) :-
   vertex(X),
   not(black(X)).

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

when I run the goal foo(X) I get a problem: If I remove the fact edge(root,root) the program find some solutions (6 different solutions). Otherwise, I get infinite solutions and all are X=root. Why does this happen?

Upvotes: 2

Views: 172

Answers (1)

false
false

Reputation: 10102

First a quick answer which shows you a bit how a Prolog programmer looks at your program, the explanation to it is below. Your program does not terminate, because the following failure-slice does not terminate:

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) :- X = root, Y = root,
   edge(X,Y),
   black(Y),
   foo(Y), false.

All through-striken text is irrelevant to understand non-termination. As you can see the remainder is relatively short and thus fast to grasp.

Prolog is not able to detect this loop directly. However, you can use closure0/3 defined here for this purpose:

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

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

Now for the details.

Before answering your question why this happens, let's take a step back. We need first to find a good way to observe the problem. The goal foo(X) does produce answers, actually only X = root. So maybe you are just impatient waiting Prolog to finish? By asking the query foo(X), false instead, we get rid of these irritating, eye-straining answers, and we will just wait to get false as an answer back.

Still we cannot be sure about the non-termination property of the program. But we can narrow down the actual reason by inserting goals false (and also (=)/2). In the above failure-slice I have inserted the maximum. If you are just starting, simply add one false and then reload the program and retry the query. With some experience you will soon be able to identify such parts rapidly. So now we only have to understand

foo(root) :-
   edge(root,root), % always true
   black(root),     % always true
   foo(root), false.

or even shorter

foo(root) :-
   foo(root).

Prolog's very simple but efficient execution mechanism does not detect such loops. There are essentially several ways out:

  1. add loop detection manually. This is typically very prone to errors

  2. use closure0/3 - see above

  3. write your own meta-interpreter to detect loops in general

  4. use a language extension like tabling, offered in B-Prolog or XSB-Prolog.

Upvotes: 4

Related Questions