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 him the usual questions, for example, is Socrates a man or if Socrates is 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 immortal 

It crashed due to the recursive definition of immortal . Circular links also crash or fail with Out of stack space.

It seems to me that, at least in this case, Mr. Prolog will be rather trivial to conclude that it is impossible to conclude from the rules in the program that Socrates is immortal. How? I assume that he could check the stack and see if it follows the rule already passed.

Is there a reason this has not yet been implemented? Will there be any problem with what I am losing sight of, or are there any Prolog implementations that are already doing this kind of analysis?

Answer 1

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

Prolog uses an incomplete output algorithm for efficiency. This meant that it was a programming language where programs make logical sense in addition to the procedural, rather than a full-blown theoretical breakthrough. You have to be careful with the order in which you write sentences, prevent circular definitions, etc.

As for the boolean value of your immortal predicate, this

 immortal(X) -> immortal(X) 

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

Answer 2

Using tabs 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 

Answer 3

Your definitions - and how you interpret them:

 man(socrates). 

Socrates is a man.

 mortal(X) :- man(X). 

Everyone is mortal.

 immortal(X) :- immortal(X). 

Every immortal is immortal.

---

Your definitions - and how Prolog interprets them:

 man(socrates). 

If you ask about the masculinity of Socrates, I know that this is true.

 mortal(X) :- man(X). 

If you ask me about someone's mortality, I will check his masculinity (and if so, then mortality).

 immortal(X) :- immortal(X). 

If you ask me about the immortality of someone, I will check his immortality. (Are you still wondering how this leads to an endless loop?)

---

If you want to claim that someone is immortal, if he cannot be proved mortal, you can use:

 immortal(X) :- not( mortal(X) ). 

Answer 4

How about this little program:

  loopy(Y) :- read(X), Z is X+Y, print(Z), nl, loopy(Y). 

Your Mr. Prolog would conclude that loopy (Y) has already been called and will fail.