Create successor numbers from natural numbers

Question

I want to create successor Numbers from natural numbers in Prolog.

nat2s(0, s(0)).
nat2s(NaturalNumber, SNumber) :-
            N is NaturalNumber - 1,
            nat2s(N, s(SNumber)).

The output should be like this:

nat2s(3, X).
X = s(s(s(0))).

Actually it's an infinitive loop. I don't how to end the loop without only getting true as result.

Answer 1

I suggest a slightly different approach, namely the use of library(clpfd). First let's pick a more declarative name for the predicate. Since in your post the natural number and the number in s(X)-notation are the first and second argument respectively, let's call it nat_sx/2. Then the predicate can be defined like so:

:- use_module(library(clpfd)).

nat_sx(0,0).
nat_sx(N,s(X)) :-
   N #> 0,
   N0 #= N-1,
   nat_sx(N0,X).

This yields the desired result in your post:

   ?- nat_sx(3,X).
X = s(s(s(0))) ? ;
no

To see why the use of clpfd is beneficial let's incorporate the suggested corrections from the comments into your code and compare both versions.

nat2s(0, 0).
nat2s(NaturalNumber, s(SNumber)) :-
   NaturalNumber > 0,
   N is NaturalNumber - 1,
   nat2s(N, SNumber).

The above query works with this version as well:

   ?- nat2s(3,S).
S = s(s(s(0))) ? ;
no

However, it would be nice to be able to use the predicate in the other direction as well. So let's ask which natural number corresponds to s(s(0)):

   ?- nat_sx(N,s(s(0))).
N = 2 ? ;
no
   ?- nat2s(N,s(s(0))).
     ERROR at  clause 2 of user:nat2s/2 !!
     INSTANTIATION ERROR- =:=/2: expected bound value

The reason for the instantiation error is the fact that is/2 expects a variable-free expression on the right side:

   ?- X is 3-1.
X = 2
   ?- 2 is X-1.
     ERROR!!
     INSTANTIATION ERROR- in arithmetic: expected bound value
   ?- 2 is 3-X.
     ERROR!!
     INSTANTIATION ERROR- in arithmetic: expected bound value

This is also the reason why the most general query of nat2s/2 has an instantiation error after the first solution...

   ?- nat2s(N,S).
N = S = 0 ? ;
     ERROR at  clause 2 of user:nat2s/2 !!
     INSTANTIATION ERROR- =:=/2: expected bound value

... while nat_sx/2 keeps generating solutions:

   ?- nat_sx(N,S).
N = S = 0 ? ;
N = 1,
S = s(0) ? ;
N = 2,
S = s(s(0)) ? ;
...