Declarative interpretation of list concatenation program in Prolog

Question

I have this very simple problem: write a Prolog program that implement the append Prolog function, that concatenate two strings and that work in the following way:

1. append([a,b],[c,d],X). ---> X = [a,b,c,d]
2. append([a,b],X,[a,b,c,d]). ---> X = [c,d]
3. append([a,b],[X,d],[a,b,c,d]). ---> X=c
4. append(X,Y,[a,b,c,d]). ---> X=[] and Y=[a,b,c,d)

So I have the following two solutions and I am not so sure if my declarative interpretation is correct:

1) SOLUTION 1:

myappend1([],L,L).

myappend1([X|L1],L2,[X|L3]) :- myappend1(L1,L2,L3).

I think that I can read it in a declarative way as following:

The fact say that: if the first list (L1) is empty and the second list (L2) is not empty then it is TRUE that the concatenation of L1*L2 is L2

If the fact it is not true it means that the first list is not empty and so the concatenation of the first list and the second list it is not true that is the second list

So, let me call the first list L1, the second list L2 and the third list L3 then the rule responds TRUE if L3 is the concatenation of L1 and L2, false otherwise

I think that the declarative meaning of this rule is that: the head of the rule is true if the body of the rule is true.

• In the head extract the first X element from the L1 list and from L3 list (and try to unify, if it matching go ahead, otherwise it means that the third list it is not the concatenation for the first and the second list)
• In the body call the function on the first list without X element, the second list and the L3 list (that represent the concatenation)

When it reach the base case in which I have the demonstrated fact myappend1([],L,L). that is true, the program do backtracking at the previous past and because the X element of the first list unified with the X element of the third list it can do that also this computational pass it is TRUE and go back until reach the first assertion

Is this a correct declarative interpretation?

2) SECOND SOLUTION:

myappend2([],L,L).

myappend2(L1,L2,L3) :-  L1=[X|T],               % Dimostra questo predicato AND
                    L3=[X|L4],      % Dimostra questo predicato AND
            myappend2(T,L2,L4).     % Dimostra questa funzione

As in the previous solution the fact simply say that: if the first list (L1) is empty and the second list (L2) is not empty then it is TRUE that the concatenation of L1*L2 is L2

If the fact it is not true it means that the first list is not empty and so the concatenation of the first list and the second list it is not true that is the second list

If the fact it is not true Prolog call the rule and this rule means that: the head of the rule is true if the body of the rule is true.

In this case I can read it in this way:

The concatenation of L1 and L2 is L3 is TRUE if it is true that:

• The current first X element of L1 unifies with the current first element of concatenation list and myappend2 called on the first sublist, L2 and the third sublist it is true

Is it correct?

for me it is so difficult reasoning in declarative way :-(

Answer 1

Like last time, you're adding restrictions that aren't present in the code. Don't feel bad about it, Prolog is very different and it will take time to get used to it.

Let's start.

append([], L, L).

You said:

If the first list (L1) is empty and the second list (L2) is not empty then it is TRUE that the concatenation of L1*L2 is L2

In fact this rule says nothing about whether L2 is empty--or even a list!--or not. It simply says that the empty list appended to something else is that something else. Observe:

?- append([], foo, X).
X = foo.

The declarative reading here is "the empty list appended to L is L."

If the fact it is not true it means that the first list is not empty and so the concatenation of the first list and the second list it is not true that is the second list

Yes, this is correct, but Prolog isn't probing that deeply into the body. It just says "the first list is not empty, so this rule does not match; moving on."

The next rule:

myappend1([X|L1], L2, [X|L3]) :- myappend1(L1,L2,L3).

Your commentary seems excessively complex to me. I would say that this rule says: "myappend1 of the list [X followed by L1] to L2 is the list [X followed by L3], if myappend1 of the list L1 to L2 is L3." The consequences of this reading, however, are exactly as you describe.

Your understanding of what is happening in the first version is, therefore, correct.

The second solution is, mechanically, exactly the same as the first solution. The only difference is that we have moved the unification from the head of the clause into the body. This version is, to my eyes, clearly inferior, because all it has done is create extra work for the reader.

I think the problem you're having, so far, is that your declarative reasoning is intimately tied up with Prolog's engine of computation. A purer declarative reading like the ones I have supplied are simpler and look more like what the Prolog is saying (and have less to do with how it is evaluated).

It will take practice for you to separate these notions, but I think it will help you get better (clearly it's something you're concerned about). In the meantime there's nothing wrong with coming here and asking for help like you've been doing when you get confused. :)

Let me know if I can help more!

Answer 2

When you try to figure out the declarative meaning of a predicate, you are asking: For which solutions does this predicate hold?

Prolog's¹ clauses contribute to the set of solutions independently. So making any connections between the clauses needs some extra scrutiny. It is very easy to make some assumptions that are not the case:

myappend1([],L,L). If the fact it is not true it means that the first list is not empty and so ...

Consider a goal, myappend1([],[],[a]). The fact does not apply, still the first list is empty. Here, you are attempting to operationalize the meaning of the clause. It is very tempting to do this since the largest part of programming languages can only be understood by imagining how something happens step-by-step. The difficulty in Prolog lies in trying to ignore such details, without entirely ignoring procedural aspects.

myappend1([X|L1],L2,[X|L3]) :- myappend1(L1,L2,L3).

To read rules, in particular recursive rules, it is helpful to look at the :- which is a 1970s rendering of ← . So it is an arrow, but it goes from right-to-left. Therefore, you can read this rules as follows, starting with the right-hand-side:

Provided that myappend(L1,L2,L3) holds, _{now cross the :- over to the left side} also myappend([X|L1],L2,[X|L3]) holds.

Sometimes, an even better way to read such a rule is to cover the head completely and ask

??? :- myappend1(L1,L2,L3).

Assume, I know some L1, L2, L3 that hold for myappend1(L1,L2,L3). what can I conclude out of this? Is there anything interesting? Is there anything related I can construct easily out of those 3 values?

This is something which is in the beginning a bit revolting, because you might say: But how do I know that such exists? Well, you don't. You are only assuming it exists. If it will never exist, then you will never be able to make that conclusion.

Many try to read the rules left-to-right, but while Prolog is actually executing them left-to-right, the meaning they cover is easier to understand going in the direction of the conclusion. When Prolog executes a rule left-to-right it does not know if this will work out or not. So the execution might be of entirely speculative nature. Think of append(L1,[z],[a,b,c,d,e]). Here, Prolog will apply this rule for each element of the list. But all such application is in vain. That is, ultimately it will fail.

---

Fine print

1 Actually, the pure, monotonic subset of Prolog.