Подтвердить что ты не робот

Унификация с обнаружением STO

В унификации ISO Prolog определяется только для тех случаев, которые являются NSTO (не подвержены возникновению-проверке). Идея заключается в том, чтобы охватить те случаи унификации, которые в основном используются в программах и которые фактически поддерживаются всеми системами Prolog. Более конкретно, ISO/IEC 13211-1:1995 гласит:

7.3.3 При условии наличия-проверки (STO) и не подлежащего проверке (NSTO)

Множество уравнений (или двух слагаемых) "подлежит возникновению" check "(STO), если существует способ продолжения шаги алгоритма Хербранда, такие, что 7.3.2 g
случается.

Множество уравнений (или двух слагаемых)" не подлежит "происходит-check" (NSTO), если нет способа продолжить через шаги алгоритма Хербранда, так что 7.3.2 g происходит.

...

Этот шаг 7.3.2 g гласит:

g) Если существует уравнение вида X = t такое, что  что X - переменная, а t - непеременный член  который содержит эту переменную, а затем выйти с ошибкой (не  единичный, положительный результат - проверка).

Полный алгоритм называется алгоритмом Хербранда и является тем, что обычно называют алгоритмом унификации Martelli-Montanari - который, по существу, осуществляется путем переписывания наборов уравнений не детерминированным образом.

Обратите внимание, что новые уравнения вводятся с:

d) Если существует уравнение вида f (a 1, a 2,... a N) =
 f (b 1, b 2,... b N), затем заменим его на набор уравнений   a i= b i.

Это означает, что два составных члена с одним и тем же функтором, но с другой аристократией никогда не будут способствовать STO-ness.

Этот недетерминизм - это то, что делает STO-тест настолько сложным для реализации. В конце концов, недостаточно проверить, может ли понадобиться проверка наличия, но доказать, что для всех возможных способов выполнения алгоритма этот случай никогда не произойдет.

Вот пример, иллюстрирующий ситуацию:

?- A/B+C*D = 1/2+3*4.

Унификация может начинаться с A = 1, но также и с любой другой пар и продолжать в любом порядке. Чтобы обеспечить собственность NSTO, необходимо обеспечить, чтобы не было пути, который мог бы создать ситуацию STO. Рассмотрим случай, который не является проблематичным для текущих реализаций, но это все еще STO:

?- 1+A = 2+s(A).

Системы пролога начинаются с перезаписи этого уравнения на:

?- 1 = 2, A = s(A).

Теперь они выбирают либо

  • 1 = 2, что приводит к выходу алгоритма с ошибкой или

  • A = s(A), где применяется шаг g, и обнаруживается STO-ness.

Мой вопрос двоякий. Сначала речь идет о реализации в ISO Prolog unify_sto(X,Y) (используя только определенные встроенные элементы части 1), для которых выполняется следующее:

  • если унификация является STO, тогда unify_sto(X,Y) вызывает ошибку, в противном случае

  • если unify_sto(X,Y) преуспевает, тогда также X = Y успешно

  • Если unify_sto(X,Y) терпит неудачу, то также X = Y не работает

и мой второй вопрос касается конкретной ошибки в этой ситуации. См. ISO классы ошибок.

Вот простой шаг для начала: все случаи успеха покрываются успехом unify_with_occurs_check(X,Y). Остается сделать различие между сбоем NSTO и случаями ошибок STO. Это стало началом трудностей...

4b9b3361

ОТВЕТЫ

Ответ 1

Третья попытка. Это в основном ошибка в предыдущем ответе (который уже имел много изменений). Редактировать: 06/04/2015

При создании более общего термина я оставлял обе подтермы as-is, если бы одна из них была переменной. Теперь я строю более общий термин для "другого" подтерма в этом случае, вызывая term_general/2.

unify_sto(X,Y):-
  unify_with_occurs_check(X,Y) -> true ;
  (
   term_general(X, Y, unify(X,Y), XG, YG),
   \+unify_with_occurs_check(XG,YG),
   throw(error(type_error(acyclic, unify(X,Y)),_))
  ).

term_general(X, Y, UnifyTerm, XG, YG):-
  (var(X) -> (XG=X, term_general(Y, YG)) ;
  (var(Y) -> (YG=Y, term_general(X, XG)) ;
  ((
    functor(X, Functor, Len),
    functor(Y, Functor, Len),
    X=..[_|XL],
    Y=..[_|YL],
    term_general1(XL, YL, UnifyTerm, NXL, NYL)
  ) ->
  (
    XG=..[Functor|NXL],
    YG=..[Functor|NYL]
  ) ;
  ( XG=_, YG=_ )
  ))).

term_general1([X|XTail], [Y|YTail], UnifyTerm, [XG|XGTail], [YG|YGTail]):-
  term_general(X, Y, UnifyTerm, XG, YG),
  (
    \+(unify_with_occurs_check(XG,YG)) ->
        throw(error(type_error(acyclic,UnifyTerm),_)) ;
        term_general1(XTail, YTail, UnifyTerm, XGTail, YGTail)
  ).
term_general1([], [], _, [], []).

term_general(X, XG):-
  (var(X) -> XG=X ;
  (atomic(X) -> XG=_ ;
  (
     X=..[_|XL],
     term_general1(XL, XG)
  ))).

term_general1([X|XTail], [XG|XGTail]):-
  term_general(X, XG),
  term_general1(XTail, XGTail).
term_general1([], _).

И вот единицы измерения, упомянутые в этом вопросе:

unit_tests:-
  member([TermA,TermB], [[_A+_B,_C+_D], [_E+_F, 1+2],
                         [a(_G+1),a(1+_H)], [a(1), b(_I)],
                         [A+A,a(B)+b(B)], [A+A,a(B,1)+b(B)]]),
  (unify_sto(TermA, TermB)->Unifies=unifies ; Unifies=does_not_unify),
  writeln(test(TermA, TermB, Unifies)),
  fail.
unit_tests:-
     member([TermA,TermB], [[A+A,B+a(B)], [A+A,A+b(A)],
                            [A+A,a(_)+b(A)], [1+A,2+s(A)],
                            [a(1)+X,b(1)+s(X)]]),
  catch(
   (
     (unify_sto(TermA, TermB)->true;true),
     writeln(test_failed(TermA, TermB))
   ), E, writeln(test_ok(E))),
   fail.
unit_tests.

Ответ 2

Вот еще одна попытка:

unify_sto(X,Y):-
  unify_with_occurs_check(X,Y) -> true ;
  (
    term_general(X, Y, XG, YG),
    \+(unify_sto1(XG,YG)),
    throw(error(type_error(acyclic,unify(X,Y)),_))
  ).

unify_sto1(X, Y):-
   unify_with_occurs_check(X,Y).
unify_sto1(X, Y):-
   X\=Y.

term_general(X, Y, XG, YG):-
  ((var(X) ; var(Y)) ->  (XG=X, YG=Y) ;
  ((
    functor(X, Functor, Len),
    functor(Y, Functor, Len),
    X=..[_|XL],
    Y=..[_|YL],
    term_general1(XL, YL, NXL, NYL)
  ) ->
  (
    XG=..[Functor|NXL],
    YG=..[Functor|NYL]
  ) ;
  ( XG=_, YG=_ )
  )).

term_general1([X|XTail], [Y|YTail], [XG|XGTail], [YG|YGTail]):-
  term_general(X, Y, XG, YG),
  term_general1(XTail, YTail, XGTail, YGTail).
term_general1([], [], [], []).

Сначала он пытается unify_with_occurs_check, и если это не удастся, тогда он перейдет к созданию еще двух общих терминов, пересекающих структуру каждого термина.

  • Если любой из них является переменной, он оставляет оба выражения как-есть.
  • Если оба термина являются одним и тем же атомом или оба являются компромиссными терминами с тем же функтор и арность [*], он обходит свои аргументы, делая больше общий термин для них.
  • В противном случае он назначает новую новую переменную для каждого термина.

Затем он снова пытается выполнить unify_with_occurs_check более общие термины  для проверки ациклической унификации и соответственно выдачи ошибки.

[*] Тест на arity в компромиссных терминах выполняется с жадностью, так как term_general1/4 не даст рекурсии, поскольку OP заявляет, что использует только встроенные предикаты, определенные в части 1 этого ссылка с не включает length/2.. (отредактировано:) Добавлены два вызова functor/3 для проверки функтора и arity перед вызовом term_general1, чтобы не пытаться проверять внутренние термины, если их arity не соответствует)

например:

?- unify_sto(s(1)+A,A+s(B)).
A = s(1),
B = 1
?- unify_sto(1+A,2+s(A)).
ERROR: Type error: `acyclic' expected, found `unify(1+_G5322,2+s(_G5322))'
?- unify_sto(a(1)+X,b(1)+s(X)).
ERROR: Type error: `acyclic' expected, found `unify(a(1)+_G7068,b(1)+s(_G7068))'

Редактировать 06/02/2015:

Вышеизложенное решение для запроса:

unify_sto(A+A,a(A)+b(A)).

это не дает унифицированной ошибки.

Здесь улучшается алгоритм, который обрабатывает каждый подтерм попарно и дает ошибку, как только он обнаруживает его:

unify_sto(X,Y):-
  unify_with_occurs_check(X,Y) -> true ;
  (
   term_general(X, Y, unify(X,Y), XG, YG),
   \+unify_with_occurs_check(XG,YG),
   throw(error(type_error(acyclic,unify(X,Y)),_))
  ).

unify_sto1(X, Y):-
   unify_with_occurs_check(X,Y).
unify_sto1(X, Y):-
   X\=Y.

term_general(X, Y, UnifyTerm, XG, YG):-
  ((var(X) ; var(Y)) ->  (XG=X, YG=Y) ;
  ((
    functor(X, Functor, Len),
    functor(Y, Functor, Len),
    X=..[Functor|XL],
    Y=..[Functor|YL],
    term_general1(XL, YL, UnifyTerm, NXL, NYL)
  ) ->
  (
    XG=..[Functor|NXL],
    YG=..[Functor|NYL]
  ) ;
  ( XG=_, YG=_ )
  )).

term_general1([X|XTail], [Y|YTail], UnifyTerm, [XG|XGTail], [YG|YGTail]):-
  term_general(X, Y, UnifyTerm, XG, YG),
  \+(unify_with_occurs_check(XG,YG))-> throw(error(type_error(acyclic,UnifyTerm),_)) ;
  term_general1(XTail, YTail, UnifyTerm, XGTail, YGTail).
term_general1([], [], _, [], []).

Тестовый пример запроса, который дал неправильные результаты в исходном ответе:

   ?-  unify_sto(A+A,a(A)+b(A)).
    ERROR: Type error: `acyclic' expected, found `unify(_G6902+_G6902,a(_G6902)+b(_G6902))'
   ?- unify_sto(A+A, a(_)+b(A)).
    ERROR: Type error: `acyclic' expected, found `unify(_G5167+_G5167,a(_G5173)+b(_G5167))'

Ответ 3

Вот моя попытка:

unify_sto(X,Y):-
  unify_with_occurs_check(X,Y) -> true ;
  (
    term_general(X, XG),
    term_general(Y, YG),
    \+(unify_sto1(XG,YG)),
    throw(error(type_error(acyclic,unify(X,Y)),_))
  ).

unify_sto1(X, Y):-
   unify_with_occurs_check(X,Y).
unify_sto1(X, Y):-
   X\=Y.

term_general(X, Y):-
  (var(X) ->  Y=X ;
  (atomic(X) -> Y=_ ;
  (
    X=..[Functor|L],
    term_general1(L, NL),
    Y=..[Functor|NL]
  ))).

term_general1([X|XTail], [Y|YTail]):-
  term_general(X, Y),
  term_general1(XTail, YTail).
term_general1([], []).

Сначала он пытается unify_with_occurs_check, и если он не выполняется, то он начинает строить более общий термин для каждого аргумента, затем пытается объединить такой термин и проверить, является ли он циклическим. Если он цикличен, то a type_error ациклического типа бросается.

например:

?- unify_sto(1+A,2+s(A)).
ERROR: Unhandled exception: error(type_error(acyclic,unify(1+_G3620,2+s(_G3620))))

Ответ 4

Вот моя версия, которую я использовал для тестирования версий @gusbro. Идея состоит в том, чтобы использовать Мартелли-Монтанари в буквальном смысле. Переписав список уравнений [X1=Y1,X2=Y2|Etc], некоторые правила перезаписи применяются немедленно - с помощью! для обязательств. И для некоторых правил я был не уверен, поэтому я оставил их как не определенные, как исходный алгоритм.

Заметим, что rewrite_sto/1 либо сбой, либо возникнет ошибка. Нам не интересен случай успеха, который обрабатывается без какого-либо поиска. Кроме того, обратите внимание, что уравнение, которое приводит к (немедленному) сбою, может быть устранено! Это немного неинтуитивно, но нас интересует здесь только случай STO.

unify_with_sto_check(X,Y) :-
   (  \+ unify_with_occurs_check(X, Y)
   -> rewrite_sto([X=Y])  % fails or error
   ;  X = Y
   ).

rewrite_sto(Xs0) :-
   select(X=Y, Xs0,Xs),
   (  X == Y
   ;  nonvar(X), nonvar(Y),
      functor(X,F,A),
      \+ functor(Y,F,A)
   ;  var(X), var(Y),
      X = Y
   ),
   !,
   rewrite_sto(Xs).
rewrite_sto(Xs0) :-
   select(X=Y, Xs0, Xs1),
   nonvar(X), nonvar(Y),
   functor(X,F,A),
   functor(Y,F,A),
   !,
   X =.. [_|XArgs],
   Y =.. [_|YArgs],
   maplist(\Xi^Yi^(Xi=Yi)^true, XArgs, YArgs, XYs),
   append(XYs,Xs1,Xs),
   rewrite_sto(Xs).
rewrite_sto(Xs0) :-
   select(X=Y, Xs0,Xs),
   (  var(X), nonvar(Y) -> unify_var_term(X, Y)
   ;  nonvar(X), var(Y) -> unify_var_term(Y, X)
   ;  throw(impossible)
   ),
   rewrite_sto(Xs).

unify_var_term(V, Term) :-
   (  unify_with_occurs_check(V, Term) -> true
   ;  throw(error(type_error(acyclic_term, Term), _))
   ).

Ответ 5

В SWI-прологе:

unify_sto(X,Y) :-
  \+ unify_with_occurs_check(X,Y),
  X = Y,
  !,
  writeln('Error: NSTO failure'),
  fail.

unify_sto(X,Y) :-
  X = Y.

дает следующие результаты:

[debug]  ?- unify_sto(X,s(X)).
Error: NSTO failure
false.

[debug]  ?- unify_sto(X,a).
X = a.

[debug]  ?- unify_sto(b,a).
false.