后继算术和的最佳绿色削减是什么? [英] What are the optimal green cuts for successor arithmetics sum?
问题描述
为了了解 Prolog 中的绿色切割，我试图将它们添加到后继算术中 sum 的标准定义中(请参阅 这个查询的 SLD 树是什么?).这个想法是通过消除所有无用的回溯(即，没有 ... ; false)尽可能清理"输出，同时在所有可能的参数实例化组合下保持相同的行为 - 所有实例化，一/二/三完全未实例化，以及所有变体，包括部分实例化的参数.
这是我在尝试尽可能接近这个理想时能够做到的(我承认 false 对 如何将绿色剪辑插入 append/3 作为来源):
natural_number(0).自然数(s(X)):- 自然数(X).plus(X, Y, X) :- (Y == 0 -> ! ; Y = 0), (X == 0 -> ! ; true), natural_number(X).加(X，s(Y)，s(Z)):-加(X，Y，Z).在 SWI 下，这似乎适用于所有查询，但形状为 ?- plus(+X, -Y, +Z).，至于 SWI 的谓词描述符号.例如， ?- plus(s(s(0)), Y, s(s(s(0)))). 产生 Y = s(0) ；错误..我的问题是:
- 我们如何证明上述切割是(或不是)绿色?
- 我们能否比上面的程序做得更好，并通过添加一些其他绿色削减来消除最后的回溯?
- 如果是，怎么做?
首先是一个小问题:plus/3 的通用定义交换了第一个和第二个参数，这允许利用第一个参数索引.参见 Prolog 艺术的程序 3.3.这也应该在您的上一篇文章中进行更改.我将把你的交换定义称为 plusp/3 和你的优化定义 pluspo/3.因此，给定
检测红色切口(问题一)
如何证明或反驳红/绿削减?首先，注意守卫中的写"统一.也就是说，对于削减之前的任何此类统一.在您优化的程序中:
<块引用>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，但隐藏了所有其他的解决方案！所以在这里我们有一个如此邪恶的红色切割！并将其与提供无限多解决方案的未优化程序进行对比:
因此，您的程序是不完整的，因此有关进一步优化它的任何问题都无关紧要.但我们可以做得更好，让我重申一下我们想要优化的实际定义:
<上一页>加(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 的不同之处:现在只有剪切前的测试！此后所有的统一.
到目前为止的优化只依赖于调查两个子句的头部.他们没有考虑递归规则.因此，它们可以被合并到 Prolog 编译器中，而无需任何全局分析.在 O'Keefe 的术语中，这些绿色切割可能被视为蓝色切割.引用 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/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 在有有限多个答案时不会终止的情况吗?
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?
First a minor issue: the common definition of plus/3 has the first and second argument exchanged which allows to exploit first-argument indexing. See Program 3.3 of the Art of Prolog. That should also be changed in your previous post. I will call your exchanged definition plusp/3 and your optimized definition pluspo/3. Thus, given
plusp(X, 0, X) :- natural_number(X). plusp(X, s(Y), s(Z)) :- plusp(X, Y, Z).
Detecting red cuts (question one)
How to prove or disprove red/green cuts? First of all, watch for "write"-unifications in the guard. That is, for any such unifications prior to the cut. In your optimized program:
pluspo(X, Y, X) :- (Y == 0 -> ! ; Y = 0), (X == 0 -> ! ; true), ...
I spot the following:
pluspo(X, Y, X) :- (...... -> ! ; ... ), ...
So, let us construct a counterexample: To make this cut cut in a red manner, the "write unification" must make its actual guard Y == 0 true. Which means that the goal to construct must contain the constant 0 somehow. There are only two possibilities to consider. The first or third argument. A zero in the last argument means that we have at most one solution, thus no possibility to cut away further solutions. So, the 0 has to be in the first argument! (The second argument must not be 0 right from the beginning, or the "write unification would not have a detrimental effect.). Here is one such counterexample:
?- pluspo(0, Y, Y).
which gives one correct solution Y = 0, but hides all the other ones! So here we have such an evil red cut!
And contrast it to the unoptimized program which gave infinitely many solutions:
Y = 0 ; Y = s(0) ; Y = s(s(0)) ; Y = s(s(s(0))) ; ...
So, your program is incomplete, and any questions about further optimizing it are thus not relevant. But we can do better, let me restate the actual definition we want to optimize:
plus(0, X, X) :- natural_number(X). plus(s(X), Y, s(Z)) :- plus(X, Y, Z).
In practically all Prolog systems, there is first-argument indexing, which makes the following query determinate:
?- plus(s(0),0,X). X = s(0).
But many systems do not support (full) third argument indexing. Thus we get in SWI, YAP, SICStus:
?- plus(X, Y, 0). X = Y, Y = 0 ; false.
What you probably wanted to write is:
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).
Note the differences to pluspo/3: There are now only tests prior to the cut! All unifications are thereafter.
?- pluso(X, Y, 0). X = Y, Y = 0.
The optimizations so far relied only on investigating the heads of the two clauses. They did not take into account the recursive rule. As such, they can be incorporated into a Prolog compiler without any global analysis. In O'Keefe's terminology, these green cuts might be considered blue cuts. To cite The Craft of Prolog, 3.12:
Blue cuts are there to alert the Prolog system to a determinacy it should have noticed but wouldn't. Blue cuts do not change the visible behavior of the program: all they do is make it feasible.
Green cuts are there to prune away attempted proofs that would succeed or be irrelevant, or would be bound to fail, but you would not expect the Prolog system to be able to tell that.
However, the very point is that these cuts do need some guards to work properly.
Now, you considered another query:
?- pluso(X, s(s(0)), s(s(s(0)))). X = s(0) ; false.
or to put a simpler case:
?- pluso(X, s(0), s(0)). X = 0 ; false.
Here, both heads apply, thus the system is not able to determine determinism. However, we know that there is no solution to a goal plus(X, s^n, s^m) with n > m. So by considering the model of plus/3 we can further avoid choicepoints. I'll be right back after this break:
Better use call_semidet/1!
It gets more and more complex and chances are that optimizations might easily introduce new errors in a program. Also optimized programs are a nightmare to maintain. For practical programming purposes use rather call_semidet/1. It is safe, and will produce a clean error should your assumptions turn out to be false.
Back to business: Here is a further optimization. If Y and Z are identical, the second clause cannot apply:
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).
I (currently) believe that pluso2/3 is the optimal usage of green/blue cuts w.r.t. leftover choicepoints. You asked for a proof. Well, I think that is well beyond an SO answer...
The goal ground(Z) is necessary to ensure the non-termination properties. The goal plus(s(_), Z, Z) does not terminate, that property is preserved by ground(Z). Maybe you think it is a good idea to remove infinite failure branches too? In my experience, this is rather problematic. In particular, if those branches are removed automatically. While at first sight it seems to be a good idea, it makes program development much more brittle: An otherwise benign program change might now disable the optimization and thus "cause" non-termination. But anyway, here we go:
Beyond simple green cuts
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).
Can you find a case where pluso3/3 does not terminate while there are finitely many answers?
这篇关于后继算术和的最佳绿色削减是什么?的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！
