recursion - Prolog中的递归成功加法

Question

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

我不明白这个是如何工作的。如果我运行查询：

add(succ(succ(succ(0))), succ(succ(0)), R)

它如何从第一个参数中删除 succ ？

如果我运行它：

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

这满足了身体。我们将它们输入到头部：

add(succ(X),Y,succ(Z)) %% becomes
add(succ(succ(succ(0))),succ(succ(0)),succ(R))

即它看起来好像它只是添加了成功，而不是从第一个参数中删除它们？我看到关于这个确切问题的另一篇文章，但这对我来说没有意义。

标签： recursionprologadditionsuccessor-arithmetics

Answer 1

当您调用目标add(succ(succ(succ(0))), succ(succ(0)), R)并且 Prolog 尝试使用 head 执行子句时add(succ(X),Y,succ(Z))，就会发生统一。统一是 Prolog 的核心概念之一，理解它很重要。统一也是操作员执行的=操作。执行子句头部时发生的情况与执行以下等效查询时发生的情况完全相同：

?- add(succ(succ(succ(0))), succ(succ(0)), R) = add(succ(X),Y,succ(Z)).

重要的是要理解统一不仅仅是“拆包”或“构建”术语，而是两者同时进行。

它可以从术语中“提取”信息：

?- X = f(a), Y = f(Z), X = Y.
X = Y, Y = f(a),
Z = a.

在这里，我们发现这a是 中f函子的参数X。

它可以“构造”术语：

?- X = f(Y), Y = g(h).
X = f(g(h)),
Y = g(h).

在这里，我们将术语“插入”g(h)到Y.X

它也可以同时对多个术语进行：

?- X = f(a, B), Y = f(A, b), X = Y.
X = Y, Y = f(a, b),
B = b,
A = a.

这里统一“解开”了这两个f术语，然后在每个术语中“填充”了一个洞。

现在，有了这些知识，你的例子中的统一有什么作用？

?- add(succ(succ(succ(0))), succ(succ(0)), R) = add(succ(X),Y,succ(Z)).
R = succ(Z),
X = Y, Y = succ(succ(0)).

特别是，当succ(succ(succ(0)))与 统一时succ(X)， this 将绑定X到succ(succ(0))。不受整个术语的约束，X而仅与“内部”部分有关。这就是从论点中删除一级的原因。succ(succ(succ(0)))succ