sentencia - ¿Cómo definir(y nombrar) los predicados de comparación de términos seguros correspondientes en ISO Prolog?

reglas en prolog (8)

¡Qué diablos ! ¡Le daré una oportunidad, también!

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

Algunas cosas más auxiliares:

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

Vamos a tener algunas pruebas (con 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

Editar 2015-05-06

Se modificó la implementación de lt/2 para usar T_alpha y T_omega , no dos variables nuevas .

lt(X,Y) hace dos copias de X ( X1 y X2 ) y dos copias de Y ( Y1 e Y2 ).
Las variables compartidas de X e Y también son compartidas por X1 e Y1 , y por X2 e Y2 .
T_alpha viene antes que todos los demás términos (en X1 , X2 , Y1 , Y2 ) con el orden estándar.
T_omega viene después de todos los demás términos en el orden estándar.
En los términos copiados, las variables que están en X pero no en Y (y viceversa) se unifican con T_alpha / T_omega .
- Si esto tiene un impacto en el orden de los términos, aún no podemos decidir el orden.
- Si no es así , terminamos.

Ahora, el contraejemplo dado por @false funciona:

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

El orden de los términos estándar (ISO / IEC 13211-1 7.2 orden de los términos) se define en todos los términos, incluidas las variables. Si bien hay buenos usos para esto, piense en la implementación de setof/3 , esto hace que muchos usos limpios y lógicos de los built-ins en 8.4 Term comparen una pesadilla declarativa con imps (forma corta para constructos imperativos) a su alrededor. 8.4 Características de comparación de términos:

8.4 Comparación de términos
8.4.1 (@ = <) / 2, (==) / 2, (/ ==) / 2, (@ <) / 2, (@>) / 2, (@> =) / 2.
8.4.2 compare/3 .
8.4.3 sort/2 .
8.4.4 keysort/2 .

Para dar un ejemplo, considere:

?- X @< a. true.

Esto tiene éxito, porque

7.2 Orden de término
Un orden de term_precedes (3.181) define si o
no es un término X término-precede un término Y
Si X e Y son términos idénticos, X term_precedes Y
y Y term_precedes X son ambos falsos.
Si X e Y tienen diferentes tipos: X term_precedes Y iff the
el tipo de X precede al tipo de Y en el siguiente orden:
variable precede al floating point precede al integer
precede al atom precede al compound .
NOTA: predicados incorporados que prueban el orden de los términos
se definen en 8.4.
...

Y así todas las variables son más pequeñas que a . Pero una vez que X es instanciado:

?- X @< a, X = a. X = a.

el resultado se vuelve inválido

Entonces ese es el problema. Para superar esto, uno puede usar restricciones, o apegarse al comportamiento central solamente y por lo tanto producir un instantiation_error .

7.12.2 Clasificación de error
Los errores se clasifican según la forma de Error_term :
a) Habrá un Error de instanciación cuando
argumento o uno de sus componentes es una variable, y una
Se requiere un argumento o componente instanciado. Tiene
el formulario instantiation_error .

De esta manera, sabemos con certeza que un resultado está bien definido siempre que no se produzca un error de instanciación.

Para (/==)/2 , ya existe dif/2 que utiliza restricciones o iso_dif/2 que produce un error de instanciación limpia.

iso_dif(X, Y) :- X /== Y, ( X /= Y -> true ; throw(error(instantiation_error,iso_dif/2)) ).

Entonces, ¿de qué se trata mi pregunta? ¿Cómo definir (y nombrar) los predicados de comparación de términos seguros correspondientes en ISO Prolog ? Idealmente, sin ningún cruce de términos explícito. Tal vez para aclarar: por encima de iso_dif/2 no se utiliza ningún iso_dif/2 términos explícito. Ambos (/==)/2 y (/=)/2 atraviesan el término internamente, pero los gastos generales para esto son extremadamente bajos en comparación con el recorrido explícito con (=..)/2 o functor/3, arg/3 .

Aquí hay un boceto de lo que creo que podría ser un enfoque de trabajo. Considere la meta lt(X, Y) y term_variables(X, XVars), term_variables(Y, YVars) .

El propósito de la definición es determinar si una instanciación adicional puede cambiar el orden de los términos (7.2). Entonces, es posible que deseemos averiguar las variables responsables directamente. Como term_variables/2 atraviesa un término de la misma manera que es relevante para el orden de término, se cumple lo siguiente:

Si hay una creación de instancias que cambia el orden de los términos, entonces las variables que se deben instanciar para atestiguar que el cambio se encuentra en la lista hace XCs , YCs de XVars y YVars , respectivamente, y

XCs , YCs , XVars e YVars son idénticos, o
XCs y YCs son idénticos hasta el último elemento, o
XCs y YCs son idénticos hasta el final, donde una lista tiene un elemento adicional, y la otra lista es idéntica a su correspondiente lista de variables XVars o YVars .

Como un caso especial interesante, si los primeros elementos en XVars e YVars difieren, entonces esas son las únicas variables que se probarán para determinar su relevancia. Entonces esto incluye el caso donde no hay una variable común, pero es incluso más general que eso.

En esta respuesta, presentamos el predicado safe_term_less_than/2 , un análogo monotónico del predicado safe_term_less_than/2 iso-prolog (@<)/2 (§8.4.1, "término menor que"). Sus principales propiedades son:

Recorrido explícito de términos recursivos.
Basado en prolog-coroutining instalaciones prolog-coroutining , en particular when/2 .
- La comparación puede progresar gradualmente :
  - "congelar" cuando la creación de instancias no sea suficiente
  - "despertar" cada vez que cambie la instanciación de los términos más significativos
- La línea de frente actual de la comparación se representa como una pila explícita (LIFO).
- El estado actual se pasa directamente alrededor de los objetivos residuales.

El siguiente código ha sido desarrollado y probado en sicstus-prolog versión 4.3.2:

safe_term_less_than(L, R) :- % exported predicate i_less_than_([L-R]).

La definición anterior de safe_term_less_than/2 se basa en los siguientes predicados auxiliares:

i_less_than_([L-R|LRs]) :- Cond = (?=(L,R) ; nonvar(L),nonvar(R)), when/2(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).

Consultas de muestra:

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

En comparación con las respuestas anteriores, observamos:

El "volumen de texto" de los objetivos residuales parece algo "hinchado".
La consulta ?- safe_term_less_than(X+2, Y+1), X = Y. falla, ¡justo como debería!

Esta no es una respuesta completamente original, ya que se basa en la answer de @coredump.

Hay un tipo de consultas lt/2 (la implementación de referencia que realiza el recorrido de términos explícito) no responde correctamente:

| ?- lt(b(b), a(a,a)). no | ?- @<(b(b), a(a,a)). yes

La razón es que el orden estándar de los términos considera la aridad antes de comparar los nombres de los funtores.

En segundo lugar, lt/2 no siempre lanza un instatiation_error cuando se trata de comparar variables:

| ?- lt(a(X), a(Y)). no

Escribo aquí otro candidato para una implementación explícita de referencia:

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

El predicado lt_args(Xs, Ys) es verdadero cuando hay un par de argumentos correspondientes Xi , Yi tales que lt(Xi, Yi) y Xj == Yj para todos los pares anteriores Xj , Yj (por ejemplo lt_args([a,X,a(X),b|_], [a,X,a(X),c|_]) es verdadero).

Algunas consultas de ejemplo:

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

Esta respuesta sigue a la anterior que presentó safe_term_less_than/2 .

¿Que sigue? Una variante segura de compare -inicialmente llamada scompare/3 :

scompare(Ord, L, R) :- i_scompare_ord([L-R], Ord). i_scompare_ord([], =). i_scompare_ord([L-R|Ps], X) :- when/2((?=(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) ) ).

Los predicados term_itype/2 y args_args_paired//2 son los mismos que se han definido anteriormente .

iso_dif/2 es mucho más fácil de implementar que una comparación:

El operador incorporado /= está disponible
Ahora usted exactamente qué argumentos debe proporcionar a /=

Definición

Según sus comentarios, la comparación segura significa que la orden no cambiará si las variables en ambos subtítulos son instanciadas. Si nombramos la comparación lt , tenemos por ejemplo:

lt(a(X), b(Y)) : siempre se cumple para todos los X e Y, porque a @< b
lt(a(X), a(Y)) : no lo sabemos con certeza: intanciation_error
lt(a(X), a(X)) : siempre falla, porque X @ <X falla

Como se dijo en los comentarios, desea lanzar un error si, al hacer un recorrido de ambos términos lado a lado, el primer par de términos (potencialmente) discriminativo contiene:

dos variables no idénticas ( lt(X,Y) )
una variable y una no variable ( lt(X,a) o lt(10,Y) )

Pero primero, repasemos los posibles enfoques que no quiere usar:

Defina una función de comparación de término-cruce explícito. Sabía que preferiría no hacerlo, por razones de rendimiento, pero aún así, este es el enfoque más directo. Recomiendo hacerlo de todos modos, para que tenga una implementación de referencia para comparar con otros enfoques.
Use restricciones para tener una comparación demorada: no sé cómo hacerlo usando ISO Prolog, pero con, por ejemplo, ECLiPSe, suspendería la comparación real sobre el conjunto de variables term_variables/2 (usando term_variables/2 ), hasta que no haya más variables. Previamente, también sugerí usar el predicado coroutine/0 , pero pasé por alto el hecho de que no influye en el operador @< (solo < ).
Este enfoque no aborda exactamente el mismo problema que usted describe, pero está muy cerca. Una ventaja es que no lanza una excepción si los valores eventuales dados a las variables satisfacen la comparación, mientras que arroja uno cuando no sabe de antemano.

Recorrido de término explícito (implementación de referencia)

Aquí hay una implementación del enfoque de término explícito para lt , la versión segura de @< . Por favor revísalo para verificar si esto es lo que esperas. Podría haber perdido algunos casos. No estoy seguro de si esto se ajusta a ISO Prolog, pero eso también se puede arreglar, si lo desea.

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

(Editar: teniendo en cuenta las observaciones de Tudor Berariu: (i) falta el caso de error var / var, (ii) ordena primero por aridad; además, arreglar (i) me permite eliminar subsumes_term por listas. Gracias.)

Atraso de términos implícitos (no funciona)

Aquí está mi intento de lograr el mismo efecto sin desestructurar los términos.

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

Razón fundamental

Supongamos que X @< Y tiene éxito. Queremos verificar que la relación no dependa de algunas variables no inicializadas. Entonces, produzco las copias respectivas X2 e Y2 de X e Y , donde se instancian todas las variables:

En X2 , las variables se unifican con 1.
En Y2 , las variables se unifican con 0.

Entonces, si la relación X2 @< Y2 aún se mantiene, sabemos que no dependemos del orden de términos estándar entre las variables. De lo contrario, lanzamos una excepción, porque significa que una relación 1 @< 0 , que previamente no estaba ocurriendo, hizo que la relación fallara.

Deficiencias

(basado en los comentarios de OP)

lt(X+a,X+b) debería tener éxito pero producir un error.
A primera vista, uno puede pensar que las variables unificadoras que ocurren en ambos términos con el mismo valor, digamos val , pueden arreglar la situación. Sin embargo, puede haber otras ocurrencias de X en los términos comparados donde esto conduzca a un juicio erróneo.
lt(X,3) debería producir un error pero tiene éxito.
Para arreglar ese caso, uno debe unificar X con algo que sea mayor que 3. En el caso general, X debe tomar un valor que sea mayor que cualquier otro término posible ¹ . Dejando a un lado las limitaciones prácticas, la relación @< no tiene un máximo: los términos compuestos son mayores que los compuestos no compuestos, y por definición, los términos compuestos se pueden hacer arbitrariamente grandes.

Entonces, ese enfoque no es concluyente y no creo que pueda corregirse fácilmente.

1 : Nótese que para cualquier término dado, sin embargo, podríamos encontrar los términos máximos y mínimos locales, que serían suficientes para el propósito de la pregunta.

¡Próximo! Esto debería funcionar mejor que mi intento anterior :

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

El auxiliar maybe_unify/2 trata con variables que ocurren tanto en X como en Y :

maybe_unify(K,X) :- ( var(X) -> X = K ; true ).

Comprobando con GNU-Prolog 1.4.4:

¡Tercer intento! Desarrollado y probado con GNU Prolog 1.4.4.

Exhibición ''A'': "tan simple como sea posible"

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

Anexo ''B'': " no hay necesidad de etiquetar todos los vars "

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

Algunos códigos compartidos:

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