iso_dif/2 реализовать намного проще, чем сравнение:

• Доступен встроенный оператор \=
• Теперь вы точно, какие аргументы предоставить to\=

Определение

Основываясь на ваших комментариях, безопасное сравнение означает, что порядок не изменится, если будут созданы переменные в обоих подтерминах. Если мы назовем сравнение 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).

(Изменить: с учетом замечаний Тудора Берариу: (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 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: обратите внимание, что для любого заданного термина, однако, мы можем найти локально максимальный и минимальный термины, которых будет достаточно для цели вопроса.

Далее! Это должно работать лучше, чем моя предыдущая попытка:

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)

Третья попытка! Разработано и протестировано с использованием GNU Prolog 1.4.4.

Приложение «А»: «настолько просто, насколько возможно».

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).

Это не полностью оригинальный ответ, поскольку он основан на ответе @ 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)

В этом ответе мы представляем предикат safe_term_less_than/2, монотонный аналог iso-prolog встроенный предикат (@<)/2 (§8.4 .1, «срок меньше»). Его основные свойства:

• Явный обход рекурсивных терминов.

• На основе возможностей prolog-coroutining, в частности, when/2.

  • Сравнение может прогрессировать постепенно:

    • "freeze" whenever instantiation is not sufficient
    • "просыпаться" всякий раз, когда изменяется реализация наиболее значимых условий

  • Текущая передняя линия сравнения представлена ​​в виде явного стека (LIFO).

  • Текущее состояние напрямую передается остаточным целям.

Следующий код был разработан и протестирован на sicstus- пролог версии 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,[])) ? 
yes
| ?- safe_term_less_than(X, 3), X = 4.
no
| ?- safe_term_less_than(X, 3), X = 2.
X = 2 ? ;
no
| ?- 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,[])) ? ;
no
| ?- safe_term_less_than(X, a), X = a.
no
| ?- safe_term_less_than(X+2, Y+1), X = Y.
no

По сравнению с предыдущими ответами мы наблюдаем:

• «Объем текста» остаточных целей выглядит как бы «раздутым».
• Запрос ?- safe_term_less_than(X+2, Y+1), X = Y. терпит неудачу - как и должно быть!

Какого черта! Я тоже попробую!

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)).
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

Изменить 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 идет после всех остальных терминов в стандартном порядке.
• In the copied terms, the variables that are in X but not in Y (and vice versa) are unified with T_alpha / T_omega.
  • If this has an impact on term ordering, we cannot yet decide the ordering.
  • Если это не, все готово.

Теперь контрпример @false работает:

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

Вот набросок того, что, по моему мнению, могло бы быть рабочим подходом. Рассмотрим цель lt(X, Y) и term_variables(X, XVars), term_variables(Y, YVars).

Цель определения - определить, может ли дальнейшее создание экземпляра изменить порядок терминов (7.2). Поэтому мы могли бы захотеть напрямую выяснить ответственные переменные. Поскольку term_variables/2 проходит через термин точно так же, как это имеет отношение к порядку терминов, выполняется следующее:

Если есть экземпляр, который изменяет порядок терминов, то переменные, которые должны быть созданы, чтобы засвидетельствовать это изменение, находятся в префиксах списка XCs, YCs из XVars и YVars соответственно, и либо

1. XCs, YCs, XVars и YVars идентичны, или

2. XCs и YCs идентичны до последнего элемента, или

3. XCs и YCs идентичны до конца, где один список имеет дополнительный элемент, а другой список идентичен соответствующему списку переменных XVars или YVars.

В качестве интересного особого случая, если первые элементы в XVars и YVars различаются, то это единственные переменные, которые нужно проверить на релевантность. Таким образом, это включает случай, когда нет общей переменной, но он даже более общий, чем это.

Этот ответ является продолжением моего предыдущего ответа, в котором был представлен 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) :-
   when((?=(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),
      compare(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 такие же, как , определенные ранее.