prolog - prolog 如何使用 succ 遍历递归查询？

Question

有人可以向我解释为什么这个序言查询会这样工作。定义是:

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

那个教程最让我困惑的部分是，在第一个参数中，成功被剥离了，并且它递归了。虽然在递归时，R 获得了成功......如何？!另外，第一个导出 (9) 处的零是从哪里来的？我是序言的新手，我正在努力理解家庭作业的语言。非常感谢任何帮助。

注意:任何有兴趣的人，本教程的链接是 http://www.learnprolognow.org/lpnpage.php?pagetype=html&pageid=lpn-htmlse9

Answer 1

你看，call和 exit是 verbs ，解释器为解决您提出的查询而采取的操作。然后，跟踪会显示已完成的实际工作的详细信息，并让您从历史角度查看它。

当 Prolog 必须选择一个规则(一个 call )时，它使用 name你给它(所谓的 functor )，并尝试给 unify规则头部的每个参数。然后我们通常说 Prolog 也考虑 arity ，即参数的数量，用于选择。
Unification试图“使”两个术语，值得注意的结果是所谓的bindings的变量。您已经知道变量是那些以 Uppercase 开头的名称。 .此类名称标识规则中未指定的值，即 placeholders为论据。为了避免混淆，当 Prolog 显示跟踪时，变量被重命名以便我们可以识别它们，因为相关的细节是 identities或在证明期间建立的绑定(bind)。

然后你看到这样的_G648跟踪中的符号。它们停留在被调用目标的尚未实例化的参数中，即 R和 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).

因此必须解决这些绑定(bind)(在左侧调用者的术语):

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

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

添加(成功(成功(0))，成功(成功(0))，_G648)

依此类推...直到 X 变为 0和目标匹配
add(0,Y,Y).
那么Y就变成了succ(succ(0))，值得注意的是还给 Z赋值在调用规则中。

高温高压