首先是一个小问题：第一个和第二个参数交换的通用定义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在有有限多个答案的情况下不会终止的情况吗？