Unificación con detección STO

En ISO la unificación Prolog se define solo para aquellos casos que son NSTO (no sujetos a occurs-check). La idea detrás es cubrir aquellos casos de unificaciones que se utilizan 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 occurs-check (STO) y no sujeto
a occurs-check (NSTO)

Un conjunto de ecuaciones (o dos términos) es " sujeto a ocurre -
comprobar" (STO) iff existe una manera de proceder a través
los pasos del algoritmo de Herbrand tales que 7.3.2 g
suceder.

Un conjunto de ecuaciones (o dos términos) " no está sujeto a{[17]]} ocurre-check " (NSTO) iff no existe manera de proceder
a través de los pasos del algoritmo de Herbrand tales que
7.3.2 g sucede.

...

Este paso 7.3.2 g dice:

G) Si hay una ecuación de la forma X = t tales
que X es una variable y t es un no-término variable
que contiene esta variable, luego sale con failure (not
unifiable, se produce positivo-check ).

El algoritmo completo se llama Algoritmo de Herbrand y es lo que comúnmente se conoce como el Algoritmo de unificación Martelli-Montanari - que esencialmente procede reescribiendo conjuntos de ecuaciones en un no determinista{[46]]} manera.

Tenga en cuenta que las nuevas ecuaciones se introducen con:

D) Si hay una ecuación de la forma f(a1,un2, ...a N) =
f(b1,b2, ...bN) luego reemplazarlo por el conjunto de ecuaciones
uni = bi.

Que significa que dos términos compuestos con la misma functor pero diferentes arity nunca va a contribuir a STO-ness.

Esto no-determinismo es lo que hace que el STO-prueba tan difícil de implementar. Después de todo, no es suficiente probar si es necesario o no un occurs-check, sino probar que para 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 NSTO, debe asegurarse de que no hay ruta que podría producir una STO situación. Considere un caso que no es problemático para las implementaciones actuales, pero que sigue siendo STO:

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

Los sistemas Prolog comienzan reescribiendo esta ecuación en: 

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

Ahora, eligen cualquiera{[14]]}

  • 1 = 2 lo que hace que el algoritmo salga con un fallo, o

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

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

  • Si la unificación es SAD, 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 ISO clases de error.

Aquí es un paso sencillo para empezar: 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. Ahí es donde las cosas empiezan a ponerse difíciles...

Author: false, 2015-05-30
Source

5 answers

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

Al crear un término más general, estaba dejando ambos subtemas como están si cualquiera de ellos fuera una variable. Ahora construyo un término más general para el "otro" subterm en este caso, llamando 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 unitarias hasta ahora mencionadas 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.
 15
Author: gusbro,
Warning: date(): Invalid date.timezone value 'Europe/Kyiv', we selected the timezone 'UTC' for now. in /var/www/agent_stack/data/www/ajaxhispano.com/template/agent.layouts/content.php on line 61
2015-06-04 17:33:47

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 unify_with_occurs_check, y si no tiene éxito, entonces procede a construir dos términos más generales, recorriendo 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 el mismo átomo, o si ambos son términos de compund con el mismo funtor y arity [ * ], atraviesa sus argumentos haciendo un más término general para ellos.
  • De lo contrario asigna una nueva variable a cada término.

Luego intenta de nuevo unify_with_occurs_check los términos más generales para probar la unidad acíclica y lanzar un error en consecuencia.

[*] La prueba de aridad en términos de compund se realiza con avidez, ya que term_general1/4 fallará la recursividad como se indica OP para usar solo predicados incorporados definidos en la parte 1 de este enlace con no incluye length/2.. (editado: Añadido dos functor/3 llamadas para probar el funtor y arity antes de llamar a term_general1, para no intentar inspeccionar términos internos si su arity no coincide)

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 06/02/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í va una mejora sobre el algoritmo que se ocupa de cada subterm en pares 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 produjo un error resultados 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))'
 13
Author: gusbro,
Warning: date(): Invalid date.timezone value 'Europe/Kyiv', we selected the timezone 'UTC' for now. in /var/www/agent_stack/data/www/ajaxhispano.com/template/agent.layouts/content.php on line 61
2015-06-02 20:51:46

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 intenta unify_with_occurs_check, y si no tiene éxito, entonces procede a construir un término más general para cada argumento, luego intenta unificar dicho término y probar para ver si es cíclico. Si es cíclico, se lanza un type_error del tipo acíclico.

Ej: 

?- unify_sto(1+A,2+s(A)).
ERROR: Unhandled exception: error(type_error(acyclic,unify(1+_G3620,2+s(_G3620))))
 9
Author: gusbro,
Warning: date(): Invalid date.timezone value 'Europe/Kyiv', we selected the timezone 'UTC' for now. in /var/www/agent_stack/data/www/ajaxhispano.com/template/agent.layouts/content.php on line 61
2015-06-01 21:07:15

Aquí está mi versión que usé para probar con 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-usando el ! por compromiso. Y para ciertas reglas no estaba tan seguro, así que las dejé como no determinadas como el algoritmo original.

Remarca que rewrite_sto/1 fallará o producirá un error. No estamos interesados en el caso de éxito, que se maneja sin ninguna búsqueda. También, observe que una ecuación que conduce al fracaso (inmediato), puede ser eliminado! Eso es un poco intuitivo, pero sólo nos interesan aquí para encontrar STO de los casos.

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), _))
   ).
 7
Author: false,
Warning: date(): Invalid date.timezone value 'Europe/Kyiv', we selected the timezone 'UTC' for now. in /var/www/agent_stack/data/www/ajaxhispano.com/template/agent.layouts/content.php on line 61
2015-06-11 14:36:02

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.
 2
Author: pasaba por aqui,
Warning: date(): Invalid date.timezone value 'Europe/Kyiv', we selected the timezone 'UTC' for now. in /var/www/agent_stack/data/www/ajaxhispano.com/template/agent.layouts/content.php on line 61
2015-05-31 10:17:13