exception - 为什么 length/2 让我退出全局堆栈？

Question

当我提交查询时:

?- X in 1..2, length(List,X).

返回结果为:

X = 1, List = [_1260];
X = 2, List = [_1260, _1266];
ERROR: Out of global-stack.
ERROR: No room for exception term. Aborting.
% Execution Aborted

我认为发生这种情况是因为 X 没有接地，所以我又运行了 3 个查询来查看 length/2 如何以非实例化变量作为长度:

?- X in inf..sup, length(List,X).
?- length(List,_).
?- length(List,_X).

并且一切正常。因此，如果 X 没有接地，则在达到域的最高值后，length/2 会崩溃。为什么会发生这种情况？它不应该返回 false 吗？

Answer 1

Why is this happening? Shouldn't it return false instead?

不，因为 length/2不知道这些界限，它只是建议值，并且每次卡住约束检查都会拒绝这些值。

length/2 [swi-doc]可以以“建设性”的方式使用。事实上，我们可以生成具有相应长度的列表，例如:

?- length(L, N).
L = [],
N = 0 ;
L = [_2316],
N = 1 ;
L = [_2316, _2322],
N = 2 ;
L = [_2316, _2322, _2328],
N = 3
...

现在您定义了 N 的约束，这意味着如果您设置 N到某个值时，Prolog解释器将检查该值是否在1..2中范围。对于 N > 2 的每个值，因此将会失败。但是length/2当然不理解这个范围。它将不断建议列表及其相应的长度，但每次都会失败。

它相当于:

?- length(L, N), member(N, [1, 2]).
L = [_2304],
N = 1 ;
L = [_2304, _2310],
N = 2 ;
ERROR: Out of global-stack.
ERROR: No room for exception term. Aborting.

这里反向执行此操作更有意义，例如:

?- member(N, [1,2]), length(L, N).
N = 1,
L = [_3372] ;
N = 2,
L = [_3372, _3378].

或者如果这不是一个选项，请尝试 freeze/2 [swi-doc]列表的构建直到 N众所周知。