prolog - 术语的安全排序

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_si(List, Sorted) 的实例化错误仅在存在具有不同结果的目标 sort(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)
   ).