在 CLP(FD) 中生成任意长度的列表时不终止

Question

为什么在 return 预期答案之后，以下内容以 ERROR: Out of global stack 退出？

?- L #>= 0, L #=< 3, length(X, L).

L = 0,
X = [] ;
L = 1,
X = [_G1784] ;
L = 2,
X = [_G1784, _G1787] ;
L = 3,
X = [_G1784, _G1787, _G1790] ;
ERROR: Out of global stack

更新：W.r.t。 @Joan 的回答，我试图理解 为什么 它不会终止，不一定找到会终止的解决方案。我的意思是，如果问题是无限性，那么在贴标签之前它不应该同样产生任何答案，对吧？所以我的问题更多地与产生答案（而不是终止）的机制有关，而不是修复代码。

Answer 1

那是因为当长度为运行时，它仍然只是一个未绑定的变量。直到：

约束的域减少为单个值
未绑定变量与实际值统一
您明确标记了变量

变量将绑定到单个值。

您可以通过以下方式修复示例：

?- L #>= 0, L #=< 3, label([L]), length(X, L).

要看第一点你可以看到：

?- L #>= 1, L #=< 1, length(X, L).

也有效，因为变量被限制为单个值。

Answer 2

问题是 length/2 谓词是坚定的。您可以在 Stack Overflow 中找到一些了解坚定性的帖子，@mat 提出的一个好问题是：Steadfastness: Definition and its relation to logical purity and termination。简而言之，坚定性是谓词最后评估其参数的属性。

在您的示例中，您可以给出约束条件：

L #>= 0, L #=< 3

但在 length(X, L). L 将在最后计算。所以发生的是 length(X, L) 有无限的选择点（它将检查每个列表 X）并且对于每个列表 X 它将评估 L 并且，如果 L 满足约束那么它将 return 你一个答案并且将继续检查导致无限循环的下一个列表。

您可以在跟踪模式下看到以下内容：

  Call: (8) length(_G427, _G438) ? creep
   Exit: (8) length([], 0) ? creep
   Call: (8) integer(0) ? creep
   Exit: (8) integer(0) ? creep
   Call: (8) 0>=0 ? creep
   Exit: (8) 0>=0 ? creep
   Call: (8) integer(0) ? creep
   Exit: (8) integer(0) ? creep
   Call: (8) 3>=0 ? creep
   Exit: (8) 3>=0 ? creep
X = [],
L = 0 ;
   Redo: (8) length(_G427, _G438) ? creep
   Exit: (8) length([_G1110], 1) ? creep
   Call: (8) integer(1) ? creep
   Exit: (8) integer(1) ? creep
   Call: (8) 1>=0 ? creep
   Exit: (8) 1>=0 ? creep
   Call: (8) integer(1) ? creep
   Exit: (8) integer(1) ? creep
   Call: (8) 3>=1 ? creep
   Exit: (8) 3>=1 ? creep
X = [_G1110],
L = 1 ;
   Redo: (8) length([_G1110|_G1111], _G438) ? creep
   Exit: (8) length([_G1110, _G1116], 2) ? creep
   Call: (8) integer(2) ? creep
   Exit: (8) integer(2) ? creep
   Call: (8) 2>=0 ? creep
   Exit: (8) 2>=0 ? creep
   Call: (8) integer(2) ? creep
   Exit: (8) integer(2) ? creep
   Call: (8) 3>=2 ? creep
   Exit: (8) 3>=2 ? creep
X = [_G1110, _G1116],
L = 2 ;
   Redo: (8) length([_G1110, _G1116|_G1117], _G438) ? creep
   Exit: (8) length([_G1110, _G1116, _G1122], 3) ? creep
   Call: (8) integer(3) ? creep
   Exit: (8) integer(3) ? creep
   Call: (8) 3>=0 ? creep
   Exit: (8) 3>=0 ? creep
   Call: (8) integer(3) ? creep
   Exit: (8) integer(3) ? creep
   Call: (8) 3>=3 ? creep
   Exit: (8) 3>=3 ? creep
X = [_G1110, _G1116, _G1122],
L = 3 ;
 Redo: (8) length([_G1110, _G1116, _G1122|_G1123], _G438) ? creep
   Exit: (8) length([_G1110, _G1116, _G1122, _G1128], 4) ? creep
   Call: (8) integer(4) ? creep
   Exit: (8) integer(4) ? creep
   Call: (8) 4>=0 ? creep
   Exit: (8) 4>=0 ? creep
   Call: (8) integer(4) ? creep
   Exit: (8) integer(4) ? creep
   Call: (8) 3>=4 ? creep
   Fail: (8) 3>=4 ? creep

正如您在第一次调用中看到的那样 length([_G1110|_G1111], _G438) 它不会从一开始就计算 L 而是根据第一个参数计算它然后检查约束。

在 CLP(FD) 中生成任意长度的列表时不终止

Non-termination when generating lists of arbitrary length in CLP(FD)

prolog

clpfd