Search code examples
prologsuccessor-arithmetics

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

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.

Solution

  • 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.