Prolog递归加法异常求助：s(0)与p(0)无法抵消导致结果错误

我写了一段Prolog代码实现带s(0)（0的后继）和p(0)（0的前驱）的加法，执行查询：

?- add3(p(0)+s(s(0)),s(s(0)),Z). 

得到结果Z = p(s(s(s(s(0)))))，但预期结果应该是Z = s(s(s(0)))——因为p(0)本该和一个s(0)抵消。不清楚递归哪里出问题，求排查。

原知识库代码 #

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

% Base case when 0 cannot be broken down further
simple(0,0).
simple(p(s(0)), 0).
simple(s(p(0)), 0).

% Change to make to simplify expression

simple(s(X),s(Y)) :-
    simple(X,Y).

simple(p(X), p(Y)) :-
    simple(X, Y).

% Case if X+Y
simple(X+Y,Z) :-
    simple(X,XS),
    simple(Y,YS),
    add(XS,YS,Z).

% add3
add3(A,B,C) :-
    simple(A,RA),
    simple(B,RB),
    add(RA,RB,C).

问题根源 #

你的simple/2规则只处理直接嵌套的s(p(0))或p(s(0))，但当化简p(0)+s(s(0))时，simple/2会先分别化简p(0)和s(s(0))——这两个都触发不了抵消的基准规则（p(0)不是p(s(0))，s(s(0))也不是s(p(0))）。随后调用add(p(0), s(s(0)), Z)，原add/3规则直接给结果加了p前缀，得到p(s(s(0)))，再和第二个参数s(s(0))相加，最终得到p(s(s(s(s(0)))))，完全没机会触发抵消逻辑。

简单说：你的化简逻辑只处理已经成对出现的s(p(...))或p(s(...))，但没处理分散的p和s在加法后可以抵消的情况。

修复方案 #

方案1：先合并为纯序列再化简

调整思路：先把所有表达式转换成纯s/p的嵌套序列，再对序列进行化简抵消p和s。

修改后的代码：

% 基础加法：将表达式转换为纯s/p嵌套形式
add_raw(0, X, X).
add_raw(s(X), Y, s(Z)) :- add_raw(X, Y, Z).
add_raw(p(X), Y, p(Z)) :- add_raw(X, Y, Z).
add_raw(X+Y, Z, Result) :- add_raw(X, Y, Temp), add_raw(Temp, Z, Result).

% 化简纯s/p序列：抵消相邻的p和s
simplify(0, 0).
simplify(s(p(X)), Y) :- simplify(X, Y).
simplify(p(s(X)), Y) :- simplify(X, Y).
simplify(s(X), s(Y)) :- simplify(X, Y).
simplify(p(X), p(Y)) :- simplify(X, Y).

% 最终的add3：先转成纯序列，再化简
add3(A, B, C) :-
    add_raw(A, B, Temp),
    simplify(Temp, C).

方案2：调整化简顺序（先相加再化简）

修改原simple/2的加法规则，先执行加法再化简，而非先化简再相加：

% 原add规则保留
add(0,X,X).
add(s(X),Y,s(Z)) :- add(X,Y,Z).
add(p(X), Y, p(Z)) :- add(X,Y,Z).

% 化简规则调整：加法先计算再化简
simple(0,0).
simple(s(p(X)), Y) :- simple(X, Y).
simple(p(s(X)), Y) :- simple(X, Y).
simple(s(X), s(Y)) :- simple(X, Y).
simple(p(X), p(Y)) :- simple(X, Y).
simple(X+Y,Z) :-
    add(X,Y,Temp),  % 先相加，再化简
    simple(Temp,Z).

% add3规则：最后再对加法结果化简一次
add3(A,B,C) :-
    simple(A,RA),
    simple(B,RB),
    add(RA,RB,Temp),
    simple(Temp,C).

测试验证 #

执行原查询：

?- add3(p(0)+s(s(0)),s(s(0)),Z). 

两种方案都会得到正确结果：Z = s(s(s(0)))

内容的提问来源于stack exchange，提问作者ggplot2