术语的安全排序

Question

标准术语顺序仅将变量作为句法对象。因此，beside other problems、sort/2 打破了关系定义的常见假设。答案替换既不能保证解决方案，也不能对第二个参数的地面实例进行排序。

?- X = 1, sort([1,X],[1]).
   X = 1.
?-        sort([1,X],[1]).   % generalization fails
false.
?-        sort([1,X],[2,1]).
   X = 2.                    % unsorted list succeeds
?- X = 2, sort([1,X],[2,1]). % answer substitution fails
false.

但是即使我们忽略了声明性问题，我们仍然面临着变量排序仅在创建排序列表期间保持不变的问题。所以根据我们得到的变量的“年龄”

?- _=X+Y, sort([X,Y],[2,1]).
   X = 2, Y = 1.
?- _=Y+X, sort([X,Y],[2,1]).
   Y = 2, X = 1.

而且年龄可能会随着时间而改变，甚至是相对年龄。

我们真的应该受到所有这些古怪行为的保护。

到目前为止，我尝试的是一个安全的定义，它会产生与sort/2 完全相同的类型错误，但是当要排序的列表不接地时会产生实例化错误。只要不发生实例化错误，这个定义确实是完美的。

sort_si(List, Sorted) :-
   sort(List, ISorted),
   ( sort([], [_|Sorted]) ; true ), % just to get the type_error
   (  ground(ISorted)
   -> Sorted = ISorted
   ;  throw(error(instantiation_error, _Imp_def))
   ).

?- sort_si([X,X],S).
caught: error(instantiation_error, _97) % unexpected; expected: S = [X]
?- sort_si([-X,+Y], S).
caught: error(instantiation_error, _97) % unexpected; expected: S = [+Y,-X]
?- sort_si([_,_], []).
caught: error(instantiation_error, _97) % unclear, maybe failure

我的问题是：如何通过减少不必要的实例化错误的数量来改进 ISO Prolog 中的定义？理想情况下，仅当目标 sort(List, Sorted) 的实例具有不同的结果时，才会发生 sort_si(List, Sorted) 的实例化错误。不需要最佳数量的实例化错误。也许在某种程度上可以使用列表ISorted 排序的事实。

而且，Sorted 也可以考虑，因为现在Sorted 将永远不会有未排序的地面列表解决方案。

Answer 1

我的看法是通过ISorted 并检查每对连续术语是否“安全可比”，这意味着没有进一步的实例化会改变它们的顺序。我在comparable/2 谓词中捕捉到了这个想法，具体情况如下：

• 如果两个参数是变量，那么它们必须是相同的变量才能进行比较。
• 如果这两个论点是有根据的，那么它们是可比较的。 （不确定这种情况是否必要，除了缩短手动遍历术语的方法。）
• 否则，这两个参数必须是非变量，并且其中至少一个包含变量。我们需要进一步比较这些术语，但前提是它们都是具有相同函子和相同数量参数的复杂术语。在这种情况下，第一个论点需要具有可比性。然后，仅当第一个不区分这两个术语时，以下几个才需要可比较，这发生在第一个参数相等时 (==)。

当ISorted 不能与Sorted 统一时，我在主谓词中添加了一个测试失败，其想法是sort_si/2 只会在sort/2 成功时与sort/2 不同“不正确”，但不是在失败时，但我不确定这一点。

sort_si(List, Sorted) :-
   sort(List, ISorted),
   ( sort([], [_|Sorted]) ; true ), % just to get the type_error
   ( Sorted \= ISorted % just to fail whenever sort/2 would fail
   -> fail
   ;  pairwise_comparable(ISorted)
   -> Sorted = ISorted
   ;  throw(error(instantiation_error, _Imp_def))
   ).


pairwise_comparable([]).
pairwise_comparable([_]).
pairwise_comparable([X1,X2|Xs]):-
   comparable(X1,X2),
   pairwise_comparable([X2|Xs]).

comparable(X1,X2):-
   var(X1),
   var(X2),
   X1==X2.
comparable(X1,X2):-
   ground(X1),
   ground(X2).
comparable(X1,X2):-
   nonvar(X1),
   nonvar(X2),
   functor(X1,F1,A1),
   functor(X2,F2,A2),
   (  F1\=F2
   -> true
   ;  A1\=A2
   -> true
   ;  X1=..[_|Xs1],
      X2=..[_|Xs2],
      comparable_args(Xs1,Xs2)
   ).

comparable_args([],[]).
comparable_args([X1|Xs1],[X2|Xs2]):-
   comparable(X1, X2),
   (  X1\==X2
   -> true
   ;  comparable_args(Xs1,Xs2)
   ).