To grok green cuts in Prolog I am trying to add them to the standard definition of sum in successor arithmetics (see predicate plus in What's the SLD tree for this query?). The idea is to "clean up" the output as much as possible by eliminating all useless backtracks (i.e., no ... ; false) while keeping identical behavior under all possible combinations of argument instantiations - all instantiated, one/two/three completely uninstantiated, and all variations including partially instantiated args.

This is what I was able to do while trying to come as close as possible to this ideal (I acknowledge false's answer to how to insert green cuts into append/3 as a source):

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

Under SWI this seems to work fine for all queries but those with shape ?- plus(+X, -Y, +Z)., as for SWI's notation of predicate description. For instance, ?- plus(s(s(0)), Y, s(s(s(0)))). yields Y = s(0) ; false.. My questions are:

How do we prove that the above cuts are (or are not) green?
Can we do better than the above program and eliminate also the last backtrack by adding some other green cuts?
If yes, how?

第一个小问题：共同定义plus/3具有在第一和第二个参数交换，其允许利用第一参数的索引。见序言的艺术计划3.3。这应该也可以在你改变以前的帖子。我会打电话给你的交换定义plusp/3和你的优化定义pluspo/3 。因此，给定

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

检测红色切口（问题一）

如何证明或反驳红/绿削减？首先，看在后卫“写” -unifications。即，对于前切割任何此类unifications。在您的优化方案：

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

所以，你的程序是不完整的，并且关于进一步优化它的任何问题，因此是不相关的。但是，我们可以做的更好，让我重申，我们要优化的实际定义：

plus(0, X, X) :- natural_number(X).
plus(s(X), Y, s(Z)) :- plus(X, Y, Z).

在几乎所有的Prolog系统来说，首先是参数的索引，这使得下面的查询确定的：

?- plus(s(0),0,X).
X = s(0).

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

?- plus(X, Y, 0).
X = Y, Y = 0 ;
false.

什么，你可能想要写的是：

pluso(X, Y, Z) :-
   % Part one: green cuts
   (  X == 0 -> !  % first-argument indexing
   ;  Z == 0 -> !  % 3rd-argument indexing, e.g. Jekejeke, ECLiPSe
   ;  true
   ),
   % Part two: the original unifications
   X = 0,
   Y = Z,
   natural_number(Z).
pluso(s(X), Y, s(Z)) :- pluso(X, Y, Z).

注意差异pluspo/3 ：现在只有测试之前，切！所有unifications是其后。

?- pluso(X, Y, 0).
X = Y, Y = 0.

该优化只能在调查两个子句的头到目前为止依赖。他们没有考虑到递归规则。因此，它们可以纳入Prolog的编译器没有任何全球性的分析。在奥基夫的术语，这些绿色的削减可能会被视为蓝色削减。举的Prolog的工艺，3.12：

蓝削减在那里，提醒Prolog的系统，它应该已经注意到一个确定性，但不会。蓝削减不改变程序的可视行为：他们做的是使之可行。
绿色削减在那里精简掉试图证明这会成功或者是无关紧要的，或将注定要失败的，但你不希望Prolog的系统能够告诉。

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

现在，你考虑的另一个查询：

?- pluso(X, s(s(0)), s(s(s(0)))).
X = s(0) ;
false.

或把一个简单的情况：

?- pluso(X, s(0), s(0)).
X = 0 ;
false.

在这里，无论是头应用，因此系统不能够确定决定。但是，我们知道，有没有解决的一个进球plus(X, s^n, s^m)与n > m 。所以，考虑的模型plus/3 ，我们可以进一步避免choicepoints。我会在这次休息之后马上回来：

更好地利用call_semidet / 1！

它变得越来越复杂，并有机会，优化可以很容易地在程序中引入新的错误。还优化程序，以保持一个噩梦。对于实际的编程目的使用，而call_semidet/1 。它是安全的，并会产生一个干净的误差应你的假设变成是假的。

返回业务：这里是一个进一步的优化。如果Y和Z是相同的，第二句话不能申请：

pluso2(X, Y, Z) :-
   % Part one: green cuts
   (  X == 0 -> !  % first-argument indexing
   ;  Z == 0 -> !  % 3rd-argument indexing, e.g. Jekejeke, ECLiPSe
   ;  Y == Z, ground(Z) -> !
   ;  true
   ),
   % Part two: the original unifications
   X = 0,
   Y = Z,
   natural_number(Z).
pluso2(s(X), Y, s(Z)) :- pluso2(X, Y, Z).

我（目前）认为， pluso2/3是绿/蓝削减WRT剩choicepoints的最佳使用。你问了一个证明。嗯，我认为这是远远超出一个SO回答...

我们的目标ground(Z)是必要的，以确保未结束的属性。我们的目标plus(s(_), Z, Z)不会终止，该属性由保存ground(Z) 也许你认为这是一个好主意，除去无限故障分支吗？根据我的经验，这是相当有问题的。特别是，如果这些分支被自动删除。虽然乍一看这似乎是个好主意，它使程序开发更脆：原本良性的程序变化，现在可能会禁用优化，因而“因”未结束。但无论如何，在这里我们去：

除了简单的绿色切削

pluso3(X, Y, Z) :-
   % Part one: green cuts
   (  X == 0 -> !  % first-argument indexing
   ;  Z == 0 -> !  % 3rd-argument indexing, e.g. Jekejeke, ECLiPSe
   ;  Y == Z -> !
   ; var(Z), nonvar(Y), \+ unify_with_occurs_check(Z, Y) -> !, fail
   ; var(Z), nonvar(X), \+ unify_with_occurs_check(Z, X) -> !, fail
   ;  true
   ),
   % Part two: the original unifications
   X = 0,
   Y = Z,
   natural_number(Z).
pluso3(s(X), Y, s(Z)) :- pluso3(X, Y, Z).

你能找到其中的情况下pluso3/3 ，同时也有有限个答案不会终止？