Prolog: a(b,c) and a(X,Y):-a(Y,X), query a(c,b) returns infinite true?

Question

Here is my knowledge base:

a(b,c). 
a(X,Y):-a(Y,X).

Here is my query: a(c,b).

I am using SWI-Prolog. I thought that this query would lead to the program printing "true". However, instead it prints "true" and continues to print true if I hit the semicolon... until FOREVER.

Why doesn't it stop?

My thoughts: First, X is bound to b and Y is bound to c. Then, Prolog tests a(b,c) and finds that this is true. Therefore, a(c,b) is true as well and SWI-Prolog should print true once. However, since it prints true forever as long as I keep hitting that semicolon, this leads me to think that something recursive is going on. Where is this happening? Help!

EDIT: More specifically my question is why does the program pause after each "true" and wait for me to press the semicolon or another key instead of just being done? If I have two predicates human(socrates) and mortal(X):-humans(X), the response to the query mortal(socrates) will be a single "true". (Sorry if I failed to make this clear above.)

Fred Foo Fred Foo · Accepted Answer · 2012-05-15T21:59:31

Prolog first proves a(c,b) by means of the second rule followed by the first. Then, it proves a(c,b) by means of three invocations of the second rule followed by the first. Then, by five invocations of the second rule, etc. Prolog's inference algorithm is a depth-first search without a closed set, i.e. it doesn't keep track of what it has already proved and happily proves it again.

If you don't want this behavior, you should either rewrite the rules as, e.g.,

a_fact(b, c).
a(X, Y) :- a_fact(X, Y).
a(Y, X) :- a_fact(X, Y).

... or use some kind of tabling execution. I don't think SWI-Prolog supports tabling, though.

Prolog: a(b,c) and a(X,Y):-a(Y,X), query a(c,b) returns infinite true?

1 Answers