Unnecessary predicate definition for simple transitivity checkup?

For the given 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).

This solution:

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

...was given to improve my stack overflow issue described in Prolog: check transitivity for simple facts.

The solution itself works like a charm. However, I am confused by the doubled trust_direct(A, B). Why is this necessary?

Shouldn't the trusts(A, C) predicate already cover the trust_direct(A, B) relationship?

Solution

That's a great question!

To show the reason for this, I use the following definition to enable declarative debugging:

:- op(950,fy, *).

*_.

I can now put * in front of any goal to generalize it away. Declaratively, this means that I can simply ignore the goal (recall that a goal is always a constraint, restricting any solution). I could of course also simply comment goals away, but that does not work nicely for the last goal of a clause body.

Now consider your definition:

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

Now, to answer your very legitimate question, suppose we only had the second clause, i.e.:

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

To make our life simpler, I now generalize this definition as follows:

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

This is more general than the immediately preceding snippet: If trusts(X, Y) holds for any X and Y with the preceding snippet, then trusts(X, Y) also holds with this definition.

I have used ~~strikeout~~ text to indicate goals that are not relevant (because they are generalized away). So, this is declaratively equivalent to:

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

Let us read this declaratively:

trusts(A, C) holds if trusts(B, C) holds.

But when does trusts(B, C) hold? Of course (by simply applying the definition again), if trusts(B', C') holds. And when does this hold? Of course (by simply applying the definition), if ... etc. From here, it is easy to see that we will never find any A and C so that trusts(A, C) holds at all.

And that despite the fact that this is actually the significantly more general version of the original clause! Thus, there is not the slightest hope to satisfy the more specific version!

This answers our question: We need a case that actually holds, and what could be simpler than talking about trust_direct/2, which is really the simplest case in which we definitely expect the more general relation trusts/2 to hold too.

It is thus very natural to start with this case, and say:

If trust_direct(X, Y) holds then trusts(X, Y) holds.

In Prolog:

trusts(X, Y) :- trust_direct(X, Y).

And that's exactly your first clause!