sorting - 如何在 ISO Prolog 中定义（和命名）相应的安全术语比较谓词？

Question

标准术语顺序（ISO/IEC 13211-1 7.2 术语顺序）定义在所有术语上——包括变量。虽然这有很好的用途——想想setof/3. 8.4 词条比较特点：

8.4 术语比较

8.4.1 (@=<)/2, (==)/2, (\==)/2, (@<)/2, (@>)/2, (@>=)/2。
8.4.2 比较/3。
8.4.3 排序/2。
8.4.4 键排序/2。

举个例子，考虑：

?- X @< a.
true.

这成功了，因为

7.2 期限顺序

排序term_precedes
(3.181) 定义 了 term是否在Xterm 之前Y。

如果X和Y是相同的术语，那么X term_precedes Y
和Y term_precedes X都是假的。

如果X和Y有不同的类型：Xterm_precedes Yiff 的
类型按以下顺序在类型之前：X先于先于先于 先于。Y
variablefloating pointinteger
atomcompound

注意——测试术语顺序的内置谓词
在 8.4 中定义。
...

因此所有变量都小于a。但是一旦X实例化：

?- X @< a, X = a.
X = a.

结果无效。

所以这就是问题所在。为了克服这个问题，可以使用约束，或者只坚持核心行为，从而产生一个instantiation_error.

7.12.2 错误分类

错误按以下形式分类Error_term：

a) 当参数或其组件之一是变量并且需要
实例化参数或组件时，应存在实例化错误。它有
形式instantiation_error。

通过这种方式，只要不发生实例化错误，我们就可以确定结果是明确定义的。

对于(\==)/2，已经存在dif/2使用约束或iso_dif/2产生干净实例化错误的情况。

iso_dif(X, Y) :-
   X \== Y,
   ( X \= Y -> true
   ; throw(error(instantiation_error,iso_dif/2))
   ).

那么我的问题是：如何在ISO Prolog中定义（和命名）相应的安全术语比较谓词？理想情况下，没有任何明确的术语遍历。也许要澄清一下：上面iso_dif/2没有使用任何明确的术语遍历。两者(\==)/2和在内部遍历该术语，但是与使用or(\=)/2的显式遍历相比，这样做的开销非常低。(=..)/2functor/3, arg/3

Answer 1

iso_dif/2实现起来比比较简单得多：

• 内置\=运算符可用
• 你现在确切地提供什么论据\=

定义

根据您的评论，安全比较意味着如果两个子项中的变量都被实例化，则顺序不会改变。如果我们命名比较lt，我们有例如：

• lt(a(X), b(Y)): 总是适用于所有 X 和 Y，因为a @< b
• lt(a(X), a(Y)): 我们不确定：intanciation_error
• lt(a(X), a(X)): 总是失败，因为 X @< X 失败

正如评论中所说，如果在并行遍历这两个术语时，第一个（可能）有区别的术语对包含：

• 两个不相同的变量 ( lt(X,Y))
• 一个变量和一个非变量 ( lt(X,a), 或lt(10,Y))

但首先，让我们回顾一下您不想使用的可能方法：

• 定义一个显式的术语遍历比较函数。出于性能原因，我知道您不希望这样做，但仍然是最直接的方法。无论如何，我建议您这样做，以便您有一个参考实现来与其他方法进行比较。

• 使用约束进行延迟比较：我不知道如何使用 ISO Prolog 进行比较，但是使用例如 ECLiPSe，我会暂停对一组未实例化变量（使用term_variables/2）的实际比较，直到没有更多变量为止。之前，我也建议使用coroutine/0谓词，但我忽略了它不会影响@<运算符（仅<）的事实。

  这种方法不能解决与您描述的完全相同的问题，但它非常接近。一个优点是，如果赋予变量的最终值满足比较，它不会抛出异常，而lt在事先不知道时抛出异常。

显式项遍历（参考实现）

lt这是 .的安全版本的显式术语遍历方法的实现@<。请查看它以检查这是否是您所期望的。我可能错过了一些案例。我不确定这是否符合 ISO Prolog，但如果您愿意，也可以修复。

lt(X,Y) :- X == Y,!,
    fail.

lt(X,Y) :- (var(X);var(Y)),!,
    throw(error(instanciation_error)).

lt(X,Y) :- atomic(X),atomic(Y),!,
    X @< Y.

lt([XH|XT],[YH|YT]) :- !,
    (XH == YH ->
         lt(XT,YT)
     ;   lt(XH,YH)).

lt(X,Y) :-
    functor(X,_,XA),
    functor(Y,_,YA),
    (XA == YA ->
       X =.. XL,
       Y =.. YL,
       lt(XL,YL)
    ;  XA < YA).

（编辑：考虑到 Tudor Berariu 的评论：（i）缺少 var/var 错误案例，（ii）首先按 arity 排序；此外，修复（i）允许我删除subsumes_term列表。谢谢。）

隐式术语遍历（不工作）

这是我在不破坏术语的情况下达到相同效果的尝试。

every([],_).
every([X|L],X) :-
    every(L,X).

lt(X,Y) :-
    copy_term(X,X2),
    copy_term(Y,Y2),
    term_variables(X2,VX),
    term_variables(Y2,VY),
    every(VX,1),
    every(VY,0),
    (X @< Y ->
         (X2 @< Y2 ->
              true
          ;   throw(error(instanciation_error)))
     ;   (X2 @< Y2 ->
              throw(error(instanciation_error))
          ;   false)).

基本原理

假设X @< Y成功了。我们要检查关系是否不依赖于一些未初始化的变量。X2因此，我生成了和Y2的相应副本X，Y其中所有变量都被实例化：

• 在X2中，变量统一为 1。
• 在Y2中，变量统一为 0。

所以，如果关系X2 @< Y2仍然成立，我们知道我们不依赖变量之间的标准术语排序。否则，我们抛出一个异常，因为这意味着1 @< 0以前没有发生的关系使关系失败。

缺点

（基于OP的评论）

• lt(X+a,X+b)应该成功但产生错误。

  乍一看，人们可能认为统一出现在两个术语中的具有相同值的变量，例如val，可能会解决这种情况。但是，X在比较条款中可能会出现其他情况，从而导致错误判断。

• lt(X,3)应该产生错误但成功。

  为了解决这种情况，应该统一X大于 3 的值。在一般情况下，X应该取一个大于其他任何可能项¹的值。抛开实际限制不谈，这种@<关系没有最大值：复合项大于非复合项，根据定义，复合项可以任意大。

所以，这种方法不是决定性的，我认为它不能轻易纠正。

---

1：请注意，对于任何给定的术语，我们可以找到局部最大和最小术语，这对于问题的目的来说已经足够了。

Answer 2

第三次尝试！使用 GNU Prolog 1.4.4 开发和测试。

---

展览“A”：“尽可能简单”

lt(X,Y) :-
   X \== Y,
   (  X \= Y
   -> alpha_omega(Alpha,Omega),
      term_variables(X+Y,Vars),                           % A
      \+ \+ (label_vars(Vars,Alpha,Omega), X @< Y),
      (  \+ (label_vars(Vars,Alpha,Omega), X @> Y)
      -> true
      ;  throw(error(instantiation_error,lt/2))
      )
   ;  throw(error(instantiation_error,lt/2))
   ).    

---

图表“B”：“无需标记所有变量”

lt(X,Y) :-
   X \== Y,
   (  X \= Y
   -> alpha_omega(Alpha,Omega),
      term_variables(X,Xvars),                            % B
      term_variables(Y,Yvars),                            % B 
      vars_vars_needed(Xvars,Yvars,Vars),                 % B
      \+ \+ (label_vars(Vars,Alpha,Omega), X @< Y),
      (  \+ (label_vars(Vars,Alpha,Omega), X @> Y)
      -> true
      ;  throw(error(instantiation_error,lt/2))
      )
   ;  throw(error(instantiation_error,lt/2))
   ).

vars_vars_needed([],    [],    []).
vars_vars_needed([A|_], [],    [A]).
vars_vars_needed([],    [B|_], [B]).
vars_vars_needed([A|As],[B|Bs],[A|ABs]) :-
   (  A \== B
   -> ABs = [B]
   ;  vars_vars_needed(As,Bs,ABs)
   ).

---

一些共享代码：

alpha_omega(Alpha,Omega) :-
    Alpha 是 -(10.0^1000)，% HACK！
    函子（欧米茄，z，255）。%哈克！

标签变量（[]，_，_）。
label_vars([Alpha|Vs],Alpha,Omega) :- label_vars(Vs,Alpha,Omega)。
label_vars([Omega|Vs],Alpha,Omega) :- label_vars(Vs,Alpha,Omega)。

Answer 3

这不是一个完全原创的答案，因为它建立在@coredump 的答案之上。

有一种类型的查询lt/2（执行显式术语遍历的参考实现）无法正确回答：

| ?- lt(b(b), a(a,a)).

no
| ?- @<(b(b), a(a,a)).

yes

原因是术语的标准顺序在比较函子名称之前考虑了数量。

其次，lt/2在比较变量时并不总是抛出 instatiation_error ：

| ?- lt(a(X), a(Y)).

no

---

我在这里写了另一个参考显式实现的候选者：

lt(X,Y):- var(X), nonvar(Y), !, throw(error(instantiation_error)).
lt(X,Y):- nonvar(X), var(Y), !, throw(error(instantiation_error)).

lt(X,Y):-
    var(X),
    var(Y),
    ( X \== Y -> throw(error(instatiation_error)) ; !, false).

lt(X,Y):-
    functor(X, XFunc, XArity),
    functor(Y, YFunc, YArity),
    (
        XArity < YArity, !
      ;
        (
            XArity == YArity, !,
            (
                XFunc @< YFunc, !
              ;
                XFunc == YFunc,
                X =.. [_|XArgs],
                Y =.. [_|YArgs],
                lt_args(XArgs, YArgs)
            )
        )
    ).

lt_args([X1|OtherX], [Y1|OtherY]):-
    (
        lt(X1, Y1), !
      ;
        X1 == Y1,
        lt_args(OtherX, OtherY)
     ).

lt_args(Xs, Ys)当存在一对对应的参数时，谓词为真Xi，Yi例如，lt(Xi, Yi)对于Xj == Yj所有先前的对Xj，Yj（例如lt_args([a,X,a(X),b|_], [a,X,a(X),c|_])为真）。

一些示例查询：

| ?- lt(a(X,Y,c(c),_Z1), a(X,Y,b(b,b),_Z2)).

yes
| ?- lt(a(X,_Y1,c(c),_Z1), a(X,_Y2,b(b,b),_Z2)).
uncaught exception: error(instatiation_error)

Answer 4

什么鬼！我也来试试！

lt(X,Y) :-
   X \== Y,
   (  X \= Y
   -> term_variables(X,Xvars),
      term_variables(Y,Yvars),
      list_vars_excluded(Xvars,Yvars,XonlyVars),
      list_vars_excluded(Yvars,Xvars,YonlyVars),

      _   = s(T_alpha),
      functor(T_omega,zzzzzzzz,255), % HACK!

      copy_term(t(X,Y,XonlyVars,YonlyVars),t(X1,Y1,X1onlyVars,Y1onlyVars)),
      copy_term(t(X,Y,XonlyVars,YonlyVars),t(X2,Y2,X2onlyVars,Y2onlyVars)),
      maplist(=(T_alpha),X1onlyVars), maplist(=(T_omega),Y1onlyVars),
      maplist(=(T_omega),X2onlyVars), maplist(=(T_alpha),Y2onlyVars),

      % do T_alpha and T_omega have an impact on the order?
      (  compare(Cmp,X1,Y1),      
         compare(Cmp,X2,Y2)
      -> Cmp = (<)                % no: demand that X @< Y holds
      ;  throw(error(instantiation_error,lt/2))
      )

   ;  throw(error(instantiation_error,lt/2))
   ).

还有一些辅助的东西：

listHasMember_identicalTo([X|Xs],Y) :-
   (  X == Y
   -> true
   ;  listHasMember_identicalTo(Xs,Y)
   ).

list_vars_excluded([],_,[]).
list_vars_excluded([X|Xs],Vs,Zs) :-
   (  listHasMember_identicalTo(Vs,X)
   -> Zs = Zs0
   ;  Zs = [X|Zs0]
   ),
   list_vars_excluded(Xs,Vs,Zs0).

让我们进行一些测试（使用 GNU Prolog 1.4.4）：

?- lt(a(X,Y,c(c),Z1), a(X,Y,b(b,b),Z2))。
是的
?- lt(a(X,Y,b(b,b),Z1),a(X,Y,c(c),Z2))。
不
?- lt(a(X,Y1,c(c),Z1),a(X,Y2,b(b,b),Z2))。
未捕获的异常：错误（instantiation_error，lt/2）
?- lt(a(X,Y1,b(b,b),Z1),a(X,Y2,c(c),Z2))。
未捕获的异常：错误（instantiation_error，lt/2）
?- lt(b(b), a(a,a))。
是的
?- lt(a(X), a(Y))。
未捕获的异常：错误（instantiation_error，lt/2）
?- lt(X, 3)。
未捕获的异常：错误（instantiation_error，lt/2）
?- lt(X+a, X+b)。
是的
?- lt(X+a, Y+b)。
未捕获的异常：错误（instantiation_error，lt/2）
?- lt(a(X), b(Y))。
是的
?- lt(a(X), a(Y))。
未捕获的异常：错误（instantiation_error，lt/2）
?- lt(a(X), a(X))。
不

---

编辑 2015-05-06

将执行更改lt/2为使用T_alphaand T_omega，而不是两个新鲜变量。

• lt(X,Y)制作(和 ) 的两个副本和X(X1和X2) 的两个副本。YY1Y2
• X和的共享变量Y也被X1and共享Y1，并且被X2and共享Y2。
• T_alpha以标准顺序出现在所有其他术语（in X1, X2, Y1, ）之前。Y2
• T_omega在 标准顺序中的所有其他术语之后。
• X在复制的术语中，在但不在的变量Y（反之亦然）与T_alpha/统一T_omega。
  • 如果这对术语排序有影响，我们还不能决定排序。
  • 如果没有，我们就完成了。

现在，@false 给出的反例有效：

?- lt(X+1,1+2).
uncaught exception: error(instantiation_error,lt/2)
?- X=2, lt(X+1,1+2).
no

Answer 5

这是我认为可能是一种工作方法的草图。考虑目标lt(X, Y)和term_variables(X, XVars), term_variables(Y, YVars)。

定义的目的是确定进一步的实例化是否会改变术语顺序（7.2）。所以我们可能想直接找出负责任的变量。由于term_variables/2以与术语顺序相关的相同方式遍历术语，因此以下成立：

如果存在更改术语顺序的实例化，则必须实例化以见证更改的变量分别位于列表前缀XCs、和YCs中，或者XVarsYVars

1. XCs, YCs, XVars, 和YVars是相同的，或者

2. XCs并且YCs与最后一个元素相同，或

3. XCs并且YCs直到一个列表有另一个元素的末尾都是相同的，而另一个列表与其对应的变量列表XVars相同YVars。

作为一个有趣的特殊情况，如果 和 中的第一个元素XVars不同YVars，那么这些是唯一要测试相关性的变量。所以这包括没有公共变量的情况，但比这更普遍。

Answer 6

下一个！这应该比我之前的尝试做得更好：

lt(X,Y) :-
   X \== Y,
   (  X \= Y
   -> term_variables(X,Xvars),
      term_variables(Y,Yvars),

      T_alpha is -(10.0^1000),  % HACK!
      functor(T_omega,z,255),   % HACK!

      copy_term(t(X,Y,Xvars,Yvars),t(X1,Y1,X1vars,Y1vars)),
      copy_term(t(X,Y,Xvars,Yvars),t(X2,Y2,X2vars,Y2vars)),
      copy_term(t(X,Y,Xvars,Yvars),t(X3,Y3,X3vars,Y3vars)),
      copy_term(t(X,Y,Xvars,Yvars),t(X4,Y4,X4vars,Y4vars)),

      maplist(=(T_alpha),X1vars), maplist(maybe_unify(T_omega),Y1vars),
      maplist(=(T_omega),X2vars), maplist(maybe_unify(T_alpha),Y2vars),
      maplist(=(T_omega),Y3vars), maplist(maybe_unify(T_alpha),X3vars), 
      maplist(=(T_alpha),Y4vars), maplist(maybe_unify(T_omega),X4vars),

      % do T_alpha and T_omega have an impact on the order?
      (  compare(Cmp,X1,Y1),     
         compare(Cmp,X2,Y2),
         compare(Cmp,X3,Y3),
         compare(Cmp,X4,Y4),
      -> Cmp = (<)                % no: demand that X @< Y holds
      ;  throw(error(instantiation_error,lt/2))
      )

   ;  throw(error(instantiation_error,lt/2))
   ).

辅助maybe_unify/2处理同时出现在X和中的变量Y：

maybe_unify(K,X) :-
   (  var(X)
   -> X = K
   ;  true
   ).

使用 GNU-Prolog 1.4.4 检查：

?- lt(a(X,Y,c(c),Z1), a(X,Y,b(b,b),Z2)).
yes
?- lt(a(X,Y,b(b,b),Z1), a(X,Y,c(c),Z2)).
no
?- lt(a(X,Y1,c(c),Z1), a(X,Y2,b(b,b),Z2)).
uncaught exception: error(instantiation_error,lt/2)
?- lt(a(X,Y1,b(b,b),Z1), a(X,Y2,c(c),Z2)).
uncaught exception: error(instantiation_error,lt/2)
?- lt(b(b), a(a,a)).
yes
?- lt(a(X), a(Y)).
uncaught exception: error(instantiation_error,lt/2)
?- lt(X, 3).
uncaught exception: error(instantiation_error,lt/2)
?- lt(X+a, X+b).
yes
?- lt(X+a, Y+b).
uncaught exception: error(instantiation_error,lt/2)
?- lt(a(X), b(Y)).
yes
?- lt(a(X), a(Y)).
uncaught exception: error(instantiation_error,lt/2)
?- lt(a(X), a(X)).
no
?- lt(X+1,1+2).
uncaught exception: error(instantiation_error,lt/2)

?- lt(X+X+2,X+1+3).                                       % NEW
uncaught exception: error(instantiation_error,lt/2)

Answer 7

这个答案是我之前提出的答案的后续safe_term_less_than/2。

下一步是什么？一个安全的变体——compare/3难以想象地称为scompare/3：

比较（Ord，L，R）：-
   i_scompare_ord（[LR]，Ord）。

i_scompare_ord([], =)。
i_scompare_ord([LR|Ps], X) :-
   当((?=(L,R);nonvar(L),nonvar(R)), i_one_step_scompare_ord(L,R,Ps,X))。

i_one_step_scompare_ord(L, R, LRs, Ord) :-
   ( L == R
   -> scompare_ord（LRs，Ord）
   ; term_itype(L, L_type),
      term_itype(R, R_type),
      比较（Rel，L_type，R_type），
      ( 相对\== (=)
      -> Ord = Rel
      ;  化合物(L)
      -> L =.. [_|Ls],
         R =.. [_|Rs],
         短语（args_args_paired（Ls，Rs），LRs0，LRs），
         i_scompare_ord(LRs0, Ord)
      ; i_scompare_ord(LRs , Ord)
      )
   ）。

谓词term_itype/2和与前面定义args_args_paired//2的相同。

Answer 8

在这个答案中，我们提出了谓词，它是iso-prolog内置safe_term_less_than/2谓词的单调类似物（第 8.4.1 节，“术语小于”）。它的主要特性是： (@<)/2

• 显式遍历递归项。

• 基于prolog-cooutining设施，特别是when/2.

  • 比较可能会逐渐进行：

    • 每当实例化不够时“冻结”
    • 每当最重要术语的实例化发生变化时“唤醒”

  • 比较的当前前线表示为显式 (LIFO) 堆栈。

  • 当前状态直接围绕剩余目标传递。

---

以下代码已在sicstus-prolog版本 4.3.2 上开发和测试：

safe_term_less_than(L, R) :-                    % exported predicate
   i_less_than_([L-R]).

上面的定义safe_term_less_than/2基于以下辅助谓词：

i_less_than_([LR|LRs]) :-
   Cond = (?=(L,R) ; nonvar(L),nonvar(R)),
    when (Cond, i_lt_step_(L,R,LRs))。

i_lt_step_(L, R, LRs) :-
   ( L == R
   -> i_less_than_(LRs)
   ; term_itype(L, L_type),
      term_itype(R, R_type),
      比较（Ord，L_type，R_type），
      ord_lt_step_(Ord, L, R, LRs)
   ）。

term_itype(V, T) :-
   (   var (V) -> throw (错误( instanceation_error ,_))
   ;  浮动(V) -> T = t1_float(V)
   ;  整数(V) -> T = t2_integer(V)
   ;  可调用(V) -> T = t3_callable(A,F),函子(V, F, A)
   ; 抛出（错误（系统错误，_））
   ）。

ord_lt_step_(<, _, _, _)。
ord_lt_step_(=, L, R, LRs) :-
   (  化合物(L)
   -> L =.. [_|Ls],
      R =.. [_|Rs],
      短语（args_args_paired（Ls，Rs），LRs0，LRs），
      i_less_than_(LRs0)
   ; i_less_than_(LRs)
   ）。

args_args_paired([], []) --> []。
args_args_paired([L|Ls], [R|Rs]) --> [LR], args_args_paired(Ls, Rs)。

示例查询：

| ?- safe_term_less_than(X, 3)。
序言：trig_nondif（X，3，_A，_B），
序言：trig_or([_B,X],_A,_A),
prolog:when(_A,(?=(X,3);nonvar(X),nonvar(3)),user:i_lt_step_(X,3,[])) ？
是的
| ?- safe_term_less_than(X, 3), X = 4。
不
| ?- safe_term_less_than(X, 3), X = 2。
X = 2 ? ;
不
| ?- safe_term_less_than(X, a)。
序言：trig_nondif（X，a，_A，_B），
序言：trig_or([_B,X],_A,_A),
prolog:when(_A,(?=(X,a);nonvar(X),nonvar(a)),user:i_lt_step_(X,a,[])) ? ;
不
| ?- safe_term_less_than(X, a), X = a。
不
| ?- safe_term_less_than(X+2, Y+1), X = Y。
不

与之前的答案相比，我们观察到：

• 剩余目标的“文本量”显得有些“臃肿”。
• 查询?- safe_term_less_than(X+2, Y+1), X = Y.失败——就像它应该的那样！