首先是一个小问题：plus/3 的通用定义交换了第一个和第二个参数，这允许利用第一个参数索引。参见 Prolog 艺术的程序 3.3。这也应该在您的previous post 中进行更改。我将调用您的交换定义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(<strong>X</strong>, Y, <b>X</b>) :- (...... -> <b>!</b> ; ... ), ...
所以，让我们构建一个反例：要使这个剪切以红色方式剪切，“写入统一”必须使其实际保护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 -> ！ % 第三个参数索引，例如耶克耶克，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 的术语中，这些绿色切割可能被视为蓝色切割。引用The Craft of Prolog，3.12：
蓝色剪切用于提醒 Prolog 系统注意它应该注意到但不会注意到的确定性。蓝切不会改变程序的可见行为：它们所做的只是让它变得可行。
绿色削减用于修剪可能成功或无关紧要或注定失败的尝试证明，但您不会期望 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) 与n > m 没有解决方案。因此，通过考虑plus/3 的模型，我们可以进一步避免选择点。休息后我马上回来：
最好使用 call_semidet/1！
它变得越来越复杂，优化可能很容易在程序中引入新的错误。优化程序也是维护的噩梦。出于实际编程目的，请使用 call_semidet/1。这是安全的，如果您的假设被证明是错误的，它将产生一个干净的错误。
回到正题：这是进一步的优化。如果Y 和Z 相同，则第二个子句不能适用：
pluso2(X, Y, Z) :-
% 第一部分：绿色削减
( X == 0 -> ! % 第一个参数索引
; Z == 0 -> ！ % 第三个参数索引，例如耶克耶克，ECLiPSe
; Y == Z，
ground(Z) -> ！
;真的
),
% 第二部分：原始统一
X = 0,
Y = Z，
自然数（Z）。
pluso2(s(X), Y, s(Z)) :- pluso2(X, Y, Z)。
我（目前）相信pluso2/3 是绿色/蓝色切割 w.r.t 的最佳用法。剩余的选择点。你要求证明。好吧，我认为这远远超出了 SO 的答案......
目标ground(Z) 是确保非终止属性所必需的。目标plus(s(_), Z, Z) 不会终止，该属性由ground(Z) 保留。也许您认为删除无限故障分支也是一个好主意？根据我的经验，这是相当有问题的。特别是，如果这些分支被自动删除。虽然乍一看这似乎是一个好主意，但它使程序开发变得更加脆弱：原本良性的程序更改现在可能会禁用优化，从而“导致”不终止。但无论如何，我们开始吧：
超越简单的绿色切割
pluso3(X, Y, Z) :-
% 第一部分：绿色削减
( X == 0 -> ! % 第一个参数索引
; Z == 0 -> ！ % 第三个参数索引，例如耶克耶克，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 在有有限多个答案时不会终止的情况吗？