Prolog peano 数字差/减法答案

【问题标题】：Prolog peano numbers difference/subtractionProlog peano 数字差/减法
【发布时间】：2020-04-16 17:17:12
【问题描述】：

我正在尝试计算“Peano 数字”(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).

【问题讨论】：

在您的原始定义中，很少出现 0。这是故意的吗？
嗯，当数字相同时应该出现0，或者右边大于左边。或者你是什么意思？
在您的原始定义中，第一个参数没有 0。但是随后您给出了一个定义，它也作为第一个参数出现。这两者如何对应？
@false 哦，这是因为根据定义，只要左操作数为零，结果也必须为零，因为没有负值。至少这就是我这样做的原因。我只是没有将它作为单独的规则添加为信息，因为它是由其他规则产生的。
这正是我的观点。因此，您确信它们遵循现有规则。我没有看到 0 - 0 = 0 遵循您的定义。不是吗？

标签： recursion prolog successor-arithmetics

【解决方案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)).

因为规则的右侧是通过 LHS 的模式匹配定位 X=s(0) 和 Y=s(0) 来设置的。

再次尝试证明sub(s(0),s(0),s(0)) 意味着使用规则（没有其他适用），假设X=0、Y=0、X=s(0)。但是X 不能同时是0 和s(0)。僵局！ false.

【讨论】：

感谢您的解释。您对如何改进我的子程序有什么建议吗？我这样做的原因是，因为我必须递归减少x 和y，同时在结果周围添加s()，我无法让它工作。