Prolog 中带有 Peano 数字的递归加法不起作用

Question

我目前正在尝试练习一些 Prolog。我刚开始，我面临一个我不太明白的问题。我想递归地确定一个皮亚诺数是否是另一个皮亚诺数的两倍。我试图这样解决它：

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

由于某种原因它不起作用。有谁知道为什么？

Answer 1

您不需要三个参数来定义这样的谓词。只需考虑它应该描述什么关系：数字与其双精度数之间的关系。因此，您只需要两个参数和两个描述这两种可能性的规则。要么数字为零，那么它的双精度也为零。否则，每次递归中的双精度数相差 2 s/2，但数字只有 1：

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

或者如果您想按照 cmets 中的建议测试一对：

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