Reasoning through a program in Prolog

Question

I am attempting a past paper question for a Prolog exam. I drew a 'tree' for how I believed Prolog ought to behave given the program and a certain goal. However, Prolog does not behave as I expected, and given a query for which I believed it would return 'true', it actually returned 'false'.

Here is my program:

sum(Term,N) :- Term = 0, N = 0.
sum(Term,N) :- Term = f(M,Subterm), number(M), sum(Subterm,N-M).

My query and search tree are as follows (goals are bracketed and in bold):

[ sum(f(1,0),1) ]

Using Rule 1, let Term = 0, N = 0, tries to unify [ 1 = 0, 1 = 0 ] fail.

Redo: using Rule 2, let Term = f(1,0), N=1 [ f(1,0) = f(M,Subterm), number(M), sum(Subterm,1-1) ]

Unifying, let M=1 and Subterm=0 [ number(1), sum(0,0) ]

Using Rule 1, this should succeed. However (SWI) Prolog says 'false'.

If someone can point out to me why my reasoning is flawed (and how I can learn from this in future), I would be very grateful.

Answer 1

Since your program is almost a pure¹ one, you can locate the error in a systematic manner without using a debugger. The idea is to generalize your program by removing goals, one-by-one. I came up with the following pure generalization which I obtained by "commenting" out some goals like so:

:- op(950, fy, *).
*(_).

sum(Term,N) :-
   Term = 0,
   N = 0.
sum(Term,N) :-
   * Term = f(M,Subterm),
   * number(M),
   sum(Subterm,N-M).

?- sum(Term, N).
   Term = 0, N = 0
;  false.

Also the query above is more general than yours. This is a very useful technique in Prolog: Instead of thinking about concrete solutions, we first let Prolog do all the work for us.

The answer was quite clear: There is exactly one solution to this relation, even if the relation is now generalized.

So the problem must be somewhere in the remaining visible part. Actually, it's the -. Why not write instead:

:- use_module(library(clpfd)).

sum(0, 0).
sum(Term, N0) :-
   Term = f(M, Subterm),
   N0 #= M+N1,
   sum(Subterm, N1).

I find that program much easier to understand. If I read a name sum, I immediately look for a corresponding +. Of course, if you insist, you could write N0-M #= N1 instead. It would be exactly the same, except that this requires a bit more thinking.

---

_{Fine print you don't need to read}

1) Your original program used number/1 which is not pure. But since the problem persisted by removing it, it did not harm our reasoning.

Answer 2

To be more accurate, the first rule tries to unify f(1,0) = 0 and 1 = 0, which of course fails.

Analysis of rule 2 is also incorrect. Partly, it's because Prolog does not evaluate arithmetic expressions inline. The term N-M is just a term (short-hand for '-'(N, M). It does not result in M being subtracted from M unless the evaluation is done explicitly via is/2 or an arithmetic comparison (e.g., =:=/2, =</2, etc).

The analysis of rule 2 would go as follows. Step 5 is where your logic breaks down due to the above.

1. Call sum(f(1,0), 1) results in Term = f(1,0) and N = 1.
2. In rule 2, Term = f(M, Subterm) becomes f(1,0) = f(M, Subterm) which results in M = 1 and Subterm = 0.
3. number(N) becomes number(1) and succeeds (since 1 is a number)
4. The call sum(Subterm, N-M) becomes sum(0, 1-1).
5. Prolog matches sum(0, 1-1) with the head of rule 1 sum(Term, N) :- Term = 0, N = 0., but it fails because 1-1 = 0 (which is the same as '-'(1, 1) = 0 unification fails.
6. Prolog matches sum(0, 1-1) with the head of rule 2, and unifies Term = 0 and N = 1-1 (or N = '-'(1, 1)).
7. Term = f(M, Subterm) becomes 0 = f(M, Subterm) which fails because 0 cannot match the term f(M, Subterm).
8. No more rules to attempt, so the predicate call fails.

The easy fix here is a common, basic Prolog pattern to use a new variable to evaluate the expression explicitly:

sum(Term,N) :-
    Term = f(M,Subterm),
    number(M),
    R is N - M,
    sum(Subterm, R).

You can also tidy up the code quite a bit by unifying in the heads of the clauses. So the clauses could be rewritten:

sum(0, 0).
sum(f(M, Subterm), N) :-
    number(N),
    R is N - M,
    sum(Subterm, R).

---

EDIT