6

为了了解 Prolog 中的绿色切割，我试图将它们添加到后继算术中 sum 的标准定义中（参见What's the SLD tree for this query?plus中的谓词）。这个想法是通过消除所有无用的回溯（即 no ）来尽可能“清理”输出，同时在所有可能的参数实例化组合下保持相同的行为 - 所有实例化，一/二/三个完全未实例化，以及所有变体包括部分实例化的参数。... ; false

这是我在尝试尽可能接近这个理想时能够做到的（我承认 false 对如何将绿色剪辑append/3作为源插入的回答）：

natural_number(0).
natural_number(s(X)) :- natural_number(X).

plus(X, Y, X) :- (Y == 0 -> ! ; Y = 0), (X == 0 -> ! ; true), natural_number(X).
plus(X, s(Y), s(Z)) :- plus(X, Y, Z).

在 SWI 下，这似乎适用于所有查询，但形状为 的查询除外?- plus(+X, -Y, +Z).，至于SWI 的谓词描述符号。例如，?- plus(s(s(0)), Y, s(s(s(0)))).产量Y = s(0) ; false.。我的问题是：

  • 我们如何证明上述削减是（或不是）绿色？
  • 我们能否比上述程序做得更好，并通过添加一些其他绿色削减来消除最后的回溯？
  • 如果是，如何？
4

1 回答 1

8

首先是一个小问题：第一个和第二个参数交换的通用定义plus/3允许利用第一个参数索引。参见 Prolog 艺术的程序 3.3。这也应该在你以前的帖子中改变。我将调用您的交换定义plusp/3和优化定义pluspo/3。因此，给定

plusp(X, 0, X) :- natural_number(X)。
plusp(X, s(Y), s(Z)) :- plusp(X, Y, Z)。

检测红色切口（问题一）

如何证明或反驳红/绿削减？首先，注意守卫中的“写”统一。也就是说，对于削减之前的任何此类统一。在您优化的程序中：

pluspo(X, Y, X) :- (Y == 0 -> ! ; Y = 0), (X == 0 -> ! ; true), ...

我发现以下内容：

pluspo(X, Y, X) :- (...... -> ! ; ... ), ...

所以，让我们构造一个反例：要使这个剪切以红色方式剪切，“写统一”必须使其实际保护为Y == 0真。这意味着构造的目标必须以某种方式包含常量 0。只有两种可能性需要考虑。第一个或第三个参数。最后一个参数中的零意味着我们至多有一个解决方案，因此不可能删除进一步的解决方案。所以，0 必须在第一个参数中！（第二个参数从一开始就不能为 0，否则“写统一不会产生不利影响。）这是一个这样的反例：

?- pluspo(0, Y, Y).

它提供了一个正确的解决方案Y = 0，但隐藏了所有其他的解决方案！所以在这里我们有一个如此邪恶的红色切割！并将其与提供无限多解决方案的未优化程序进行对比：

Y = 0 ;
Y = s(0) ;
Y = s(s(0)) ;
Y = s(s(s(0))) ;
...

因此，您的程序是不完整的，因此有关进一步优化它的任何问题都无关紧要。但是我们可以做得更好，让我重申一下我们想要优化的实际定义：

加（0，X，X）：-自然数（X）。
加（s（X），Y，s（Z））：-加（X，Y，Z）。

实际上，在所有 Prolog 系统中，都有第一个参数索引，这使得以下查询具有确定性：

?- 加(s(0),0,X)。
X = s(0)。

但是许多系统不支持（完整的）第三个参数索引。因此我们得到 SWI、YAP、SICStus：

?- 加（X，Y，0）。
X = Y, Y = 0 ;
假的。

你可能想写的是：

加号（X，Y，Z）：-
   % 第一部分：绿色削减
   ( X == 0 -> ! % 第一个参数索引
   ; Z == 0 -> ！% 3rd-argument 索引，例如 Jekejeke、ECLiPSe
   ; 真的
   ),
   % 第二部分：原始统一
   X = 0,
   Y = Z，
   自然数（Z）。
pluso(s(X), Y, s(Z)) :- pluso(X, Y, Z)。

请注意与以下各项的区别pluspo/3：现在只有在削减之前的测试！此后所有的统一。

?- pluso(X, Y, 0)。
X = Y，Y = 0。

到目前为止的优化只依赖于调查这两个子句的头部。他们没有考虑递归规则。因此，它们可以被合并到 Prolog 编译器中，而无需任何全局分析。在 O'Keefe 的术语中，这些绿色切割可能被视为蓝色切割。引用Prolog 的工艺，3.12：

蓝色的削减是为了提醒 Prolog 系统注意它应该注意到但不会注意到的确定性。蓝切不会改变程序的可见行为：它们所做的只是让它变得可行。

Green cut 用于剪除可能成功或无关紧要或注定失败的尝试证明，但您不会期望 Prolog 系统能够分辨出这一点。

然而，关键是这些削减确实需要一些警卫才能正常工作。

现在，您考虑了另一个查询：

?- pluso(X, s(s(0)), s(s(s(0))))。
X = s(0) ;
假的。

或者说一个更简单的情况：

?- pluso(X, s(0), s(0))。
X = 0 ;
假的。

在这里，两个头都适用，因此系统无法确定确定性。但是，我们知道>无法解决目标plus(X, s^n, s^m)。所以通过考虑模型我们可以进一步避免选择点。休息后我马上回来：nmplus/3

最好使用 call_semidet/1！

它变得越来越复杂，优化可能很容易在程序中引入新的错误。优化程序也是维护的噩梦。出于实际编程目的，请使用call_semidet/1. 它是安全的，如果你的假设被证明是错误的，它将产生一个干净的错误。

回到正题：这是进一步的优化。如果Y和Z相同，则第二个子句不能适用：

pluso2(X, Y, Z) :-
   % 第一部分：绿色削减
   ( X == 0 -> ! % 第一个参数索引
   ; Z == 0 -> ！% 3rd-argument 索引，例如 Jekejeke、ECLiPSe
   ; Y == Z，地面（Z） ->！
   ; 真的
   ),
   % 第二部分：原始统一
   X = 0,
   Y = Z，
   自然数（Z）。
pluso2(s(X), Y, s(Z)) :- pluso2(X, Y, Z)。

我（目前）认为这pluso2/3是剩余选择点的绿色/蓝色切割的最佳使用。你要求证明。好吧，我认为这远远超出了 SO 的答案......

目标ground(Z)是确保非终止属性所必需的。目标plus(s(_), Z, Z)不会终止，该属性由ground(Z). 也许您认为删除无限故障分支也是一个好主意？根据我的经验，这是相当有问题的。特别是，如果这些分支被自动删除。虽然乍一看这似乎是一个好主意，但它使程序开发变得更加脆弱：原本良性的程序更改现在可能会禁用优化，从而“导致”不终止。但无论如何，我们开始吧：

超越简单的绿色切割

pluso3(X, Y, Z) :-
   % 第一部分：绿色削减
   ( X == 0 -> ! % 第一个参数索引
   ; Z == 0 -> ！% 3rd-argument 索引，例如 Jekejeke、ECLiPSe
   ; Y == Z -> ！
   ; var(Z), nonvar(Y), \+ unify_with_occurs_check(Z, Y) -> !, 失败
   ; var(Z), nonvar(X), \+ unify_with_occurs_check(Z, X) -> !, 失败
   ; 真的
   ),
   % 第二部分：原始统一
   X = 0,
   Y = Z，
   自然数（Z）。
pluso3(s(X), Y, s(Z)) :- pluso3(X, Y, Z)。

你能找到一个pluso3/3在有有限多个答案的情况下不会终止的情况吗？

于 2012-11-09T15:53:44.077 回答