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 @
正如评论中所述，如果在并行遍历两个术语时，第一个（可能）有区别的术语对包含：
- 两个不相同的变量（
lt(X,Y))
- 一个变量和一个非变量 (
lt(X,a), or lt(10,Y))
但首先，让我们回顾一下您不想使用的可能方法：
定义显式的术语遍历比较函数。我知道出于性能原因您不愿意这样做，但这仍然是最直接的方法。无论如何，我建议您这样做，以便您有一个参考实现来与其他方法进行比较。
-
使用约束进行延迟比较：我不知道如何使用 ISO Prolog 来做到这一点，但是使用例如ECLiPSe，我将暂停对未实例化变量集的实际比较（使用term_variables/2），直到不再有变量为止。之前，我还建议使用协程/0 http://eclipseclp.org/doc/bips/kernel/obsolete/coroutine-0.html谓词，但我忽略了一个事实，即它不影响@<运算符（仅<).
这种方法并不解决与您描述的完全相同的问题，但它非常接近。一个优点是，如果赋予变量的最终值满足比较，它不会引发异常，而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 and Y2 of X and Y，其中所有变量都被实例化：
- In
X2，变量统一为1。
- In
Y2，变量统一为0。
所以，如果关系X2 @< Y2仍然成立，我们知道我们不依赖变量之间的标准术语排序。否则，我们会抛出异常，因为这意味着1 @< 0以前没有发生的关系导致关系失败。
缺点
（基于OP的评论）
-
lt(X+a,X+b)应该成功但会产生错误。
乍一看，人们可能会认为将两个项中出现的变量统一为具有相同的值，例如val，可能会解决这种情况。但也可能会出现其他情况X相比而言，这会导致错误的判断。
-
lt(X,3)应该会产生错误但会成功。
In order to fix that case, one should unify X with something that is greater than 3. In the general case, X should take a value that is greater than other any possible term1. Practical limitations aside, the @< relation has no maximum: compound terms are greater than non-compound ones, and by definition, compound terms can be made arbitrarly great.
因此，这种方法并不是决定性的，而且我认为它不容易纠正。
1：但是请注意，对于任何给定的项，我们可以找到局部最大和最小项，这足以满足问题的目的。
