3

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

  1. cTI 报告 sum(A,B,C)terminates_if b(A);b(C).以下规则：
sum(0, Y, Y).
sum(s(X), Y, s(Z)) :-
  sum(X, Y, Z).
  1. cTI 报告 sum(A,B,C)terminates_if b(A),b(B);b(C).以下规则（X并Y已交换）：
sum(0, Y, Y).
sum(s(X), Y, s(Z)) :-
  sum(Y, X, Z).

sum(X, 0, Z).例如，可以通过使用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(0))))
;  …

它为第二条规则返回以下解决方案：

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

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

4

1 回答 1

3

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

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

（以上输出来自 Scryer，可读性更好）

在查看具体定义之前，请考虑我们期望X和的一组解决方案Z。两者应该相同，并且它们应该描述所有自然 s(X)-numbers 0, s(0), s(s(0))... 所以我们有无限多的解决方案。我们，拥有有限 Prolog 系统的有限存在者，如何描述无限多的解决方案？好吧，我们可以试一试，然后开始1。这就是我们在sumA. 这里的好处是，每个答案实际上都是一个解决方案（也就是说，没有剩余的变量2）。可惜程序没有终止（普遍）。至少它以公平的方式产生所有解决方案。等待足够长的时间，也是您最喜欢的解决方案3会出现。

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

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

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

两者都是正确的sumA。只要我们能够将我们的数字与其他术语区分开来（这大致对应于一个类型良好的程序）sumB。sumB

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

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

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


2）准确地说，没有剩余约束。


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

于 2021-08-04T18:09:10.390 回答