Prolog中单目加法的置换合成逻辑解析——基于给定代码的技术问询

这段代码用Prolog的后继表示法（s(X)代表X的后继，即X+1）实现加法，核心逻辑靠置换（交换两个加数位置）完成递归推导，下面拆解具体运作方式：

核心规则拆解 #

基础终止子句 #

plus2(0, X, X).          % 0+X = X

这是加法的基础事实：0与任何数X相加结果都是X，是递归的终止条件，无需进一步推导。

递归置换子句 #

plus2(s(X), Y, s(Z)) :-    plus2(Y, X, Z).      % (X+1) + Y = Z+1  therefore  Y+X=Z

这条规则就是置换合成的核心体现：

• 规则左端要解决的问题是「X+1 和 Y 相加等于 Z+1」
• 它通过置换两个加数的位置，将问题转化为「求 Y 和 X 相加等于 Z」——把(X+1)+Y的复杂问题，转换成Y+X的简化问题，递归得到Z后，给结果加1（用s(Z)表示），就得到原问题的解。

置换逻辑的实际运作示例 #

以查询plus2(s(s(0)), s(0), R)（即计算2+1）为例：

1. 匹配递归子句：将s(s(0))对应为s(X)（即X=s(0)），Y=s(0)，需要调用plus2(s(0), s(0), Z)来求Z
2. 再次匹配递归子句：将s(0)对应为s(X)（即X=0），Y=s(0)，调用plus2(s(0), 0, Z1)
3. 第三次匹配递归子句：将s(0)对应为s(X)（即X=0），Y=0，调用plus2(0, 0, Z2)
4. 触发基础子句：plus2(0,0,0)，得到Z2=0
5. 回溯推导：Z1=s(Z2)=s(0) → Z=s(Z1)=s(s(0)) → R=s(Z)=s(s(s(0)))（即3）

整个过程中，每次递归都通过置换加数位置，把第一个加数逐步拆解到0（触发终止条件），再反向推导得到最终结果。这种置换本质是利用加法交换律，将问题逐步简化，最终落地到基础规则上。

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