后续算术总和的最佳绿线是什么? [英] What are the optimal green cuts for successor arithmetics sum?

问题描述

要在Prolog中使用绿色分割，我尝试将其添加到后续算术中sum的标准定义中(请参阅中的谓词plus该查询的SLD树?).这个想法是通过消除所有无用的回溯(即，没有... ; false)来尽可能清理"输出，同时在参数实例化的所有可能组合下保持相同的行为-所有实例化，一个/两个/三个完全未实例化，以及所有变体，包括部分实例化的args.

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.

这是我在尝试尽可能接近这一理想时所做的事情(我承认false对在append/3 中插入绿色切口作为源):

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

在SWI下，这似乎适用于所有查询，但形状为?- 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:

• 我们如何证明上述削减是(或不是)绿色?
• 我们能否比上述程序做得更好，并通过添加其他一些绿色削减措施来消除最后的回溯?
• 如果是，怎么办?

推荐答案

首先是一个小问题:plus/3的通用定义交换了第一参数和第二参数，从而可以利用第一参数索引.参见《序言艺术》程序3.3.您的上一篇文章中也应对此进行更改.我将交换的定义定义为plusp/3，将优化的定义定义为pluspo/3.因此，给定

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

我发现以下情况:

pluspo(X, Y, X) :- (...... -> ! ; ... ), ...

pluspo(X, Y, X) :- (...... -> ! ; ... ), ...

因此，让我们构造一个反例:为了以红色的方式进行剪切，"write unification"必须将其实际防护Y == 0设置为true.这意味着构造的目标必须以某种方式包含常数0.只有两种可能性要考虑.第一个或第三个参数.最后一个参数为零表示我们最多只能有一个解决方案，因此不可能删除更多的解决方案.因此，0必须在第一个参数中！ (第二个参数必须从一开始就不能为0，否则写统一"不会有不利影响.).这是一个这样的反例:

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

给出了一个正确的解决方案Y = 0，但隐藏了所有其他解决方案！所以在这里，我们有这么一个邪恶的红色切面！ 并将其与未优化的程序进行对比，该程序提供了许多解决方案:

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

几乎在所有Prolog系统中，都存在第一参数索引，这使得确定以下查询成为可能:

In practically all Prolog systems, there is first-argument indexing, which makes the following query determinate:

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

但是许多系统不支持(完整)第三个参数索引.因此，我们进入了SWI，YAP，SICStus:

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.

您可能想写的是:

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的区别:现在只有剪切之前的测试！此后所有统一.

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.

到目前为止，优化仅依赖于调查这两个子句的开头.他们没有考虑递归规则.这样，它们可以集成到Prolog编译器中，而无需任何全局分析.用O'Keefe的术语，这些绿色切口可能被认为是蓝色切口.引用 Prolog的手法，3.12:

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 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 切口可以警告Prolog系统确定性，应该但不会.剪裁不会改变程序的可见行为:它们所做的只是使其变得可行.

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.

绿色剪切可以修剪尝试的成功或不相关或必将失败的证据，但是您不希望Prolog系统能够证明这一点.

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.

在这里，两个脑袋都适用，因此系统无法确定确定性.但是，我们知道对于n>的目标plus(X, s^n, s^m)没有解决方案. m.因此，通过考虑plus/3的模型，我们可以进一步避免选择点.休息后我会马上回来:

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:

它变得越来越复杂，优化可能很容易在程序中引入新的错误.优化的程序也是要维护的噩梦.出于实际编程目的，请使用 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.

重新开始:这是进一步的优化.如果Y和Z相同，则第二个子句不适用:

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

我(目前)认为pluso2/3是绿色/蓝色切割的最佳用法.剩余的选择点.您要求提供证明.好吧，我认为这远远超出了答案……

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

目标ground(Z)对于确保非终止特性是必不可少的.目标plus(s(_), Z, Z)不会终止，该属性由ground(Z)保留.也许您认为删除无限失败分支也是一个好主意?以我的经验，这是很成问题的.特别是，如果那些分支被自动删除.乍一看，这似乎是一个好主意，但它会使程序开发变得更加脆弱:原本良性的程序更改现在可能会禁用优化，从而导致"优化.不终止.但是无论如何，我们开始:

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:

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没有终止的情况吗?

Can you find a case where pluso3/3 does not terminate while there are finitely many answers?

这篇关于后续算术总和的最佳绿线是什么?的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！