简单的Prolog程序。出现错误：>/2：参数未充分实例化。

Question

我创建了一个Prolog谓词posAt(List1,P,List2)，用于测试List1和List2中位置P的元素是否相等：

posAt([X|Z], 1, [Y|W]) :-
   X = Y.
posAt([Z|X], K, [W|Y]) :-
   K > 1,
   Kr is K - 1,
   posAt(X, Kr, Y).

测试时：

?- posAt([1,2,3], X, [a,2,b]).

我期望得到输出结果X = 2，但实际上我收到了以下错误信息:

错误: >/2：参数未充分实例化

为什么会出现这个错误？

- user1279812

---

一般来说，采纳最佳答案是一个好主意。你可以通过点击答案旁的勾号来完成这个操作。请注意，勾号表示答案被“采纳”了。 - Chetter Hummin

@ChetterHummin的评论中获得3个赞，3年未被采纳的答案。 - gsamaras

Answer 1

一个Prolog谓词是参数之间的关系，您的语句“List1和List2中位置P上的元素相等”显然是一个可能有多个解的示例。

?- posAt([1,2,3],X,[1,5,3,7]).
X = 1.

因此，尽管Sharky的答案清楚地解释了技术错误出现的原因，但需要进行一些小的修正：

posAt([X0|_], Pos, Pos, [X1|_]) :-
    X0 == X1.

现在它按预期工作。

?- posAt([1,2,3],X,[1,5,3,7]).
X = 1 ;
X = 3 ;
false.

编写用于列表处理的简单谓词是非常有价值的学徒实践，也是有效学习该语言的主要途径。如果您倾向于研究可用的库谓词，这里提供一个使用来自库(lists)中nth1/3的版本。

posAt(L0, P, L1) :-
   nth1(P, L0, E),
   nth1(P, L1, E).

这将输出：

?- posAt([1,2,3],X,[1,5,3,7]).
X = 1 ;
X = 3.

尝试理解为什么在这种情况下，SWI-Prolog“顶级”解释器能够推断解的确定性可能很有趣。

- CapelliC

---

+1：感谢您发现我的错误！我也喜欢使用nth1/3技术，不错。 - user206428

Answer 2

这是因为当Prolog计算子目标K > 1时，K仍然是一个未绑定的变量而不是一个数字。标准的Prolog不能（也不会）在这种情况下计算数值范围的真/假值，因为它们不是ground（与像CLP这样的约束求解器相反，后者允许这样做但工作方式不同）。

考虑下面的解决方案:

posAt(L0, Pos, L1) :- 
    posAt(L0, 1, Pos, L1).

posAt([X0|_], Pos, Pos, [X1|_]) :-
    X0 == X1.    
posAt([_|X0s], CurrPos, Pos, [_|X1s]) :-
    NextPos is CurrPos + 1,
    posAt(X0s, NextPos, Pos, X1s).

第一个谓词posAt/3设置了初始条件：将列表的位置设为1，并调用posAt/4来遍历整个列表。 posAt/4的第一个子句是匹配条件：两个列表在同一位置上的元素相等。在这种情况下，当前位置变量与结果Pos一致。

如果以上子句因列表元素X0和X1不相等而失败，则列表位置CurrPos加一，并递归调用posAt/4以处理下一对项。

编辑：删除了posAt/4第一个子句中的错误剪枝（感谢@chac的指正）。

- user206428

---

为了保持[标签：逻辑纯度]，为什么不使用posAt([X|_], Pos, Pos, [X|_])而不是posAt([X0|_], Pos, Pos, [X1|_]) :- X0 == X1.？ - repeat

这主要是一种风格偏好的问题。作为一名工业 Prolog 程序员，我认为这种编码方式使代码稍微更清晰，并且能够与习惯于使用相同或类似样式编码的同事团队合作。此外，为了纯粹而编码有时与效率相矛盾，特别是当你拥有可供使用的剪枝操作符时。 - user206428

Answer 3

（我刚看到这个问题，所以回答晚了...）

我看了这个问题，考虑是否可以提供一个接近原始问题的解决方案。正如已经解释的那样，问题在于关系>需要实例化其参数。实际上，is也是一样。然而，这可以通过重新排序目标来轻松解决：

posAt([X|_], 1, [X|_]).
posAt([_|X], K, [_|Y]) :-
   posAt(X, Kr, Y),
   K is Kr+1,
   K > 1.

这个解决方案是基于两个列表的长度线性运行，只要K是确定的。然而，如果第一个元素在列表中不匹配，就会出现问题，正如答案中所示。

事实上，最后一个元素是多余的，因此等效。

posAt([X|_], 1, [X|_]).
posAt([_|X], K, [_|Y]) :-
   posAt(X, Kr, Y),
   K is Kr+1.

然而，正如@repeat所证明的，这段代码非常慢。这可能是因为代码正在破坏尾递归。

一个逻辑清晰的解决方案将解决这个问题。在这里，我们将使用Peano公理（s/1继承或关系）表示自然数，解决方案将变为

posAt([X|_], zero, [X|_]).
posAt([_|X], s(K), [_|Y]) :-
   posAt(X, K, Y).

然而，这很难计时，因此，一种“hackish”解决方案大致等效。

  posAt([X|_], [a], [X|_]).
  posAt([_|X], [a|L], [_|Y]) :-
      posAt(X, L, Y).

计时这个解决方案会得到以下结果：

N=8000,numlist(1,N,_Zs), length(_LN,N),time(posAt(_Zs,_LN,_Zs)).
 7,999 inferences, 0.001 CPU in 0.001 seconds (100% CPU, 7342035 Lips)
N = 8000

- CAFEBABE

---

s(X) 用于使用列表进行算术运算。 - repeat

不错哦 ;). 从一开始接触Prolog列表时，这就给我留下了深刻的印象。它们基本上是Peano公理的实现，带有一些额外的负载：列表内容。 - CAFEBABE

Answer 4

TL;DR: @CAFEBABE、@CapelliC、@mat和@sharky的答案都存在不足之处！

那么...早先提出的答案到底有哪些不足之处呢？

The text is discussing the efficiency and logical soundness of different code solutions for a certain problem. The code solutions are provided by different users, including @CAFEBABE, @CapelliC, @mat, and @sharky. The text compares the performance of their code in terms of runtime complexity, universal termination, and logical soundness. It concludes that @sharky's code has the best performance in terms of runtime complexity, but it loses logical soundness when used with insufficiently instantiated terms. On the other hand, @CapelliC's and @mat's codes are doing alright in terms of both performance and logical soundness.

---

所以...我们该怎么办呢？为什么不按照这种方法，将@mat和@sharky的代码结合起来呢？

:- use_module(library(clpfd)).

posAt__NEW(L0, Pos, L1) :- 
    posAt__NEW_(L0, 1, Pos, L1).

posAt__NEW_([X|_], Pos, Pos, [X|_]).
posAt__NEW_([_|X0s], CurrPos, Pos, [_|X1s]) :-
    CurrPos #< Pos,
    NextPos #= CurrPos + 1,
    posAt__NEW_(X0s, NextPos, Pos, X1s).

让我们使用posAt__NEW/3重新运行上面的示例查询：

这是Prolog代码和执行结果，无法直接翻译成中文。

好的！最终，我们确定上述第三个查询中使用的目标具有线性复杂度：

?- numlist(1,100,Zs), time((posAt__NEW(Zs,_,_), false)).
% 15,455 次推理，0.004 CPU，0.004 秒（100% CPU，3545396 Lips）
false.
?- numlist(1,1000,Zs), time((posAt__NEW(Zs,_,_), false)).
% 154,955 次推理，0.016 CPU，0.017 秒（98% CPU，9456629 Lips）
false.
?- numlist(1,10000,Zs), time((posAt__NEW(Zs,_,_), false)).
% 1,549,955 次推理，0.098 CPU，0.099 秒（99% CPU，15790369 Lips）
false.
?- numlist(1,100000,Zs), time((posAt__NEW(Zs,_,_), false)).
% 15,499,955 次推理，1.003 CPU，1.007 秒（100% CPU，15446075 Lips）
false.

- repeat

---

有趣的分析。正如我所说，我的主要目标是提供一个接近帖子问题的解决方案。很长一段时间我一直在想为什么我的代码在第一个查询中表现不佳。它应该仍然是输入线性的。它可能会慢，因为它不是尾递归，但这真的是解释吗？。所以现在我想知道发生了什么。 - CAFEBABE

@CAFEBABE。问题的来源是什么？你提出的“解决方案”：“然而，通过重新排序目标可以轻松解决这个问题”。实际上，你解决了一个问题，却引入了另一个问题... - repeat

重点不同。我的陈述是谓词在O(N)中。你通过计时测试声称它不是。我的陈述是一个纯理论的论点，可以在数学上证明。你的是一个纯经验主义的论点。有两个问题出现了：(a) 如果我的代码不是在O(N)中，为什么不是？(b) 真正导致问题的是尾递归吗？ - CAFEBABE

谢谢你的挑战。我已经相应地更新了我的答案。解决方案实际上非常简单，纯粹是逻辑编程。 - CAFEBABE

发现了我之前没注意到的东西。 - CAFEBABE

Answer 5

这类问题的一般解法是约束条件。

使用clpfd进行整数算术运算，可以在所有方向上工作。

:- use_module(library(clpfd)).

posAt([X|_], 1, [X|_]).
posAt([_|X], K, [_|Y]) :-
   K #> 1, 
   Kr #= K - 1,
   posAt(X,Kr,Y).

通过这些简单的更改，您的示例将按预期工作:

?- posAt([1,2,3], X, [a,2,b]).
X = 2 ;
false.

其中，X=2 表示列表 [a,2,b] 中元素 2 的位置是在原列表 [1,2,3] 中的索引值为 2 的位置。

- mat