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

Question

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

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 或在证明期间建立的绑定。

然后你会在跟踪中看到这样的_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).

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

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

Answer 2

“第一个出口 (9) 处的零从何而来？”

调用add(0, succ(succ(0)), _G652) 与第一个子句统一，即如果add 的第一个参数为零，则第二个和第三个相同。在这种特殊情况下，变量 _G652 变为 succ(succ(0))。

“虽然在递归时，R 获得了成功......如何？！”

这是应用第二个子句的结果。该子句（大致）表明您首先从第一个参数中去除succ，然后递归调用add，最后，将succ 的另一个“层”添加到此递归调用返回的第三个参数。

谓词 add 只不过是 Peano 算术中加法的直接实现：http://en.wikipedia.org/wiki/Peano_axioms#Addition

Answer 3

带有更多注释的（希望）更清晰的痕迹是：

 (6) Call:  add(succ(succ(succ(0))),  succ(succ(0)),  R)          % R     = succ(_G648)
      (7) Call:  add(succ(succ(0)),  succ(succ(0)),  _G648)       % _G648 = succ(_G650) 
           (8) Call:  add(succ(0),  succ(succ(0)),  _G650)        % _G650 = succ(_G652) 
                (9) Call:  add(0,  succ(succ(0)),  _G652)         % _G652 = succ(succ(0))
                (9) Exit:  add(0,  succ(succ(0)),  succ(succ(0)))       
           (8) Exit:  add(succ(0),  succ(succ(0)),  succ(succ(succ(0)))) 
      (7) Exit:  add(succ(succ(0)),  succ(succ(0)), succ(succ(succ(succ(0))))) 
 (6) Exit:  add(succ(succ(succ(0))),  succ(succ(0)), succ(succ(succ(succ(succ(0))))))

如你所见，四个出口是多余的，最终答案已经知道在(9) Exit这一点上；那时只有一个出口就足够了：

     %     R = succ(_G648)
     %              _G648 = succ(_G650) 
     %                           _G650 = succ(_G652) 
     %                                        _G652 = succ(succ(0))
     % thus,
     %     R = succ(        succ(        succ(        succ(succ(0)) )))

这确实是尾调用优化下发生的情况，因为谓词定义是确实是尾递归的，R 下的结果是以自上而下的方式构建的，带有“洞”逐渐被逻辑变量的实例化填充。所以succ( _ )不是在递归调用之后添加的，而是在之前它建立的。这也是尾递归取模cons优化的精髓。