prolog 如何使用 succ 运行递归查询？

有人可以向我解释一下为什么这个序言查询会这样工作吗？定义是：

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

鉴于这种：

?-  add(succ(succ(succ(0))),  succ(succ(0)),  R).

这是查询的轨迹：

Call:  (6)  add(succ(succ(succ(0))),  succ(succ(0)),  R) 

Call:  (7)  add(succ(succ(0)),  succ(succ(0)),  _G648) 

Call:  (8)  add(succ(0),  succ(succ(0)),  _G650) 

Call:  (9)  add(0,  succ(succ(0)),  _G652) 

Exit:  (9)  add(0,  succ(succ(0)),  succ(succ(0))) 

Exit:  (8)  add(succ(0),  succ(succ(0)),  succ(succ(succ(0)))) 

Exit:  (7)  add(succ(succ(0)),  succ(succ(0)), 
                                              succ(succ(succ(succ(0))))) 

Exit:  (6)  add(succ(succ(succ(0))),  succ(succ(0)), 
                                                succ(succ(succ(succ(succ(0))))))

该教程中最让我困惑的部分是，在第一个参数中，succ 被剥离，并且它会递归。不过，在递归时，R 获得了成功...如何实现？！另外，第一个出口（9）处的零从何而来？我是序言新手，我正在尝试理解作业中的语言。非常感谢任何帮助。

注意：对于任何感兴趣的人，本教程的链接是

你看，call and exit are verbs，解释器尝试解决您提出的查询而采取的操作。然后，跟踪会公开已完成的实际工作的详细信息，并让您以历史的角度查看它。

当 Prolog 必须选择一条规则（acall），它使用name你给它（所谓的functor），并尝试unify规则头部的每个参数。那么我们通常说 Prolog 也考虑arity，即用于选择的参数数量。

Unification尝试使两项“相等”，值得注意的结果被称为bindings变量。您已经知道变量是那些开头的名称Uppercase。这些名称标识规则中未指定的值，即placeholders为了争论。为了避免混淆，当 Prolog 显示跟踪时，变量被重命名，以便我们可以识别它们，因为相关细节是identities或在证明过程中建立的约束力。

然后你看到这样的_G648跟踪中的符号。他们留下来是为了尚未实例化被调用目标的参数，即R and Z。 R 是唯一的（仅出现在顶层调用中），因此此 Prolog 善意地保留用户友好的名称，但 Z 来自程序，可能会出现多次，然后被重命名。

回答这个问题

?-  add(succ(succ(succ(0))),  succ(succ(0)),  R).

Prolog首先尝试匹配

add(0,Y,Y). 

并失败，因为 succ(succ(succ(0)) 不能等于 0。 然后尝试

add(succ(X),Y,succ(Z)) :- add(X,Y,Z).

因此必须解决这些绑定（调用者术语的左侧）：

succ(succ(succ(0))) = succ(X)
succ(succ(0)) = Y
R = Z

你可以明白为什么 X 变成succ(succ(0))，我们有一个新的目标要证明，即规则体add(X,Y,Z)刚刚建立的绑定：

添加（succ（succ（0）），succ（succ（0）），_G648）

依此类推...直到 X 变为0和进球比赛

add(0,Y,Y).

那么Y就变成了succ(succ(0))，值得注意的是还给赋值给Z在调用规则中。

HTH