Преобразовать число Пеано s(N) в целое число в прологе

Question

Я наткнулся на эту оценку натуральных чисел логических чисел в учебнике, и это доставляло мне некоторую головную боль:

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

Правило примерно гласит, что: если N является 0 это естественно, если мы не пытаемся отправить содержимое s/1 вернуться к правилу до тех пор, пока содержимое 0, то это натуральное число, если нет, то это не так.

Итак, я проверил приведенную выше логику реализации, подумал про себя, ну, это работает, если я хочу представлять s(0) как 1 а также s(s(0)) как 2, но я хотел бы иметь возможность конвертировать s(0) в 1 вместо.

Я подумал о базовом правиле:

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

Итак, вот мой вопрос: как я могу преобразовать s(0) в 1 и s(s(0)) в 2?

Был дан ответ

Редактировать: я изменил базовое правило в реализации, на которое указывал ответ, который я принял:

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

Так что теперь я могу использовать его, как я хотел, спасибо всем!

Answer 1

Это стандартная задача - решение здесь: http://www.docstoc.com/docs/82593705/Prolog-%E2%80%93-Family-Tree (стр. 109).

Ключевым моментом является то, что ценность s(N) 1+ значение Nи что если N 0, значение 0,

Answer 2

Вот еще одно решение, которое работает "в обе стороны", используя library(clpfd) SWI, YAP или 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

Нет проблем с мета-предикатом nest_right/4 в тандеме с прологом лямбда!

:- 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).

Примеры запросов:

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

Answer 4

Без использования clp и использования хвостовой рекурсии (для производительности):

      peano_int(P, I) :-
    (   integer(I)
    ->  I @>= 0
    ;   var(I)
    ),
    peano_int_(P, 0, I).

peano_int_(P, U, I) :-
    (   U == I
    ->  ! 
    ;   P == I
    ->  !,
        % Can only happen with P & U both 0
        U == 0
    ;   I = U
    ),
    % After cuts have been performed
    P = 0.
peano_int_(s(P), U, I) :-
    U1 is U + 1,
    peano_int_(P, U1, I).

Детерминирован во всех отношениях:

      ?- peano_int(P, 3).
P = s(s(s(0))).

?- peano_int(s(s(s(0))), I).
I = 3.

?- peano_int(s(s(0)), 2).
true.

?- peano_int(P, I).
P = I, I = 0 ;
P = s(0),
I = 1 ;
P = s(s(0)),
I = 2 ;

?- peano_int(P, P).
P = 0.

% Safeguards
?- peano_int(s(P), P).
false.

?- dif(P, s(0)), peano_int(P, 1).
false.

% Fast tail-end recursion, when converting to integer
?- time(peano_int(P, 1_000_000)).
% 1,000,003 inferences, 0.084 CPU in 0.084 seconds (100% CPU, 23830428 Lips)
P = s(s(s(...

Answer 5

Вот мой:

Числа Пеано, которые на самом деле лучше адаптированы для Prolog, в виде списков.

Почему списки?

• Существует изоморфизм между
  • список длины N, содержащий только s и заканчивая пустой список
  • рекурсивная линейная структура глубины N с функциональными символами sоканчивающийся символом zero
  • ... так что это одно и то же (по крайней мере, в этом контексте).
• Нет особой причины придерживаться того, что математики 19-го века (например, Джузеппе Пеано) считали "хорошей структурной структурой для рассуждений" (рожденной, как мне кажется, из приложения функций).
• Это уже делалось раньше: действительно ли кто-нибудь использует геделизацию для кодирования строк? Нет! Люди используют массивы символов. Представьте себе это.

Поехали, а посередине есть небольшая загадка, которую я не знаю, как решить (может быть, использовать аннотированные переменные?)

% ===
% Something to replace (frankly badly named and ugly) "var(X)" and "nonvar(X)"
% ===

ff(X) :- var(X).     % is X a variable referencing a fresh/unbound/uninstantiated term? (is X a "freshvar"?)
bb(X) :- nonvar(X).  % is X a variable referencing an nonfresh/bound/instantiated term? (is X a "boundvar"?)

% ===
% This works if:
% Xn is boundvar and Xp is freshvar: 
%    Map Xn from the domain of integers >=0 to Xp from the domain of lists-of-only-s.
% Xp is boundvar and Xn is freshvar: 
%    Map from the domain of lists-of-only-s to the domain of integers >=0
% Xp is boundvar and Xp is boundvar: 
%    Make sure the two representations are isomorphic to each other (map either
%    way and fail if the mapping gives something else than passed)
% Xp is freshvar and Xp is freshvar: 
%    WE DON'T HANDLE THAT!
%    If you have a freshvar in one domain and the other (these cannot be the same!)
%    you need to set up a constraint between the freshvars (via coroutining?) so that
%    if any of the variables is bound with a value from its respective domain, the
%    other is bound auotmatically with the corresponding value from ITS domain. How to
%    do that? I did it awkwardly using a lookup structure that is passed as 3rd/4th
%    argument, but that's not a solution I would like to see.
% ===

peanoify(Xn,Xp) :-
   (bb(Xn) -> integer(Xn),Xn>=0 ; true),                  % make sure Xn is a good value if bound
   (bb(Xp) -> is_list(Xp),maplist(==(s),Xp) ; true),      % make sure Xp is a good value if bound 
   ((ff(Xn),ff(Xp)) -> throw("Not implemented!") ; true), % TODO
   length(Xp,Xn),maplist(=(s),Xp).

% ===
% Testing is rewarding! 
% Run with: ?- rt(_).
% ===

:- begin_tests(peano).

test(left0,true(Xp=[]))          :- peanoify(0,Xp).
test(right0,true(Xn=0))          :- peanoify(Xn,[]).
test(left1,true(Xp=[s]))         :- peanoify(1,Xp).
test(right1,true(Xn=1))          :- peanoify(Xn,[s]).
test(left2,true(Xp=[s,s]))       :- peanoify(2,Xp).
test(right2,true(Xn=2))          :- peanoify(Xn,[s,s]).
test(left3,true(Xp=[s,s,s]))     :- peanoify(3,Xp).
test(right3,true(Xn=3))          :- peanoify(Xn,[s,s,s]).
test(f1,fail)                    :- peanoify(-1,_).
test(f2,fail)                    :- peanoify(_,[k]).
test(f3,fail)                    :- peanoify(a,_).
test(f4,fail)                    :- peanoify(_,a).
test(f5,fail)                    :- peanoify([s],_).
test(f6,fail)                    :- peanoify(_,1).
test(bi0)                        :- peanoify(0,[]).
test(bi1)                        :- peanoify(1,[s]).
test(bi2)                        :- peanoify(2,[s,s]).

:- end_tests(peano).

rt(peano) :- run_tests(peano).