algorithm - online - logic programming

Unificación con detección de STO

Question

En ISO Prolog, la unificación se define solo para aquellos casos que son NSTO (no están sujetos a la verificación de ocurrencia). La idea detrás es cubrir aquellos casos de unificaciones que se usan principalmente en programas y que en realidad son compatibles con todos los sistemas Prolog. Más específicamente, ISO / IEC 13211-1: 1995 dice:

7.3.3 Sujeto a verificación de ocurrencias (STO) y no sujeto
a occur-check (NSTO)

Un conjunto de ecuaciones (o dos términos) está "sujeto a que ocurra-
marque "(STO) si existe una forma de proceder
los pasos del algoritmo Herbrand tal que 7.3.2 g
sucede.

Un conjunto de ecuaciones (o dos términos) "no está sujeto a
ocurre-marque "(NSTO) si no hay forma de proceder
a través de los pasos del algoritmo Herbrand tal que
7.3.2 g sucede.

...

Este paso 7.3.2 g lee:

g) Si hay una ecuación de la forma X = t tal
que X es una variable yt es un término no variable
que contiene esta variable, luego sale con falla ( no
comprobaciones de ocurrencias unificables y positivas ).

El algoritmo completo se llama algoritmo Herbrand y es lo que comúnmente se conoce como el algoritmo de unificación Martelli-Montanari , que esencialmente procede al reescribir conjuntos de ecuaciones de una manera no determinista .

Tenga en cuenta que las nuevas ecuaciones se introducen con:

d) Si hay una ecuación de la forma f (a ₁ , a ₂ , ... a _N ) =
f (b ₁ , b ₂ , ... b _N ) luego reemplazarlo por el conjunto de ecuaciones
a _i = b _i .

Lo que significa que dos términos compuestos con el mismo funtor pero diferente arity nunca contribuirán a STO-ness.

Este no determinismo es lo que hace que la prueba STO sea tan difícil de implementar. Después de todo, no es suficiente para probar si una verificación de ocurrencias puede ser necesaria o no, sino para probar que de todas las formas posibles de ejecutar el algoritmo este caso nunca sucederá.

Aquí hay un caso para ilustrar la situación:

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

La unificación puede comenzar por A = 1 , pero también por cualquiera de los otros pares, y continuar en cualquier orden. Para garantizar la propiedad de NSTO, se debe garantizar que no haya ninguna ruta que pueda producir una situación de STO. Considere un caso que no es problemático para las implementaciones actuales, pero eso sigue siendo STO:

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

Los sistemas Prolog comienzan reescribiendo esta ecuación en:

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

Ahora, ellos eligen

• 1 = 2 que hace que el algoritmo salga con falla, o

• A = s(A) donde se aplica el paso g y se detecta STO-ness.

Mi pregunta es doble Primero se trata de una implementación en ISO Prolog de unify_sto(X,Y) (usando solo los unify_sto(X,Y) definidos de la Parte 1) para lo cual se cumple lo siguiente:

• si la unificación es STO, entonces unify_sto(X,Y) produce un error, de lo contrario

• si unify_sto(X,Y) tiene éxito, entonces también X = Y tiene éxito

• si unify_sto(X,Y) falla, entonces también X = Y falla

y mi segunda pregunta es sobre el error específico a emitir en esta situación. Ver las clases de error de ISO.

Aquí hay un paso simple para comenzar: Todos los casos de éxito están cubiertos por el éxito de unify_with_occurs_check(X,Y) . Lo que queda por hacer es la distinción entre falla NSTO y casos de error STO. Eso es cuando las cosas empiezan a ser difíciles ...

Answer 1

En SWI-prolog:

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

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

da los siguientes resultados:

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

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

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

Answer 2

Aquí va mi intento:

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([], []).

Primero trata de unify_with_occurs_check , y si no tiene éxito, entonces procede a construir un término más general para cada argumento, luego trata de unificar tal término y probar para ver si es cíclico. Si es cíclica, se type_error un type_error del tipo type_error .

P.ej:

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

Answer 3

Aquí va otro intento:

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([], [], [], []).

Primero intenta unificar_con_aviso_de_cceso, y si no tiene éxito, entonces procede a construir dos términos más generales, atravesando la estructura de cada término.

• Si cualquiera de los términos es una variable, deja ambos términos como están.
• Si ambos términos son del mismo átomo, o si ambos son términos compundidos con el mismo funtor y arity [*], atraviesa sus argumentos y hace un término más general para ellos.
• De lo contrario, asigna una nueva variable nueva a cada término.

Luego intenta de nuevo unificar_con_cuestiones_compruebe los términos más generales para probar la unificación acíclica y arrojar un error en consecuencia.

[*] La prueba de arity en términos de compund se realiza con avidez, ya que term_general1/4 fallará la recursión ya que OP declaró que solo usaría predicados incorporados definidos en la parte 1 de este enlace con does not include length/2 . . ( editado: se agregaron dos llamadas a functor/3 para probar Functor y Arity antes de llamar a term_general1, para no intentar inspeccionar los términos internos si su arity no coincide)

P.ej:

?- 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))''

Editar 02/06/2015:

La solución anterior falla para la consulta:

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

es que no produce un error de unificación.

Aquí hay una mejora sobre el algoritmo que trata con cada uno de los subterm por parejas y produce el error tan pronto como lo descubre:

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([], [], _, [], []).

Caso de prueba para la consulta que arrojó resultados incorrectos en la respuesta original:

   ?-  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))''

Answer 4

Tercer intento Esto es principalmente una corrección de errores en una respuesta previa (que ya tenía muchas modificaciones). Editar: 04/06/2015

Al crear un término más general, dejaba los dos subtítulos tal como están, si alguno de ellos era una variable. Ahora construyo un término más general para el "otro" subterráneo en este caso, llamando a 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([], _).

Y aquí las pruebas de unidad mencionadas hasta ahora en esta pregunta:

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.

Answer 5

Aquí está mi versión que usé para probar contra las versiones de @ gusbro. La idea es usar Martelli-Montanari bastante literalmente. Al reescribir una lista de ecuaciones [X1=Y1,X2=Y2|Etc] , ciertas reglas de reescritura se aplican inmediatamente - ¡utilizando! por compromiso Y para ciertas reglas no estaba tan seguro, así que los dejé como no determinados como el algoritmo original.

rewrite_sto/1 que rewrite_sto/1 fallará o producirá un error. No estamos interesados ​​en el caso de éxito, que se maneja sin ninguna búsqueda. ¡Además, observe que una ecuación que conduce a una falla (inmediata) puede eliminarse! Eso es poco intuitivo, pero aquí solo nos interesa encontrar casos de 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), _))
   ).