Prolog前身数学

Question

我有一个add2谓词，其解析如下：s(0)是0的后继者，即1

?- add2(s(0)+s(s(0)), s(s(0)), Z).
Z = s(s(s(s(s(0)))))

?- add2(0, s(0)+s(s(0)), Z).
Z = s(s(s(0)))

?- add2(s(s(0)), s(0)+s(s(0)), Z).
Z = s(s(s(s(s(0)))))

等。

我正在尝试添加一个类似这样的前置谓词

?- add2(p(s(0)), s(s(0)), Z).
Z = s(s(0))

?- add2(0, s(p(0)), Z).
Z = 0

?- add2(p(0)+s(s(0)),s(s(0)),Z).
Z = s(s(s(0)))

?- add2(p(0), p(0)+s(p(0)), Z).
Z = p(p(0))

我似乎找不到解决方法。我的代码在下面。

numeral(0).
numeral(s(X)) :- numeral(X).
numeral(X+Y) :- numeral(X), numeral(Y).
numeral(p(X)) :- numeral(X).


add(0,X,X).
add(s(X),Y,s(Z)) :- add(X,Y,Z).
add(p(X),Y,p(Z)) :- add(X,Y,Z).


resolve(0,0).
resolve(s(X),s(Y)) :-
    resolve(X,Y).
resolve(p(X),p(Y)) :-
    resolve(X,Y).
resolve(X+Y,Z) :-
    resolve(X,RX),
    resolve(Y,RY),
    add(RX,RY,Z).

add2(A,B,C) :-
    resolve(A,RA),
    resolve(B,RB),
    add(RA,RB,C).

Answer 1

[通常，添加后继算术意味着处理后继项，其形状为0或s(X)，其中X也是后继项。您的代码的这一部分将完全解决此问题：

add(0,X,X).
add(s(X),Y,s(Z)) :- add(X,Y,Z).

现在您必须做出决定；您可以在add/3中处理前置词和加法项，也可以将此谓词包装在另一个将处理它们的谓词中。您似乎选择用add/3包装add2/3。在这种情况下，您肯定需要创建一个归约项，例如您在此处用resolve/2构建的，我同意您对它的part的实现：

resolve(0,0).
resolve(s(X),s(Y)) :-
    resolve(X,Y).
resolve(X+Y,Z) :-
    resolve(X,RX),
    resolve(Y,RY),
    add(RX,RY,Z).

这一切都很好。您现在所缺少的是一种处理p(X)术语的方法。正确的方法是注意，您已经可以通过将add/3与s(0)结合使用来将其减一：

resolve(p(X), R) :-
    resolve(X, X1),
    add(s(0), R, X1).
换句话说，不是使用X = Y-1计算X，而是使用X + 1 = Y计算X。

提供的输入永远不会为负，您的add2/3谓词现在可以使用。