Convert peano number s(N) to integer in Prolog

问题:

I came across this natural number evaluation of logical numbers in a tutorial and it's been giving me some headache:

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

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

So I tested the above logic implementation, thought to myself, well this works if I want to represent s(0) as 1 and s(s(0)) as 2, but I´d like to be able to convert s(0) to 1 instead.

I´ve thought of the base rule:

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

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

Has been answered

Edit: I modified the base rule in the implementation which the answer I accepted pointed me towards:

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 I can now use it like I wanted to, thanks everyone!

回答1:

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

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

回答2:

Here is another solution that works "both ways" using library(clpfd) of 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).

回答3:

No problemo 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).

Sample queries:

?- 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