3

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?

Peter Olson
  • 139,199
  • 49
  • 202
  • 242

4 Answers4

6

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

Fred Foo
  • 355,277
  • 75
  • 744
  • 836
3

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
salva
  • 9,943
  • 4
  • 29
  • 57
2

Your definitions - and how you interpret them:

man(socrates).

Socrates is a man.

mortal(X) :- man(X).

Every man is a mortal.

immortal(X) :- immortal(X).

Every immortal is immortal.


Your definitions - and how Prolog interprets them:

man(socrates).

If you ask about the manhood of Socrates, I know it's true.

mortal(X) :- man(X).

If you ask me about the mortality of someone, I'll check his manhood (and if that's true, so is the mortality).

immortal(X) :- immortal(X).

If you ask me about the immortality of someone, I'll check his immortality. (Do you still wonder how that leads to an infinite loop?)


If you want to state that someone is immortal if he can't be proven mortal, then you can use:

immortal(X) :- not( mortal(X) ).
ypercubeᵀᴹ
  • 113,259
  • 19
  • 174
  • 235
  • 1
    I understand why it could be an infinite loop, but I assumed that the a logical language would be able to conclude that `immortal` would always be false. For example, suppose there were a "recursion" badge on Stack Overflow, and the only way to get the recursion badge is to get the recursion badge, it would be impossible to obtain. – Peter Olson Nov 13 '11 at 02:55
  • If you want immortal to be always false, you can declare that explicitly `immortal(X) :- False.` or with `immortal(X) :- !.` (I may be wrong on that, many years that I haven't used Prolog). For this simple case, they are equivalent but you could have other, more complex cases, where recursion is very useful (and can be stopped with `!`) – ypercubeᵀᴹ Nov 13 '11 at 03:04
  • 4
    `immortal(X) :- !.` is wrong, it will say that every X is immortal. – Joe Lehmann Nov 13 '11 at 07:03
  • @PeterOlson, **Correction**: If you want immortal to be always false, you can declare that explicitly `immortal(X) :- False.`, meaning every one is not immortal. (**and not with `immortal(X) :- !.`** which, as Joe Lehmann pointed, means the opposite, that **every one is immortal**. – ypercubeᵀᴹ Nov 13 '11 at 15:47
  • @ypercube It would be easier to leave out the `immortal` definition entirely, and it would mean essentially the same thing. – Peter Olson Nov 13 '11 at 16:12
  • 1
    @Peter Olson: It is very different. Calling an undefined predicated on ISO-Prolog does not fail but troughs an error. – salva Nov 13 '11 at 19:19
0

How about this little program:

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

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

Joe Lehmann
  • 1,087
  • 5
  • 10