Search code examples
prologfailure-slice

Prolog - Infinite loop with very basic rule definition

I was trying to practice Prolog, as suggested by my TA, I am trying to create the rule append3(A,B,C,D) which means D is the result of the append of A,B and C.

The definition of append(A,B,C) is given

append([],B,B).
append([X|A],B,[X|C]):-append(A,B,C).

So I simply wrote following, which makes sense to me, as the rule for append3

append3(A,B,C,D) :- append(A,B,X),append(X,C,D).

After, I tried some query, such as append3(A,B,C,[1,2,3]). Everything was fine in the beginning, it was giving me the right results. However, at one moment, I pressed ;, it went into an infinite loop trying to search another answer.

enter image description here

I am not really sure why this happens? I suppose that append3(A,B,C,D) is a very basic rule to define. Is there anything that I am missing or that I didn't consider?

How can I fix this problem?

Solution

  • Prolog's execution mechanism is pretty complex compared to command oriented programming languages a.k.a. imperative languages (short form: imps). Your TA has given you an excellent example where you can improve your mastery of Prolog.

    First of all, you need to understand the termination behavior of append/3. The best way is via a which helps you focus on the part that is relevant to termination. In this case it is:

    append([],B,B) :- false.
append([X|A],B,[X|C]):-append(A,B,C), false.

    This fragment or failure slice now terminates exactly in all cases where your original definition terminates! And since it is shorter, it makes understanding of termination a bit easier. Of course, this new program will no longer find answers like for append([a],[b],[a,b]) — it will fail in stead. But for termination alone it's perfect.

    Now let's go through the arguments one by one:

    1. argument needs to have a non-empty list element and will fail (and terminate) should the argument be [] or any other term. Non-termination may only occur with a partial list (that's a list with a variable instead of [] at the end like [a,b|L]) or just a variable.

    2. argument is just the variable B. There is no way how this B might be different to any term. Thus, B has no influence on termination at all. It is termination neutral.

    3. argument is essentially the same as the first argument. In fact, those arguments look quite symmetrical although they describe different things.

    To summarize, if the first or the last argument is a (fully instantiated) list, append/3 will terminate.

    Note that I just said if and not iff. After all, the first and third argument are a bit connected to each other via the variable X. Let's ignore that for this analysis.

    Now, to a failure slice of your definition.

    append3(A,B,C,D) :- append(A,B,X), false, append(X,C,D).

    Note that D does no longer occur in the visible part! Therefore, the fourth argument has no influence on termination of this fragment. And since X occurs for the first time, only A has an influence on its termination. Therefore, if A is just a variable (or a partial list), the program will not terminate! No need to look any further. No need to look at screens full of traces.

    To fix this for a query like your query append3(A,B,C,[1,2,3])., D has to influence the first goal somewhat.

    One possible fix suggested by another answer would be to exchange the goals:

    append3(A,B,C,D) :- append(X,C,D), false, append(A,B,X).

    Let's look at the variables of append(X,C,D)! C is termination neutral, X occurs for the first time and thus has no influence on termination at all. Only D may make this goal terminate. And thus queries like append3([1],[2],[3], D) will now loop! What a bargain, exchanging non-termination in one case for another!

    To make your program work for both cases, the first goal of append/3 must contain both D and at least one of A, B or C. Try to find it yourself! Here is the spoiler:

    append3(A, B, C, D) :- append(A, BC, D), append(B, C, BC).

    Now the first goal terminates if either A or D is a (fully instantiated) list. The second goal requires either B or BC to be a list. And BC comes from the first goal, which is a list if D is one.

    Thus append3(A, B, C, D) terminates_if b(A), b(B) ; (D).

    See another answer for more on termination, failure slices, and a technique I have not mentioned here, which is termination inference.

    And, note that there are still more cases where the definitions terminate, although they are rather obscure like append([a|_],_,[b|_]) or append3([a|_],_,_,[b|_])) which both fail (and thus terminate) although they only have partial lists. Because of this it's terminates_if and not terminates_iff.