prolog unary numbers - evaluating expression

Question

I am trying to understand Prolog and I came up to following situation. I have defined natural numbers (unary) in following way:

n(0).
n(s(X)) :- nat(X).

Which means that 0 is 0, s(0) is 1, s(s(0)) is 2 etc...

Then I defined predicate add:

add(0, Y, Y) :- nat(Y).
add(s(X), Y, s(Z)) :-
   add(X, Y, Z).

Which adds two unary numbers and result stores to Z.

Now I have following predicate "test" what demonstrates my problem:

test(s(0),0).

Then in interpret I type:

add(s(0),0,R). %result: R = s(0), which is correct

Then i try:

test(add(s(0),0,R), 0).

So the first argument should result in R = s(0), second argument is zero, so the whole expression should be evaluated as true, but prolog says false. I guess that it has something to do with the point, that the add(s(0),0,R) inside the "test" predicate does not evaluate the way I think. Could anyone please explain this to me or eventually provide some link that describes this behaviour? Thanks for any help! Cheers.

Answer 1

No, prolog does not work the way you assume it to. When you ask

?- test(add(s(0),0,R), 0).

prolog tries to find a matching clause. However, there is no matching clause in your database, since s(0) does not match add(s(0),0,R). Two structures can only match if the have the same functor.

s(0) has the functor s while add(s(0),0,R) has the functor add.