应该在定义加法的规则中交换第一个和第二个参数吗? [英] Should the first and second arguments be swapped in a rule defining addition?

问题描述

Prolog 中有两种可能的加法规则，根据 cTI 具有不同的终止属性:

1. cTI 报告 sum(A,B,C)terminates_if b(A);b(C). 对于以下规则:

sum(0, Y, Y).总和(s(X), Y, s(Z)) :-总和(X，Y，Z).

2. cTI 报告 sum(A,B,C)terminates_if b(A),b(B);b(C). 对于以下规则(X 和 Y 交换):

sum(0, Y, Y).总和(s(X), Y, s(Z)) :-总和(Y，X，Z).

例如可以通过使用 sum(X, 0, Z). 来观察差异"nofollow noreferrer">SWISH，Prolog 的在线 SWI-Prolog 实现.

它返回第一条规则的以下解决方案:

?- sum(X, 0, Z).X = Z，Z = 0;X = Z, Z = s(0);X = Z, Z = s(s(0));X = Z, Z = s(s(s(0)));X = Z, Z = s(s(s(s(s(0))));…

它返回第二条规则的以下解决方案:

?- sum(X, 0, Z).X = Z，Z = 0;X = Z, Z = s(_1302);错误的.

这两条规则哪一条是正确的?

解决方案

在讨论同一个程序的不同版本时，重命名这些版本以便它们可以共存于同一个程序中会很有帮助:

sumA(0, Y, Y).sumA(s(X), Y, s(Z)) :- sumA(X, Y, Z).sumB(0, Y, Y).sumB(s(X), Y, s(Z)) :- sumB(Y, X, Z).?- sumA(X, 0, Z).X = 0，Z = 0;X = s(0), Z = s(0);X = s(s(0)), Z = s(s(0));X = s(s(s(s(0))), Z = s(s(s(s(0)));...?- sumB(X, 0, Z).X = 0，Z = 0;X = s(_A)，Z = s(_A).

(以上输出来自 Scryer，可读性更好)

在查看具体定义之前，先想一想我们对 X 和 Z 期望的解决方案集.两者应该相同，并且它们应该描述所有自然的 s(X)-numbers 0, s(0), s(s(0)) ... 所以我们有无穷多个解.我们，有限的生命体和有限的 Prolog 系统，如何描述无限多的解?好吧，我们可以尝试一下，然后开始¹.这就是我们在 sumA 中看到的.这里的好处是，每个答案实际上都是一个解决方案(也就是说，没有剩余的变量²).只是可惜程序没有终止(普遍).至少它以公平的方式产生所有解决方案.等待足够长的时间，您最喜欢的解决方案³就会出现.

在 sumB 中，以完全不同的方式枚举了无限自然数集.首先，我们得到 0 的解，然后我们得到一个 答案，其中包括所有其他 ≥ 1 的数字.所以我们将这个无限集压缩成一个变量！这就是逻辑变量的力量.当然，我们在这里付出了很小的代价，现在我们实际上也包括了 s(_A) 的参数中的所有内容.一切，包括s(nothing).

?- Z = s(nothing), sumA(Z, 0, Z).错误的.?- Z = s(nothing), sumB(Z, 0, Z).Z = s(什么都没有).

<块引用>

这两条规则哪一条是正确的?

sumA 和 sumB 都是正确的.并且 sumB 只要我们能将我们的数字与其他术语区分开来(大致相当于一个类型良好的程序).

但是哪个更可取?这一切都取决于.通常谓词将在某些上下文中使用.也许后续目标只有在其中一个论点成立时才会终止.在这种情况下，sumA 可能更可取.如果没有进一步的目标，那么 sumB 总是可取的.这一切都取决于一点.

最重要的是，一些无穷大的解可以优雅地包含在逻辑变量中，从而提高终止属性.对于更复杂的情况，这还不够，但会为这些变量附加约束.

---

1) 如果我们得到 resource_error(memory) 也不要难过，它只是一个有限系统.

2) 准确地说没有残差约束.

3) 我最喜欢的数字是 7^7^7 和 9^9^9.对于当前的实现，这将需要一些时间和空间.

There are two possible rules for addition in Prolog, with different termination properties according to cTI:

1. cTI reports sum(A,B,C)terminates_if b(A);b(C). for the following rule:

sum(0, Y, Y).
sum(s(X), Y, s(Z)) :-
  sum(X, Y, Z).

2. cTI reports sum(A,B,C)terminates_if b(A),b(B);b(C). for the following rule (X and Y are swapped):

sum(0, Y, Y).
sum(s(X), Y, s(Z)) :-
  sum(Y, X, Z).

The difference can be observed for instance by executing the query sum(X, 0, Z). with SWISH, the online SWI-Prolog implementation of Prolog.

It returns the following solutions for the first rule:

?- sum(X, 0, Z).
   X = Z, Z = 0
;  X = Z, Z = s(0)
;  X = Z, Z = s(s(0))
;  X = Z, Z = s(s(s(0)))
;  X = Z, Z = s(s(s(s(0))))
;  …

And it returns the following solutions for the second rule:

?- sum(X, 0, Z).
   X = Z, Z = 0
;  X = Z, Z = s(_1302)
;  false.

Which of these two rules is correct?

解决方案

When discussing various versions of the same program, it helps a lot to rename those versions such that they can cohabit in the same program:

sumA(0, Y, Y).
sumA(s(X), Y, s(Z)) :- sumA(X, Y, Z).

sumB(0, Y, Y).
sumB(s(X), Y, s(Z)) :- sumB(Y, X, Z).


?- sumA(X, 0, Z).
   X = 0, Z = 0
;  X = s(0), Z = s(0)
;  X = s(s(0)), Z = s(s(0))
;  X = s(s(s(0))), Z = s(s(s(0)))
;  ...
?- sumB(X, 0, Z).
   X = 0, Z = 0
;  X = s(_A), Z = s(_A).

(Above output is from Scryer, which is better readable)

Before looking at the concrete definitions, think of the set of solutions that we expect for X and Z. Both should be the same, and they should describe all natural s(X)-numbers 0, s(0), s(s(0)) ... So we have infinitely many solutions. How shall we, finite beings with our finite Prolog systems, describe infinitely many solutions? Well, we can give it a try and just start¹. That's what we see in sumA. What is nice here, is that each and every answer is actually a solution (that is, there are no variables remaining²). Just a pity that the program does not terminate (universally). At least it produces all solutions in a fair manner. Wait long enough and also your favorite solution³ will appear.

In sumB that infinite set of natural numbers is enumerated in a quite different manner. First, we get a solution for 0 and then we get a single answer which includes all other numbers ≥ 1. So we have compressed this infinite set into a single variable! That's the power of logic variables. Of course, we paid a tiny price here, for now we also include really everything in the argument of s(_A). Everything, including s(nothing).

?- Z = s(nothing), sumA(Z, 0, Z).
false.
?- Z = s(nothing), sumB(Z, 0, Z).
   Z = s(nothing).

Which of these two rules is correct?

Both sumA and sumB are correct. And sumB as long as we can distinguish our numbers from other terms (that's what roughly corresponds to a well typed program).

But which one is preferable? It all depends. Usually the predicate will be used in some context. Maybe a subsequent goal will only terminate if one of its arguments is ground. In this case, sumA may be preferable. If there is no further goal then sumB is always preferable. It all depends a bit.

What is most important to see is that some of the infinities of solutions can be elegantly subsumed with logic variables thereby improving the termination property. For more complex situations this will not be enough but then constraints will be attached to those variables.

---

1) And don't be upset if we get a resource_error(memory), it's just a finite system.

2) And no residual constraints to be precise.

3) My favorite numbers are 7^7^7 and 9^9^9. With current implementations this will take some time and space.

这篇关于应该在定义加法的规则中交换第一个和第二个参数吗?的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！