prolog - N未绑定时的“nth0/3”行为

Question

如果我在 SWI Prolog 中键入“nth0”查询，结果是：

?- nth0(N,X,a).
N = 0,
X = [a|_G282] ;
N = 1,
X = [_G281, a|_G285] ;
N = 2,
X = [_G281, _G284, a|_G288] ;
... etc

但是，SWI 手册说：

Errors
  type_error(integer, Index) if Index is not an integer or unbound.

所以，如果我对这段文字的理解是正确的（？），似乎应该触发错误而不是之前的结果。

另外，我想知道考虑到 ISO 标准，哪一种行为是正确的。

（我知道堆栈溢出不允许引用问题，所以，我不会要求提供标准链接，但如果我问：ISO 标准是否公开可用？如果没有，我希望不要违反规则等效的 RFC？）。

score 4 · Accepted Answer

如果我没看错的话，它会说，因为

nth0( ?Index , ?List , ?Elem )

“...如果Index不是整数或unbound。”

在示例中，索引未绑定：

?- nth0(N, L, E).
N = 0,
L = [E|_G1103] ;
N = 1,
L = [_G1102, E|_G1106] ;
N = 2,
L = [_G1102, _G1105, E|_G1109] .

所以你会误读手册吗？

只是为了确保：手册应该被理解为“......如果索引不是（或（一个整数，未绑定））”。当Index未绑定时，它会开始枚举 Index 可以为 0 或更大的有效列表。

score 3 · Accepted Answer

谓词nth0/3不是 ISO Prolog 的一部分，因此没有明确的引用。但是，标准中定义了报告错误的方式和时间。特别是，由于没有充分实例化参数，因此永远不会报告类型错误。SWI 手册中的具体表述有点令人遗憾。它应该阅读为nth0(N, Xs, E)：

N既不是变量也不是整数
— type_error(integer, N).

现在实例化是否会有限制N（在这种情况下不是，但让我们假设它），那么就会出现错误情况：

N是一个变量
—— instantiation_error。

自 1983 年以来，谓词nth0/3一直是 DECsystem 10 库listut（也写成ListUt）的一部分。最初，该定义仅用于N整数。然而，我们现在所拥有的错误还不存在，并且系统只是（并且错误地）因未实例化的变量而失败。

它后来在 1984 年左右被 Quintus Prolog 采用（并更正）。

现在，我们有了一个精细的错误分类，能够捕捉各种错误情况之间的细微语义差异。

更多如何在标准中定义谓词。

2 回答 2