Prolog: check transitivity for simple facts

2019-05-31 01:53发布

问题:

My intention was to implement a simple example (just for myself) of transitivity in Prolog.

These are my facts:

trust_direct(p1, p2).
trust_direct(p1, p3).
trust_direct(p2, p4).
trust_direct(p2, p5).
trust_direct(p5, p6).
trust_direct(p6, p7).
trust_direct(p7, p8).
trust_direct(p100, p200).

I've written this predicate to check whether A trusts C, which is true whenever there is a B that trusts C and A trusts this B:

trusts(A, B) :-
    trust_direct(A, B).

trusts(A, C) :-
    trusts(A, B),
    trusts(B, C).

The predicate returns true for trusts(p1, p2) or trusts(p1, p5) for example, but trusts(p5, p6) already returns ERROR: Out of local stack.

Is Prolog flooding the stack this quickly?

Or is my idea/implementation of trusts bad / wasting system memory?

回答1:

Yes, Prolog is flooding the local stack this quickly.

To see this, it suffices to only consider the following program fragment:

trusts(A, C) :-
        trusts(A, B),
        false,
        trusts(B, C).

This is called a failure-slice: I have inserted false/0, so that everything after false/0 can be ignored. I indicate parts that can be ignored with strikeout text.

This means that the snippet is actually equivalent to:

trusts(A, C) :-
        trusts(A, B),
        false.

Now, with either of the above snippets, we immediately get:

?- trusts(p5, p6).
ERROR: Out of local stack

To get rid of this problem, you have to change the remaining fragment. For this reason, such a fragment serves as an explanation of the problem.

For example, consider the following version:

trusts(A, B) :-
        trust_direct(A, B).
trusts(A, C) :-
        trust_direct(A, B),
        trusts(B, C).

Sample query:

?- trusts(p5, p6).
true ;
false.

This now works as expected. It is declaratively equivalent to the version you posted, and has much better termination properties:

?- trusts(X, Y), false.
false.

This shows that the program now terminates universally.

Alternative solutions are:

  • use your Prolog system's tabling facilities
  • use the definition of transitive closure
  • etc.