prolog - min_member/2的违反直觉的行为

Question

min_member(-Min, +List)

当Min是标准条款中的最小成员时为True。如果列表为空，则失败。

?- min_member(3, [1,2,X]).
X = 3.

当然，这种解释是变量按照标准的术语顺序排在所有其他术语之前，并且使用统一。但是，报告的解决方案感觉有点不对劲。

怎么有道理呢？我应该如何解释这个解决方案？

编辑:

阻止 min_member/2成功使用此解决方案的一种方法是如下更改标准库(SWI-Prolog) implementation:

xmin_member(Min, [H|T]) :-
    xmin_member_(T, H, Min).

xmin_member_([], Min0, Min) :-
    (   var(Min0), nonvar(Min)
    ->  fail
    ;   Min = Min0
    ).
xmin_member_([H|T], Min0, Min) :-
    (   H @>= Min0 
    ->  xmin_member_(T, Min0, Min)
    ;   xmin_member_(T, H, Min)
    ).

失败而不是引发实例化错误(如果我正确理解的话，@ mat在他的答案中提出的建议)背后的原因是，这是一个明确的问题:

“当X是自由变量时，3是 [1,2,X]的最小成员吗？”

对此的答案(至少对我来说)是明确的“否”，而不是“我不能说真的”。

这是与 sort/2相同的行为类别:

?- sort([A,B,C], [3,1,2]).
A = 3,
B = 1,
C = 2.

同样的技巧也适用:

?- min_member(3, [1,2,A,B]).
A = 3.

?- var(B), min_member(3, [1,2,A,B]).
B = 3.

Answer 1

这是许多(全部？)谓词的共同属性，取决于条件的标准顺序，而两个条件之间的顺序在合并后可以更改。基准是下面的连接词，也不能还原:

?- X @< 2, X = 3.
X = 3.

大多数使用 -Value批注作为参数的谓词表示 pred(Value)是相同的
作为 pred(Var), Value = Var。这是另一个示例:

?- sort([2,X], [3,2]).
X = 3.

仅当输入为地面时，这些谓词才表示干净关系。尽管由于用户可以意识到自己不应该进一步实例化任何排序的术语，但是因为可以将它们与变量有效地结合使用，所以要求将输入置于地面是太多了。从这个意义上说，我不同意@mat。我确实同意，约束条件一定可以使其中某些关系听起来很合理。