prologpredicatefailure-slicetransitive-closuretransitivity

Prolog: check transitivity for simple facts

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?

Solution

  • 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 : 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: