CODEWITHSUNDEEP
debuggingprolog
IIM
IIM

Reputation: 533

Reasoning through a program in Prolog

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.

Upvotes: 2

Views: 162

Answers (2)

false
false

Reputation: 10102

Since your program is almost a pure1 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.

Upvotes: 4

lurker
lurker

Reputation: 58224

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: My answer is intended to guide you through a walk through of your existing logic. Other than correcting the misunderstanding regarding expression evaluation, I did not analyze your solution for overall correctness.

Upvotes: 0

Related Questions