logo标签列表

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

sortingprologiso-prologprolog-dif
33

标准术语顺序（ISO/IEC 13211-1 7.2 术语顺序）适用于所有术语，包括变量。虽然这样做有好处——可以考虑实现setof/3，但这会使得8.4术语比较中许多本来干净、逻辑清晰的内置函数使用变得混乱不堪，到处都是命令式结构的影响（简称为imps）。8.4术语比较功能包括：

8.4 术语比较

8.4.1 (@=<)/2, (==)/2, (==)/2, (@<)/2, (@>)/2, (@>=)/2.
8.4.2 compare/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 都为 false。

如果 X 和 Y 具有不同的类型：则当以下顺序中 X 的类型在 Y 的类型之前时，X term_precedes 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使用约束条件或dif_si/2（以前是iso_dif/2）产生一个干净的实例化错误。

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

我的问题是如何定义（和命名）ISO Prolog中相应的安全术语比较谓词？最好不需要任何显式的术语遍历。可能需要澄清的是：上面的 dif_si/2 不使用任何显式的术语遍历。(\==)/2 和 (\=)/2 都在内部遍历术语，但与使用 (=..)/2 或 functor/3、arg/3 进行显式遍历相比，开销极低。请保留HTML标签。
1
由于仍然没有答案：如果有任何好的答案出现，我将授予下一个400点赏金。 - false
1
使用 freeze/2 有什么问题吗？ - user1812457
1
@Boris：不同的问题。你仍然需要遍历这些术语。毕竟，两个问题都必须先找到这样一个“关键对”。 - false
1
@Boris：此外，仅使用freeze/2将无法正常工作，您还需要在?=与when/2一起使用。例如：lt(X+2, Y+1), X = Y 应该已经失败了。 - false
1
我想补充一句话，以表达我的感激之情：对于本主题帖中只要稍微有解决方案的痕迹的答案，我都会点赞，因为这个问题很有趣且困难，当思考这个问题时，你会学到很多术语。 - mat
显示剩余4条评论
8个回答
8

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）首先按极化排序；此外，修复（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 的副本，其中所有变量都被实例化：

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

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

缺点

(基于 OP 的评论)

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

    乍一看，人们可能认为将同时出现在两个术语中的变量统一为相同的值，比如 val，可以解决问题。然而，在比较的术语中可能还有其他出现的 X，这会导致错误的判断。

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

    为了解决这种情况，应将 X 与大于 3 的某个值统一。在一般情况下，X 应该取一个比其他任何可能的术语都要大的值1。除了实际限制外，@< 关系没有最大值：复合术语大于非复合术语，并且按定义，可以使复合术语任意大。

因此，这种方法并不具有决定性，我认为它不容易得到纠正。

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

在ECLiPSe中，“coroutine/0”不会使“(@<)/2”变得声明性：X@<1，X=1成功，而X<1，X=1失败。(corr.) - false
@false 我进行了编辑，以使用subsumes/2。顺便说一下，给定的代码可能会在循环术语中表现不佳。但请注意，A=foo(A), B=foo(B), A @< B不会终止，因此这可能不是一个问题。 - coredump
2
我建议使用GNU或SICStus Prolog以符合ISO标准。 - false
1
lt(X+a,X+b) 应该成功，但是产生了错误。 - false
3
在某些情况下，显式术语遍历的参考实现是错误的，因为术语的标准顺序在比较函数名之前考虑了从属关系。例如，对于查询 | ?- lt(b(b), a(a,a))，它返回“no”，但是使用 | ?- @<(b(b), a(a,a)) 将会返回“yes”。 - Tudor Berariu
显示剩余6条评论
6

第三次尝试！使用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),    % 黑客攻击！
    functor(Omega,z,255).     % 黑客攻击！

label_vars([],_,_).
label_vars([Alpha|Vs],Alpha,Omega) :- label_vars(Vs,Alpha,Omega).
label_vars([Omega|Vs],Alpha,Omega) :- label_vars(Vs,Alpha,Omega).
2
除非您使用了非常先进的浮点表示方法，否则您的起点和终点应该会出现evaluation_error(float_overflow)。 - false
2
我并不是很开心，但你符合标准。我希望这个可以更快地完成... - false
1
@false。我没有得到溢出错误，这不应该给我“FP负无穷大”吗？ - repeat
2
ISO Prolog 中没有这样的值 - 请参考我们在去年十二月/今年一月所进行的一些浮点数相关的讨论。 - false
因为label_vars/3会产生相当大的开销，与OP的要求相反，所以我会将其降级。为什么这个问题还能得到赏金呢？ - user502187
@j4nbur53。如果我没记错，这个答案是第一个通过问题中OP给出的所有测试用例以及其他人在他们的回答和评论中提供的答案的。当然，代码非常低效...我很希望看到另一种不使用显式术语遍历（并给出相同答案）的替代方案！ - repeat
5

这不是完全原创的答案，它基于 @coredump 的 答案。

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

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

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

yes

原因是标准术语顺序在比较函数名之前考虑了arity。
其次，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)
1
为什么lt_args/2中没有[]的情况？这可能有道理，但有点令人惊讶。 - false
1
这意味着所有的参数都是等效的。 - Tudor Berariu
4

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

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)
1
@j4nbur53。"可能？" 为什么您会点赞这个明显错误的答案，而将我后来更好的答案全部点踩？发生了什么事情？ - repeat
4
这个答案是错误的！即使“安全比较”仍可能摇摆不定，lt(A+0+B,B+1+A)也会成功：当A=3，B=2时，lt(A+0+B,B+1+A)失败，但当A=2，B=3时，lt(A+0+B,B+1+A)成功...如果不使用协程，则引发异常将是正确的行为。 - repeat
3
@j4nbur53，你所假设的隐含代数性质在一般情况下未必成立。请参考Mats Carlsson在1996年7月16日发布的帖子“比较无限项”（Comparing Infinite Terms），链接为https://groups.google.com/d/msg/comp.lang.prolog/Om8bTZ_Mom4/0KhnzE5IwLEJ。 - repeat
2
@j4nbur53。使用SICStus Prolog 4.3.2，我得出了（基本上）相同的结论......小心SWI的“标准项顺序”！最好称其为“非标准项顺序”。引用自SWI手册：“变量< 数字 < 字符串 < 原子< 复合项”。 - repeat
3
@j4nbur53. 是和不是的:) 首先问SWI ?- 1.0 @> 0. ，然后考虑以下选自SICStus Prolog 4.3.2手册的摘录：“按年龄排序的变量（[...]）。 浮点数，按数字顺序排序（例如，-1.0排在1.0之前）。 整数，按数字顺序排序（例如，-1排在1之前）。 原子，按字母顺序排序（即字符代码）。 复合术语首先按arity排序，然后按主要函数符号名称排序[...]。 ”我对这些观察得出的结论（由Jan Wielemaker在私人电子邮件中确认）是：** SWI的实现 (@<)/2 和相关谓词将数字归为一类！** - repeat
显示剩余2条评论
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))。 未捕获异常：错误（实例化错误，lt/2） - lt(a(X,Y1,b(b,b),Z1), a(X,Y2,c(c),Z2))。 未捕获异常：错误（实例化错误，lt/2） - lt(b(b), a(a,a))。 是的 - lt(a(X), a(Y))。 未捕获异常：错误（实例化错误，lt/2） - lt(X, 3)。 未捕获异常：错误（实例化错误，lt/2） - lt(X+a, X+b)。 是的 - lt(X+a, Y+b)。 未捕获异常：错误（实例化错误，lt/2） - lt(a(X), b(Y))。 是的 - lt(a(X), a(Y))。 未捕获异常：错误（实例化错误，lt/2） - lt(a(X), a(X))。 不是
编辑2015-05-06：
将lt/2的实现更改为使用T_alpha和T_omega而不是两个新变量。
- lt（X，Y）创建X的两个副本（X1和X2）和Y的两个副本（Y1和Y2）。 - X和Y的共享变量也由X1和Y1以及X2和Y2共享。 - T_alpha在标准顺序中位于所有其他术语之前（在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
1
反例：lt(X+1,1+2) 成功，但 X = 2, ... 失败！ - false
1
我在考虑一些 T，它在术语排序方面排在所有其他术语之后（而不是在它们之前）。 - repeat
1
functor(F,z,255) 对于许多情况来说已经足够好了 - 当然，并非所有情况都适用。 - false
1
不需要暴力测试：您假设仅出现在一侧的变量是相关的。lt（X + X + 2，X + 1 + 3）应该是一个错误，但它并不是。 - false
lt_si/2是什么情况？ - false
4
这个回答是我之前的一个回答的后续，那个回答介绍了safe_term_less_than/2。
接下来呢？一个安全的compare/3变体——毫不起眼地被称为scompare/3：
scompare(Ord, L, R) :- i_scompare_ord([L-R], Ord).
i_scompare_ord([], =). i_scompare_ord([L-R|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), ( Rel \== (=) -> Ord = Rel ; compound(L) -> L =.. [_|Ls], R =.. [_|Rs], phrase(args_args_paired(Ls,Rs), LRs0, LRs), i_scompare_ord(LRs0, Ord) ; i_scompare_ord(LRs , Ord) ) )。

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

4
这里是我认为可能是可行方法的草图。考虑目标lt(X, Y)和term_variables(X, XVars), term_variables(Y, YVars)。
定义的目的是确定进一步实例化是否可能改变术语顺序（7.2）。因此，我们可能想直接找出负责的变量。由于term_variables/2以与术语顺序相关的方式遍历术语，因此以下内容成立：
如果有一种实例化会改变术语顺序，则必须实例化的变量在XVars和YVars的前缀列表XCs，YCs中，并且要么
1. XCs、YCs、XVars和YVars相同，或者 2. XCs和YCs在最后一个元素之前相同，或者 3. XCs和YCs在其中一个列表有一个更进一步的元素的结尾处相同，而另一个列表与其对应的变量列表XVars或YVars相同。
作为一个有趣的特例，如果XVars和YVars的第一个元素不同，则这些是唯一要测试相关性的变量。因此，这包括没有共同变量的情况，但它甚至比那更通用。
1
该问题包含一个链接，其中包括所有谓词的概述，包括term_variables/2。 - false
1
请注意，如果有一个实例化改变了...那么"if"就会发生变化。否则不等式完全无关紧要。以问题X lt Y为例，然后取X+2 lt Y+1。这只是同样的问题！ - false
1
T1Vars = [X,Y]，T2Vars = [X,Y]。因此，适用于情况1，我们必须测试两个变量 - 这是最坏的情况。X = z（..）可能是顺序更改的证据。 - false
4
在这个答案中，我们介绍了谓词safe_term_less_than/2，它是 内置谓词 (@<)/2（§8.4.1，“项小于”）的单调模拟。它的主要特点是：
  • 显式遍历递归项。

  • 基于工具，特别是when/2。

    • 比较可能会逐渐进行：

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

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

    • 当前状态直接传递到剩余目标中。
下面的代码已在 4.3.2版本上进行了开发和测试:
safe_term_less_than(L, R) :-                    % exported predicate
   i_less_than_([L-R]).

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

i_less_than_([L-R|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), compare(Ord, L_type, R_type), ord_lt_step_(Ord, L, R, LRs) ).
term_itype(V, T) :- ( var(V) -> throw(error(instantiation_error,_)) ; float(V) -> T = t1_float(V) ; integer(V) -> T = t2_integer(V) ; callable(V) -> T = t3_callable(A,F), functor(V, F, A) ; throw(error(system_error,_)) ).
ord_lt_step_(<, _, _, _). ord_lt_step_(=, L, R, LRs) :- ( compound(L) -> L =.. [_|Ls], R =.. [_|Rs], phrase(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]) --> [L-R], args_args_paired(Ls, Rs).

示例查询：

| ?- safe_term_less_than(X, 3).
prolog:trig_nondif(X,3,_A,_B),
prolog: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).
prolog:trig_nondif(X,a,_A,_B),
prolog: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.失败了——就像它应该做的那样！
@false。我还不确定when((?=(L,R) ; nonvar(L),nonvar(R)),...)是否需要一些“重新冻结”... 如果?=(L,R)成功，那么(L == R ; nonvar(L),nonvar(R))是否被暗示了？ - repeat
以上代码不像SWI-Prolog那样将数字合并，而且可能也无法处理有理树，即无限术语。这难道不表明单遍历解决方案不能涵盖所有Prolog系统吗？ - user502187
另一方面，我们仍然不知道iso_dif/2的想法是否可行或不可行，它意味着希望它适用于各种Prolog系统，因为(==)/2和(=)/2将反映不同系统的特定性。但是，代数属性已经驳斥了其中的一些说法。 - user502187
网页内容由stack overflow 提供, 点击上面的
可以查看英文原文，
原文链接