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

Question

这个问题已经有答案了:

Using a constrained variable with `length/2` (4 个回答)

已关闭 6 年前。

为什么以下退出时显示 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

问题在于 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 满足约束，那么它将返回您将得到答案，并将继续检查下一个导致无限循环的列表。

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

  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，而是根据第一个参数计算它，然后检查限制条件。