Convert peano s (N) to integer in Prolog

Question

I came across this natural estimate of the number of logical numbers in a textbook, and this gave me some headache:

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

The rule roughly states that: if N is 0 , it is natural if we do not try to send the contents of s/1 back recursively to the rule until the content is 0 , then this is a natural number if not, then this is not so.

So, I tested the above logical implementation, I thought to myself, it works well if I want to represent s(0) as 1 and s(s(0)) as 2 , but I would like to be able to convert s(0) to 1 .

I was thinking of a basic rule:

 sToInt(0,0). %sToInt(X,Y) Where X=s(N) and Y=integer of X 

So here is my question . How to convert s (0) to 1 and s (s (0)) to 2?

Was answered

Edit: I changed the basic rule in the implementation, which the answer I accepted pointed me to:

 decode(0,0). %was orignally decode(z,0). decode(s(N),D):- decode(N,E), D is E +1. encode(0,0). %was orignally encode(0,z). encode(D,s(N)):- D > 0, E is D-1, encode(E,N). 

So, now I can use it as I wanted, thanks to everyone!

Answer 1

This is a standard task - the solution is here: http://www.docstoc.com/docs/82593705/Prolog-%E2%80%93-Family-Tree (p. 109).

The key concept is that the value of s(N) is 1+ to the value of N , and if N is 0, the value is 0 .

Answer 2

Here is another solution that works both ways using library(clpfd) SWI, YAP or SICStus

 :- use_module(library(clpfd)). natsx_int(0, 0). natsx_int(s(N), I1) :- I1 #> 0, I2 #= I1 - 1, natsx_int(N, I2). 

Answer 3

No problem with meta-predicate nest_right/4 in tandem with Prolog lambdas !

 :- use_module(library(lambda)). :- use_module(library(clpfd)). :- meta_predicate nest_right(2,?,?,?). nest_right(P_2,N,X0,X) :- zcompare(Op,N,0), ord_nest_right_(Op,P_2,N,X0,X). :- meta_predicate ord_nest_right_(?,2,?,?,?). ord_nest_right_(=,_,_,X,X). ord_nest_right_(>,P_2,N,X0,X2) :- N0 #= N-1, call(P_2,X1,X2), nest_right(P_2,N0,X0,X1). 

Request examples:

 ?- nest_right(\X^s(X)^true,3,0,N). N = s(s(s(0))). % succeeds deterministically ?- nest_right(\X^s(X)^true,N,0,s(s(0))). N = 2 ; % succeeds, but leaves behind choicepoint false. % terminates universally