继承算术总和的最佳绿色削减是什么？

Question

神交在序言绿色削减我试图将它们添加到继任算术总和的标准定义(见谓词plus中什么是该查询的SLD树？).这个想法是通过消除所有无用的回溯(即,没有... ; false)尽可能"清理"输出,同时在参数实例化的所有可能组合下保持相同的行为 - 所有实例化,一个/两个/三个完全未实例化,以及所有变化包括部分实例化的args.

这是我在尝试尽可能接近这个理想时能够做到的事情(我承认错误的答案是如何插入绿色切割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..我的问题是:

• 我们如何证明上述削减是(或不是)绿色？
• 我们能否做到比上述计划更好,并通过添加其他一些绿色削减消除最后的回溯？
• 如果有,怎么样？

Answer 1

首先是一个小问题:plus/3交换的第一个和第二个参数的通用定义允许利用第一个参数索引.参见Prolog Art的Program 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))) ;
...

因此,您的计划不完整,因此任何有关进一步优化计划的问题都无关紧要.但我们可以做得更好,让我重申我们想要优化的实际定义:

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:现在只有切割之前的测试!之后所有的统一.

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

到目前为止,优化仅仅依赖于调查这两个条款的负责人.他们没有考虑递归规则.因此,它们可以在没有任何全局分析的情况下合并到Prolog编译器中.在O'Keefe的术语中,这些绿色削减可能被视为蓝色削减.引用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我们的模型,我们可以进一步避免选择点.在休息之后我会马上回来的:

最好使用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是剩余选择点的绿/蓝切割的最佳用法.你问了一个证明.好吧,我认为这远远超出了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答案有限的情况下不会终止吗？