在序言中制定自然数规则的正确方法是什么？

Question

我想我在理解序言时还有更大的问题，但是由于我无法完全表述，所以我只关注单个问题

我想创建一个规则natural(X)，如果X为1,2,3,4，...，则为true。更重要的是，我都希望：natural(5)为true 和 natural(X)输出X=1; X=2; ...

---

所以，我解释规则如下（伪）：

natural(1) must be true
natural(X) is true if natural(X-1) is true

或就序言而言：

natural(1).
natural(X) :- natural(X-1).

但是我遇到了问题-如果尝试natural(5)，则会得到无限递归调试器说程序评估：

natural(5)
 natural(5-1)
  natural(5-1-1)
   natural(5-1-1-1)
    natural(5-1-1-1-1)
     natural(5-1-1-1-1-1)
      natural(5-1-1-1-1-1-1)
...

---

我想问题是X-1没有得到评估？让我们尝试解决该问题：

natural(1).
natural(X) :-
  Y is X-1,
  natural(Y).

现在，natural(5)可以正常工作但是，如果我使用natural(X)，则会得到X=1; Exception: Arguments not sufficiently instantiated (Y is X-1)

---

好吧，我想问题是我们试图评估可能还没有价值的东西如果尝试使用Y = X-1，我们将回到第一个问题。 Y == X-1返回false

我发现唯一可行的解​​决方案是切换行和定义顺序：

natural(1).
natural(X) :-
  natural(Y),
  X is Y+1.

将最后一行更改为=会得到“ + 1 + 1 + 1 ...”结果。 ==只是失败。

此解决方案在生成X=1; X=2; ...时效果很好，但是当我将其用作检查（natural(5)）时，它会显示为“ 0，（0,1），（0,1,2），（0,1， 2,3），...“命令。是的，我得到了正确的结果，但是那条路很长，而不是我的想象。如果在以前的解决方案中没有看到检查natural（5）的更快方法，我将在这里停止。

---

所以，我错过了哪种更好的创建此规则的方法？

[我猜一种方法是将“ true / false”查询与生成器查询分开...但是有没有一种方法可以使其“可能评估的话进行评估”，即，将hass变量与only-constants分开？ var(X-1)某种程度上是假的...

Answer 1

通过使用succ/2，通常可以大大改善自然交易。如您所知，is/2是Prolog评估算术表达式的[[必需，但它具有单个实例化模式：-Number is +Expr。没有限制，拥有一个完全开放的模式（例如?Number is ?Expr）将是完全不明智的。另一方面，succ/2具有两种模式：succ(+Pred, -Succ)和succ(-Pred, +Succ)。举例来说：succ(X, 3)统一X = 2，succ(2, X)统一X =3。尽管succ(X, Y)仍然是错误。但是，您可以使用natural/1构建succ/2的解决方案，但要注意：

natural(1).
natural(X) :- natural(X0), succ(X0, X).

这可以同时使用两种方法，但是有一个令人讨厌的问题：

?- natural(X).
X = 1 ;
X = 2 ;
X = 3 ;
....

?- natural(5).
true ;
^CAction (h for help) ? abort

是的，如果在提供值后要求第二个结果，则会出现无限循环。 Prolog尝试找出是否5再出现一次
after

5。避免问题的简单解决方案是使用between/3：

natural(X) :- between(1, inf, X).

?- natural(X).
X = 1 ;
X = 2 ;
X = 3 ;
...

?- natural(5).
true.

无循环。这将是我的首选解决方案。

除了var/1和nonvar/1之外，还有ground/1，它可以区分具有变量的项和不具有变量的项。您可以使用它来区分（一侧）5、3-1等与另一侧的X，X-1。以我的经验，将这样的情况分开通常会导致眼泪和向后正确性的麻烦，但在极端情况下，这是有必要的。

此时，您可能对Prolog的逻辑感到有些不适。标准系统的算法令人失望。但是clpfd更加强大和灵活，许多人建议您首先学习它，因为它更擅长生成解决方案（is/2确实无法生成，但可以使用clpfd进行标记）。以我的经验，succ/2足够接近Peano算术，以至于整数混乱通常是可以的，但是对于任何严重的问题，您将希望使用clpfd。