Prolog 后继算术

Question

我有以下知识库：

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

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

add2(W+X,Y+Z,R) :- add(W,X,A),add(Y,Z,T),add2(A,T,R).
add2(X+Y,Z,R) :- add(X,Y,A),add2(A,Z,R).
add2(X,Y+Z,R) :- add(Y,Z,A),add2(X,A,R).
add2(X,Y,R) :-  add(X,Y,R).

正确评估查询，例如：

?- 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(s(0)+s(0), s(0+s(s(0))), Z).
Z = s(s(s(0+s(s(0))))) .

但要求的输出是：

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

我知道问题出在以下行：

add2(W+X,Y+Z,R) :- add(W,X,A),add(Y,Z,T),add2(A,T,R).

但我就是想不通。如有任何帮助，我们将不胜感激！

Answer 1

我认为您通过使用 add2/3 谓词处理案例使问题变得更加复杂。您首先需要将前两个参数的结构解析为形状 s(s(...s(0)...)).

为了做到这一点，我们可以创建一个 resolve/2 函数来查找 (+)/2 项并递归地使用 add/3:

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

所以现在语法：

E -> 0
E -> s(E)
E -> E + E

resolve/2 会将其转换为语法：

E -> 0
E -> s(E)

例如：

?- resolve(s(0)+s(0),X).
X = s(s(0)).

?- resolve(s(0+s(s(0))),X).
X = s(s(s(0))).

现在我们的 add2/3 谓词将首先 resolve/2 操作数，然后将它们相加：

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

您随后编写的示例查询解析为：

?- 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(s(0)+s(0), s(0+s(s(0))), Z).
Z = s(s(s(s(s(0))))).

Prolog 后继算术

Prolog Successor Arithmetic

prolog

successor-arithmetics