can any one help me to understand this recursive prolog example?

Question

here is the plus code that i don't understand

plus(0,X,X):-natural_number(X).
plus(s(X),Y,s(Z)) :- plus(X,Y,Z).

while given :

natural_number(0).
natural_number(s(X)) :- natural_number(X).

I don't understand this recursion. If I have plus(s(0),s(s(s(0))),Z) how can i get the answer of 1+3=4?

I need some explanation for the first code. I try that plus(0,X,X) will stop the recursion but I think that I do it wrong.

Answer 1

So, let's start with natural_number(P). Read this as "P is a natural number". We're given natural_number(0)., which tells us that 0 is always a natural number (i.e. there are no conditions that must be met for it to be a fact). natural_number(s(X)) :- natural_number(X). tells us that s(X) is a natural number if X is a natural number. This is the normal inductive definition of natural numbers, but written "backwards" as we read Prolog "Q := P" as "Q is true if P is true".

Now we can look at plus(P, Q, R). Read this as "plus is true if P plus Q equals R". We then look at the cases we're given:

1. plus(0,X,X) :- natural_number(X).. Read as Adding 0 to X results in X if X is a natural number. This is our inductive base case, and is the natural definition of addition.
2. plus(s(X),Y,s(Z)) :- plus(X,Y,Z). Read as "Adding the successor of X to Y results in the successor Z if adding X to Y is Z'. If we change the notation, we can read it algebraically as "X + 1 + Y = Z + 1 if X + Y = Z", which is very natural again.

So, to answer you direct question "If I have plus(s(0),s(s(s(0))),z), how can i get the answer of 1+3=4?", let's consider how we can unify something with z each step of the induction

1. Apply the second definition of plus, as it's the only one that unifies with the query. plus(s(0),s(s(s(0))), s(z')) is true if plus(0, s(s(s(0))), z') is true for some z
2. Now apply the first definition of plus, as it's the only unifying definition: plus(0, s(s(s(0))), z') if z' is s(s(s(0))) and s(s(s(0))) is a natural number.
3. Unwind the definition of natural_number a few times on s(s(s(0))) to see that is true.
4. So the overall statement is true, if s(s(s(0))) is unified with z' and s(z') is unified with z.

So the interpreter returns true, with z' = s(s(s(0))) and z = s(z'), i.e. z = s(s(s(s(0)))). So, z is 4.

Answer 2

That code is a straightforward implementation of addition in Peano arithmetic.

In Peano arithmetic, natural numbers are represented using the constant 0 and the unary function s. So s(0) is a representation of 1, s(s(s(0))) is representation of 3. And plus(s(0),s(s(s(0))),Z) will give you Z = s(s(s(s(0)))), which is a representation of 4.

Answer 3

You won't get numerical terms like 1+3=4, all you get is the term s/1 which can embed itself to any depth and thus can represent any natural number. You can combine such terms (using plus/3) and thereby achieve summing.

Note that your definition of plus/3 has nothing to do with SWI-Prolog's built-in plus/3 (which works with integers and not with the s/1 terms):

?- help(plus).
plus(?Int1, ?Int2, ?Int3)
    True if Int3 = Int1 + Int2.
    At least two of the three arguments must be instantiated to integers.