如何防止Prolog无限制地检查不可能的解决方案？

Question

假设以下程序：

nat(0).
nat(s(N)) :- nat(N).

/* 0+b=b */
plus(0,B,B) :- nat(B).
/* (a+1)+b = c iff a+(b+1)=c */
plus(s(A),B,C) :- plus(A,s(B),C).

它非常适用于两个数字求和，但当我尝试进行以下类型的查询时：

plus(Z,Z,s(0)).

在明显没有解决方案的情况下（即Z>s(0)），它继续搜索Z的可能值。

我熟悉!运算符，我的直觉告诉我解决方案与它有关，只是我不确定如何在这种情况下使用它。

- yurib

---

@false 感谢您的标记，我不知道这个概念有一个正式的名称。 - yurib

Answer 1

！/0 并不是解决此类问题的好方法。通常会导致更一般的查询丢失有效的解决方案。

相反，考虑使用有限域约束，在这种情况下可以完美地工作：

?- use_module(library(clpfd)).
true.

?- Z + Z #= 0.
Z = 0.

?- Z + Z #= 0, Z #> 0.
false.

编辑：根据要求，以下是没有使用CLP(FD)的可能解决方案：

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

- mat

---

我可能应该明确提到，我正在寻找一种不使用任何库并且使用后继算术的解决方案。 - yurib

Answer 2

您在这里关心的是了解特定程序的精确终止属性。Prolog与其他编程语言非常不同，因为它具有相对复杂的执行机制。特别是回溯与“正常解析”相互交织，然后与统一组合。

理解原始程序问题的最简单方法是考虑以下失败切片（请参见链接获取其他示例）：

plus(0,B,B) :- false, nat(B).
plus(s(A),B,C) :- plus(A,s(B),C), false.

如果这个小程序无法终止，那么您的原始程序也将无法终止。因此，我们首先可以考虑这个程序何时无法终止。

考虑第三个参数：只是传递了一个名为C的变量。在这个片段中，没有人关心它的值。因此，第三个参数将不会对终止产生任何影响！

更糟糕的是，头部中的第二个参数只是一个自由变量B，因此，该参数永远不会影响此片段是否终止。

因此：如果您希望此片段终止，第一个参数必须是已知的。否则程序将循环。 您还可以使用终止推理器来查看此内容以获得终止条件：

plus(A,B,C)terminates_if b(A),b(B);b(A),b(C).

最好的方法似乎是重新构思您的程序。给您以下终止条件：

plus(A,B,C)terminates_if b(A),b(B);b(C).

在Prolog中，我们通常喜欢进一步概括程序，接受一些意外的解决方案，同时改进其终止条件以获得更好的条件。

plus(A,B,C)terminates_if b(A);b(C).

然而，这个最新版本现在允许一些不太可接受的解决方案。例如：plus(0, nonnumber, nonnumnber)现在成功了，但你可能希望它失败。

当然，你也可以尝试一些关于剪枝的实验，但要注意，使用剪枝非常容易出错。至少你应该将其与适当的测试结合使用，这通常会抵消“效率收益”。

- false

Answer 3

我意识到我的方法不正确，我需要的不是一个剪切符号（!），而是一组不同的规则，通过“分解”Z直到它达到0来找到X和Y。由于只有在减少Z时才会增加X和Y，它们永远不会被赋予不可能的值。

plus(0,0,0).
plus(s(A),B,s(C)) :- plus(A,B,C).
plus(0,s(B),s(C)) :- plus(0,B,C).

- yurib

---

@mat 你说得没错，将它作为答案提交上来，我会接受的。 - yurib