CODEWITHSUNDEEP
prologterminatefailure-slicenon-termination
absolutelydevastated
absolutelydevastated

Reputation: 1747

Prolog clause terminates individually, but not together

So

?- canCall(mary, Person).

works and terminates and

?- canFind(mary, Person).

also works and terminates. But somehow 

?- canCall(mary, Person), canFind(mary, Person).

does not terminate. What may be a possible reason?

Upvotes: 2

Views: 191

Answers (2)

false
false

Reputation: 10102

(What you actually meant was: Queries terminate individually, but their conjunction does not terminate, sometimes)

You have discovered here a very fundamental aspect of Prolog's termination properties. Let's see this with the following pure1 program:

canFind(mary, john).

canCall(mary, bob).
canCall(A, B) :-
   canCall(B, A).

?- canCall(mary, Person).
   Person = bob
;  ... .

?- canFind(mary, Person).
   Person = john.

Everything looks fine! Let's check this code in, such that everyone can use it. Now your hapless colleague tries:

?- canCall(mary, Person), canFind(mary, Person).
   loops.

Oh no, this loops! Maybe I just have to reorder the goals:

?- canFind(mary, Person), canCall(mary, Person).
   loops.

Again!

Of course, you are upset too. After all, you diligently tested this code. And it terminated. Or did it?

Two notions of termination

This is one of the most confusing things in Prolog: We have here (at least) two different notions of termination of a query. The one that you tested is (sometimes) called existential termination. However, I rather recommend to call this simply finds an answer. It is extremely brittle as you have experienced.

And if a query not only finds an answer but all of them and finishes the query, then this is called universal termination or simply termination. If Prolog programmers say that a query terminates, they mean that it terminates universally.

So how can we observe universal termination? Simply ask for all answers. In GNU-Prolog you type a. In other systems you will have to hammer SPACE or ;Return until it's finished, or your fatigued eyes or your carpal tunnels stop it.

?- canCall(mary, Person).
   Person = bob
;  Person = bob
;  Person = bob
;  Person = bob
;  Person = bob
;  ... .

So here we see that there are infinitely many answers (actually, we finite beings would have to prove that, but believe me for the moment).

Isn't there a cheaper way to observe this? Without all this walls of text of answers? You can "turn off" the answers by adding a condition that will never hold, false.

So ask instead:

?- canCall(mary, Person), false.

What can be the outcome of such a query? It can never be true. It can only be false, should it terminate. So with this query we simply test the termination property of a program only.

Now, the conjunction of two (universally) terminating queries will always terminate. So this kind of termination is much more robust.

There are many more cool properties of universal termination. For example, you can exchange the order of clauses (that is, facts and rules) as you like: No matter what order they are in, all programs share exactly the same termination property.

Another is that you can easily locate the source of non-termination in your programs with the help of a . Start reading with this one.

In command-oriented programming languages this notion is not readily present. However, with iterators, you have quite similar notions: If the iterator produces the first item, that would correspond to existential termination and if finitely many items are produced, that is, if after finitely many next it's finished, that would correspond to universal termination. Kind of.

1 Actually, in impure programs you have all kinds of nonsensical behavior. So it is pointless to consider them.

Upvotes: 6

whd
whd

Reputation: 1861

I guess, when You run individually, Person unifies to two different values. Check this.

Upvotes: 0

Related Questions