Why do circular references and recursion make my program fail?

Question

I wrote this simple Prolog program.

man(socrates).
mortal(X) :- man(X).
immortal(X) :- immortal(X).

I asked it the usual questions, such as whether Socrates is a man or if Socrates is a mortal.

?- man(socrates).
true.                    //we know for a fact that Socrates is a man
?- mortal(socrates).
true.                    //and it can logically be inferred that Socrates is mortal
?- immortal(socrates).
                         //but we can't seem to figure out if he's immortal

It crashed because of the recursive definition of immortal. Circular references also make it crash or error with Out of stack space.

It seems to me that, at least in this case, it would be fairly trivial for Mr. Prolog to conclude that from the rules in the program, it cannot be inferred that Socrates is immortal. How? I imagine it could examine the stack and see if it is traversing a rule that has already been traversed.

Is there a reason why this isn't already implemented? Would there be some problem with doing so that I am overlooking, or are there implementations of Prolog that already perform such analysis?

Answer 1

It seems to me that, at least in this case, it would be fairly trivial for Mr. Prolog to conclude that from the rules in the program, it cannot be inferred that Socrates is immortal.

Prolog uses an incomplete inference algorithm for efficiency. It's meant to be a programming language where programs have a logical meaning in addition to a procedural one, not a full-blown theorem prover. You have to be careful with the order in which you write the clauses, prevent circular definitions, etc.

As for the logical meaning of your predicate immortal, it's

immortal(X) -> immortal(X)

which is a tautology and can be removed from your program/theory without changing its logical meaning. This means you should remove it if that helps to improve the procedural meaning (gets rid of an infinite loop).

Answer 2

Using tabling with XSB:

:- table foo/1.

foo(X) :- foo(X).

bar(X) :- bar(X).

and then:

| ?- [tabled].
[tabled loaded]

yes
| ?- foo(1).

no
| ?- bar(1).    % does not finish