安全的术语排序。

Question

安全的术语排序。

3

标准术语顺序仅将变量视为句法对象。因此，除了其他问题之外，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 相同类型的错误，但当要排序的列表不是ground时会产生实例化错误。只要没有出现实例化错误，这个定义就是完美的。

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的事实。

另外，由于现在不存在未排序的ground list解决方案，因此Sorted可以被认为是已排序的。

- false

1个回答

网页内容由stack overflow 提供, 点击上面的

可以查看英文原文，
原文链接

- jnmonette · Accepted Answer

我的想法是通过 ISorted 并检查每对连续术语是否“可比较”，这意味着没有进一步的实例化会改变它们的顺序，来进行排序。我在 comparable/2 谓词中用以下情况捕获了这个思想：

如果两个参数都是变量，则它们必须是相同的变量才能进行比较。
如果两个参数都是 ground ，则它们是可比较的。(不确定这种情况是否必要，除了快捷手动遍历术语之外)
否则，两个参数必须都是非变量，并且其中至少一个包含一个变量。我们需要进一步比较术语，但只有当它们都是具有相同函数符和相同数量参数的复杂术语时才需要。在这种情况下，第一个参数需要是可比较的。然后，如果第一个参数不区分两个术语 (即第一个参数等于(==))，则仅需要比较后续的术语。

我在主谓语中添加了一个测试，以便在 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)
   ).