爲什麼不是這個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接種如何，以便它可以算目前比較的元素的索引。