Рекурсивное сложение в Прологе с числами Пеано не работает

Question

В настоящее время я пытаюсь попрактиковаться в Прологе. Я только начал, и я столкнулся с проблемой, которую я не совсем понимаю. Я хочу рекурсивно определить, является ли одно число Пеано двойным другого. Я пытался решить это так:

isDouble(0, X,X).
isDouble(s(Peano1), Peano1, Peano2) :-
    isDouble(Peano1, s(Peano1), Peano2).

По какой-то причине это не работает. Кто-нибудь знает почему?

Answer 1

Вам не нужно три аргумента, чтобы определить такой предикат. Просто подумайте, какое отношение оно должно описать: отношение между числом и его двойником. Следовательно, вам нужны только два аргумента и два правила, описывающих две возможности. Либо число равно нулю, то его дубль также равен нулю. В противном случае у вас есть разность двух с /2 для двойного в каждой рекурсии, но только одна для числа:

nat_double(0,0).
nat_double(s(X),s(s(Y))) :-
   nat_double(X,Y).

Это дает желаемые результаты:

?- nat_double(X,Y).
X = Y, Y = 0 ;                     % X=0, Y=0
X = s(0),                          % X=1
Y = s(s(0)) ;                      % Y=2
X = s(s(0)),                       % X=2
Y = s(s(s(s(0)))) ;                % Y=4
X = s(s(s(0))),                    % X=3
Y = s(s(s(s(s(s(0)))))) ;          % Y=6
X = s(s(s(s(0)))),                 % X=4
Y = s(s(s(s(s(s(s(s(0)))))))) ;    % Y=8
.
.
.

Или, если вы хотите проверить пару, как предложено в комментариях:

?- nat_double(s(s(0)),s(s(s(s(0))))).
true.

РЕДАКТИРОВАТЬ:

Если вы настаиваете на интерфейсе isDouble/3, как подсказывает ваш комментарий, то вы можете определить его как предикат вызова для nat_double/2 следующим образом:

isDouble(X,X,Y) :-
   nat_double(X,Y).

Это дает желаемый результат для вашего примера:

?- isDouble(s(s(0)),s(s(0)),s(s(s(s(0))))).
true.