1

我正在尝试计算“Peano numbers”（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)。
错误的。

谁能指出我的错误或提出更好的方法来实现子程序？
这可能是初学者的错误，因为我真的没有做太多。对不起，如果是这样的话。

//编辑 这就是我解决它的方法

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

1 回答 1

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。

Prolog 试图证明（使真实）

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.

于 2020-04-16T17:45:40.437 回答