prologsuccessor-arithmetics

Sum of a list in prolog

I'm reading 'the art of prolog' book and I found an exercise that reads 'Define the relation sum(ListOfIntegers,Sum) which holds if Sum is the sum of the ListOfIntegers, without using any auxiliary predicate' .I came up with this solution:

sum([],Sum).
sum([0|Xs], Sum):-sum(Xs, Sum).
sum([s(X)|Xs], Sum):-sum([X|Xs],s(Sum)).

Which does not work exactly as I would want it to.

?- sum([s(s(0)),s(0),s(s(s(0)))],X).
true ;
false.

I was expecting X to be

s(s(s(s(s(s(0))))))

I thought that the problem is that I have to 'initialize' Sum to 0 in the first 'iteration' but that would be very procedural and unfortunately I'm not quite apt in prolog to make that work. Any ideas or suggestions?

Solution

  • The best way to localize the problem is to first simplify your query:

    ?- sum([0],S).
   true.
?- sum([],S).
   true.

    Even for those, you get as an answer that any S will do. Like

    ?- sum([],s(s(0))).
   true.

    Since [] can only be handled by your fact, an error must lie in that very fact. You stated:

    sum([], Sum).

    Which means that the sum of [] is just anything. You probably meant 0.

    Another error hides in the last rule... After fixing the first error, we get

    ?- sum([0],Sum).
   Sum = 0.
?- sum([s(0)],Sum).
   false.

    Here, the last clause is responsible. It reads:

    sum([s(X)|Xs], Sum):-sum([X|Xs],s(Sum)).

    Recursive rules are relatively tricky to read in Prolog. The simplest way to understand them is to look at the :- and realize that this should be an arrow ← (thus a right-to-left arrow) meaning:

    provided, that the goals on the right-hand side are true
    we conclude what is found on the left-hand side

    So, compared to informal writing, the arrows points into the opposite direction!

    For our query, we can consider the following instantiation substituting Xs with [] and X with 0.

    sum([s(0)| [] ], Sum) :- sum([0| []],s(Sum)).

    So this rule now reads right-to-left: Provided, sum([0],s(Sum)) is true, ... However, we do know that only sum([0],0) holds, but not that goal. Therefore, this rule never applies! What you intended was rather the opposite:

    sum([s(X)|Xs], s(Sum)):-sum([X|Xs],Sum).