如何在ISO Prolog中定义(和命名)相应的安全术语比较谓词？

Question

标准术语顺序(ISO/IEC 13211-1 7.2术语顺序)是在所有术语(包括变量)上定义的.虽然有很好的用途 - 想想实现setof/3,但这使得许多其他清洁和逻辑用途的内置插件在8.4 Term比较中声明性的噩梦与imps(命令式构造的简短形式)四处都有.8.4术语比较功能:

8.4术语比较

8.4.1(@ = <)/ 2,(==)/ 2,(\ ==)/ 2,(@ <)/ 2,(@>)/ 2,(@> =)/ 2.
8.4.2比较/ 3.
8.4.3 sort/2.
8.4.4 keysort/2.

举个例子,考虑一下:

?- X @< a.
true.

这成功了,因为

7.2期限订单

命令term_precedes(3.181)定义
术语X术语是否在术语之前Y.

如果X且Y是相同的术语,则X term_precedes Y
和Y term_precedes X都是假的.

如果X和Y有不同的类型:Xterm_precedes Y当且仅当该
类型X先于类型Y按以下顺序:
variable先floating point先于integer
先atom先于compound.

注 - 测试术语排序的内置谓词
在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并(\=)/2相比具有显式遍历内部遍历术语,但是这方面的费用是非常低(=..)/2或functor/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排序;此外,fix(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

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

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

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

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

yes

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

其次，lt/2在比较变量时并不总是抛出 instatation_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)当存在一对对应的参数 时，谓词为 true Xi，Yi使得lt(Xi, Yi)和Xj == Yj对于所有前面的对Xj，Yj（例如lt_args([a,X,a(X),b|_], [a,X,a(X),c|_])为 true）。

一些示例查询：

| ?- 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 3

下一个!这应该比我以前的尝试做得更好:

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 4

第三次尝试!使用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 is -(10.0^1000),    % HACK!
    functor(Omega,z,255).     % HACK!

label_vars([],_,_).
label_vars([Alpha|Vs],Alpha,Omega) :- label_vars(Vs,Alpha,Omega).
label_vars([Omega|Vs],Alpha,Omega) :- label_vars(Vs,Alpha,Omega).