prolog - Prolog 定义自然数遵循哪些步骤？

Question

我正在学习如何在 Prolog 中编程，我发现了下一个定义自然数及其总和的程序:

sum( succ( X ), Y, succ( Z )) :- sum( X, Y, Z ).
sum( 0, X, X ).
?- sum( succ( succ(0)), succ( succ( succ(0))), Answer ).
Answer = succ( succ( succ( succ( succ(0)))))

(找到 here )

问题是我正在努力解决这个程序的执行流程。说实话我不知道它有什么作用。 Prolog 如何计算出 Answer 的值？ Prolog 遵循哪些步骤来查找答案的值？

提前致谢。

Answer 1

它有助于理解 Prolog 在计算现有谓词或设计新谓词时如何运行。当您进行如下查询时:

sum( succ(succ(0)), succ(succ(succ(0))), Answer ).

Prolog 将查找匹配 sum(_, _, _) 的事实和规则( sum/3 ) 并选择第一个匹配的。现行规则是:

(1) sum( succ(X), Y, succ(Z) ) :- sum( X, Y, Z ).
(2) sum( 0, X, X ).

如果您查看该查询，它显然与规则 #1 的模式匹配。请记住，在 Prolog 中，变量可以实例化为任何类型的术语，并且同名变量是统一的(实例化为相同的值)。当 Prolog 将规则 #1 的“头部”与查询统一时，它通过统一变量来实现，如下所示:

    X = succ(0)
    Y = succ(succ(succ(0)))
(A) Answer = succ(Z)

请注意Answer值为 succ(Z)即使Z尚未绑定(bind)(分配具体值)。现在我们遵循规则，它将查询 sum(X, Y, Z) ，这将是查询:

sum( succ(0), succ(succ(succ(0))), Z )
       |        |                  |
       X        Y                  Z

Prolog 现在将再次从顶部开始，因为这是 sum/3 的新查询。就像第一次一样，它匹配规则 #1 并具有以下统一:

    X = 0
    Y = succ(succ(succ(0)))
(B) Z = succ(Z')

我正在使用Z'与其他变量 Z 区分开来在 sum(succ(0), succ(succ(succ(0))), Z) ，因为它是不同的 Z比头部使用的 sum(..., succ(Z)) 。这就像如果您在 C 中有一个函数声明为 int f(x) { return 2*x; }然后你用另一个局部变量 x 来调用它从某个地方，那个名字x用在两个不同的地方，代表两个不同的变量)。

然后我们可以进行下一个递归查询，sum(X, Y, Z')再次，变成:

sum( 0, succ(succ(succ(0))), Z' )
     |    |                  |
     X    Y                  Z'

此递归查询与第 1 条规则不匹配，因为第一个参数 0 ，与 succ(X) 不匹配。但是，它符合规则#2:

    0 = 0
    X = succ(succ(succ(0)))
(C) X = Z'

现在X = succ(succ(succ(0)))所以Z' = succ(succ(succ(0))) 。由于该规则中不再有查询，因此它最终成功返回到查询的位置。将其返回到上面的 (B):

Z = succ(Z') = succ(succ(succ(succ(0))))

并将其返回给 (A):

Answer = succ(Z) = succ(succ(succ(succ(succ(0)))))

这就是你想要的。使用trace @CapelliC 提到的设施，您可以观察 Prolog 解释器中发生的这些连续步骤并遵循变量的实例化。