Пролог Пеано разность / вычитание чисел

Question

Я пытаюсь вычислить разницу для «чисел Пеано» (Recursive definition of natural numbers represented as s(0), s(s(0)) etc.), но я застрял с одной проблемой.

Определение для вычитания следующее:

s(X) - 0 = s(X)
s(X) - s(s(X)) = 0
s(X) - s(X) = 0
s(s(X)) - s(X) = s(0)
0 - s(X) = 0

Это мой текущий код:

nat(0).
nat(s(X)) :- nat(X).

% sub/3
% Subtracts right operand from left operand and returns difference
sub(0, _, 0).
sub(X, 0, X).
sub(s(X), s(Y), X) :-
  sub(X,Y,X).

Мой мыслительный процесс, стоящий за этим:
Поскольку мне действительно не нужно рекурсивно увеличивать разницу, я могу просто использовать последние X, которые я оставил после рекурсии, в качестве результата.

Почему-то работает следующий вопрос:

? - sub (s (0), s (0), X).
X = 0;

Но это не так:

? - sub (s (s (0)), s (s (0)), X).
false.

Кто-нибудь может указать на мою ошибку или предложить лучший способ реализации подпроцедуры?
Это может быть ошибкой новичка, поскольку я действительно мало что сделал. Извините, если это так.

// РЕДАКТИРОВАТЬ Вот как я решил это

sub(X, 0, X).
sub(0, _, 0).
% not sure why I didn't test this before, thought I did.
sub(s(X), s(Y), Diff) :-
  sub(X,Y,Diff).

Answer 1

sub(s(X), s(Y), X) :- sub(X,Y,X).

говорит, что

You can prove that     s(X)-s(Y) = X  
if you can prove that  X-Y = X

, что немного странно. Там должна быть третья переменная, Z.

Пролог пытается доказать (выполнить)

sub(s(s(0)), s(s(0)), X).

, что можно сделать, если

sub(s(0),s(0),s(0)).

потому что правая часть правила задается таким образом, устанавливая X=s(0) и Y=s(0) посредством сопоставления с образцом LHS.

Попытка доказать это sub(s(0),s(0),s(0)) еще раз означает использование правила (больше ничего применимо), положив X=0, Y=0, X=s(0). Но X не может быть одновременно 0 и s(0). Тупик! false.