为什么不是这个prolog函数返回所有有效值？ （参数没有充分实例化）

Question

我正在研究一个我在网上找到的例子，试图理解Prolog返回的内容。对于这个代码在这里...

element_at(X,[X|_],1). 
element_at(X,[_|L],K) :- 
    K > 1, 
    K1 is K - 1, 
    element_at(X,L,K1). 

这工作...

?- element_at(x, [a,b,c,x,x,d,e], Pos). 

但这并不...我预计代码返回有效值列表，例如.. 。

?- element_at(x, [a,b,c,x,x,d,e], Pos). 
Pos = 4; 
Pos = 5; 

而是我得到ERROR: >/2: Arguments are not sufficiently instantiated

什么修改我得到它返回有效数值F或Pos？

Answer 1

凭借在SWI-Prolog中有declarative arithmetic帮助：

:- [library(clpfd)]. 

element_at(X,[X|_],1). 
element_at(X,[_|L],K) :- 
    K #> 1, 
    K1 #= K - 1, 
    element_at(X,L,K1). 

我们得到预期的，声明的行为：

?- element_at(x, [a,b,c,x,x,d,e], Pos). 
Pos = 4 ; 
Pos = 5 ; 
false. 

Answer 2

如果你看看你的代码，你会发现当x是列表的第一个元素时，K被初始化。 如果不是这种情况，K就会增加。如果在您调用谓词时x不是列表的第一个元素，则K没有任何价值！

Answer 3

它不会这样工作，因为为了使Prolog中的算术可行，您没有将正整数定义为0的后继因此，对于算术比较，您需要双方都是有效的算术表达式，而对于SWI中可用的succ(N,N1)谓词（例如N1是N + 1），您至少需要将两个参数中的一个参数实例化。

SWI的谓词nth0/3和nth1/3它们完全符合您试图实现的要求（参数顺序有点不同）。它是在Prolog中实现的，它执行的是它看起来N是一个变量还是一个正整数，然后调用生成nth（返回所有回溯的索引），或者调用一个确定性的nth来选择第N个元素。

这是在SWI-Prolog的源文件中从lists.pl复制的！

nth0(Index, List, Elem) :- 
    ( integer(Index) 
    -> nth0_det(Index, List, Elem)  % take nth deterministically 
    ; var(Index) 
    -> List = [H|T], 
     nth_gen(T, Elem, H, 0, Index) % match 
    ; must_be(integer, Index) 
    ). 

注nth_gen需要与0接种如何，以便它可以算目前比较的元素的索引。