Prolog中的递归加法

Recursive addition in Prolog

知识库

add(0,Y,Y). // clause 1
add(succ(X),Y,succ(Z)) :- add(X,Y,Z). // clause 2

查询

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

我的问题

这是我感到困惑的地方。

  1. 一旦执行第一个子句,第二个子句自动执行 也被执行,然后将 succ() 添加到第一个参数?

  2. 还有,程序是怎么终止的,为什么不一直保持 将 succ() 无限添加到第一个和第三个参数?

Explanation from LearnPrologNow.com (which I don't understand)

Let’s go step by step through the way Prolog processes this query. The trace and search tree for the query are given below.

The first argument is not 0 , which means that only the second clause for add/3 can be used. This leads to a recursive call of add/3 . The outermost succ functor is stripped off the first argument of the original query, and the result becomes the first argument of the recursive query. The second argument is passed on unchanged to the recursive query, and the third argument of the recursive query is a variable, the internal variable _G648 in the trace given below. Note that _G648 is not instantiated yet. However it shares values with R (the variable that we used as the third argument in the original query) because R was instantiated to succ(_G648) when the query was unified with the head of the second clause. But that means that R is not a completely uninstantiated variable anymore. It is now a complex term, that has a (uninstantiated) variable as its argument.

The next two steps are essentially the same. With every step the first argument becomes one layer of succ smaller; both the trace and the search tree given below show this nicely. At the same time, a succ functor is added to R at every step, but always leaving the innermost variable uninstantiated. After the first recursive call R is succ(_G648) . After the second recursive call, _G648 is instantiated with succ(_G650) , so that R is succ(succ(_G650) . After the third recursive call, _G650 is instantiated with succ(_G652) and R therefore becomes succ(succ(succ(_G652))) . The search tree shows this step by step instantiation.

At this stage all succ functors have been stripped off the first argument and we can apply the base clause. The third argument is equated with the second argument, so the ‘hole’ (the uninstantiated variable) in the complex term R is finally filled, and we are through.

让我们从正确使用术语开始。

这些是子句,正如您正确指出的那样:

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

让我们先声明式阅读这个程序,以确保我们正确理解它的含义:

  1. 0加上Y就是Y。这是有道理的。
  2. 如果是真的X加上YZ那么X 加上 Y 的后继者是 Z 的后继者。

这是阅读此定义的好方法,因为它足够通用,涵盖了各种使用模式。例如,让我们从 最通用的查询 开始,其中所有参数都是新变量:

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

在这种情况下,"strip" 没有任何意义,因为 none 个参数已实例化。然而,Prolog 仍然报告了非常明智的答案,清楚地表明关系 成立 .

在你的例子中,你正在考虑一个不同的 query(不是 "predicate definition"!),即 query

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

这只是上面显示的更一般查询的特例,也是您程序的自然结果

我们也可以从另一个方向概括这个查询。例如,这是一个泛化,因为我们用逻辑变量替换了一个ground参数:

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

如果按照您发布的解释进行操作,您的生活将变得非常困难,并且会得出非常有限的逻辑程序视图:实际上,您将只能追踪一小部分模式,您 可以使用您的谓词,因此程序阅读与您实际描述的内容相去甚远。

如果您真的坚持程序阅读,请先从更简单的案例开始。例如,让我们考虑:

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

到"step through"程序上,我们可以进行如下处理:

  1. 第一个子句 匹配 吗? (请注意,"matching" 已经是有限的阅读:Prolog 实际上应用了 统一化 ,而程序阅读使我们远离了这种普遍性。)
  2. 回答:,因为s(_)0不统一。所以只有第二个条款适用。
  3. 第二个子句只成立 if 它的主体成立,在这种情况下 if add(0, succ(0), Z) 成立。并且 this 成立(通过应用 第一个子句 if Z is succ(0)Rsucc(Z).
  4. 因此,一个答案R = succ(succ(0)).。此答案已报告
  5. 是否有其他解决方案?这些仅在 回溯 时报告。
  6. 答案:,没有其他解决方案,因为没有进一步的子句匹配。

我把它作为练习,将这种艰苦的方法应用于书中所示的更复杂的查询。这样做很简单,但会越来越多地让您远离逻辑程序最有价值的方面,这些方面体现在它们的普遍性和优雅的声明式表达中。

你关于 终止 的问题既微妙又富有洞察力。注意我们必须区分Prolog中的existentialuniversal终止

例如,再次考虑上面显示的最一般的查询:它产生答案,但不会终止。对于要报告的答案,找到使查询 true 的答案替换就足够了。在您的示例中就是这种情况。如果有任何可能存在的替代方案,将在回溯时进行尝试和报告。

您始终可以尝试以下方法来测试查询的 终止 :只需附加 false/0,例如:

?- add(X, Y, Z), false.
nontermination

这让您可以专注于终止属性,而不用关心具体的答案。

另请注意,add/3 是一个糟糕的关系名称:命令总是暗示着 方向 ,但实际上 general 并且即使 none 的参数甚至被实例化也可用!一个好的谓词名称应该反映这种普遍性。