prolog - Reificación de la igualdad/desigualdad de términos

prolog-dif (6)

Los programas Pure Prolog que distinguen entre la igualdad y la desigualdad de términos de una manera limpia sufren ineficiencias de ejecución; incluso cuando todos los términos de relevancia se basan.

Un ejemplo reciente en SO es esta respuesta . Todas las respuestas y todas las fallas son correctas en esta definición. Considerar:

?- Es = [E1,E2], occurrences(E, Es, Fs). Es = Fs, Fs = [E, E], E1 = E2, E2 = E ; Es = [E, E2], E1 = E, Fs = [E], dif(E, E2) ; Es = [E1, E], E2 = E, Fs = [E], dif(E, E1) ; Es = [E1, E2], Fs = [], dif(E, E1), dif(E, E2).

Si bien el programa es perfecto desde un punto de vista declarativo, su ejecución directa en sistemas actuales como B, SICStus, SWI, YAP es innecesariamente ineficiente. Para el siguiente objetivo, se deja abierto un punto de opción para cada elemento de la lista.

?- occurrences(a,[a,a,a,a,a],M). M = [a, a, a, a, a] ; false.

Esto se puede observar usando una lista de s suficientemente grande como se muestra a continuación. Es posible que deba adaptar el I modo que la lista pueda representarse; en SWI esto significaría que

1mo el I debe ser lo suficientemente pequeño para evitar un error de recursos para la pila global como el siguiente:

?- 24=I,N is 2^I,length(L,N), maplist(=(a),L). ERROR: Out of global stack

2do el I debe ser lo suficientemente grande como para provocar un error de recurso para la pila local:

?- 22=I,N is 2^I,length(L,N), maplist(=(a),L), ( Length=ok ; occurrences(a,L,M) ). I = 22, N = 4194304, L = [a, a, a, a, a, a, a, a, a|...], Length = ok ; ERROR: Out of local stack

Para superar este problema y aún conservar las agradables propiedades declarativas, se necesita un predicado de comparación.

¿Cómo debe definirse este predicado de comparación?

Aquí hay una posible definición:

equality_reified(X, X, true). equality_reified(X, Y, false) :- dif(X, Y).

Editar: Tal vez el orden de los argumentos debe invertirse de manera similar a la compare/3 incorporada de ISO compare/3 (enlaces de enlace a borrador solamente).

Una implementación eficiente de la misma manejaría primero los casos rápidos determinados:

equality_reified(X, Y, R) :- X == Y, !, R = true. equality_reified(X, Y, R) :- ?=(X, Y), !, R = false. % syntactically different equality_reified(X, Y, R) :- X /= Y, !, R = false. % semantically different equality_reified(X, X, true). equality_reified(X, Y, false) :- dif(X, Y).

Editar: no me queda claro si X /= Y es un guardia adecuado en presencia de restricciones. Sin restricciones ?=(X, Y) o X /= Y son lo mismo.

Ejemplo

Como lo sugirió @ user1638891, aquí hay un ejemplo de cómo se podría usar una primitiva. El código original por esteras fue:

occurrences_mats(_, [], []). occurrences_mats(X, [X|Ls], [X|Rest]) :- occurrences_mats(X, Ls, Rest). occurrences_mats(X, [L|Ls], Rest) :- dif(X, L), occurrences_mats(X, Ls, Rest).

Que puede ser reescrito a algo así como:

occurrences(_, [], []). occurrences(E, [X|Xs], Ys0) :- reified_equality(Bool, E, X), ( Bool == true -> Ys0 = [X|Ys] ; Ys0 = Ys ), % ( Bool = true, Ys0 = [X|Ys] ; Bool = true, Ys0 = Ys ), occurrences(E, Xs, Ys). reified_equality(R, X, Y) :- X == Y, !, R = true. reified_equality(R, X, Y) :- ?=(X, Y), !, R = false. reified_equality(true, X, X). reified_equality(false, X, Y) :- dif(X, Y).

Tenga en cuenta que la indexación del segundo argumento de SWI solo se activa, después de ingresar una consulta como occurrences(_,[],_) . Además, SWI necesita el if-entonces-else intrínsecamente no monótono, ya que no indexa en (;)/2 - disyunción. SICStus lo hace, pero solo tiene una indexación de primer argumento. Entonces deja un (1) punto de elección abierto (al final con [] ).

ACTUALIZACIÓN: esta respuesta ha sido reemplazada por la mía del 18 de abril. No propongo que se elimine debido a los comentarios a continuación.

Mi respuesta anterior fue incorrecta. El siguiente se ejecuta contra el caso de prueba en la pregunta y la implementación tiene la característica deseada de evitar puntos de elección superfluos. Supongo que el modo de predicado superior es?, + ,? aunque otros modos podrían implementarse fácilmente.

El programa tiene 4 cláusulas en total: se visita la lista en el segundo argumento y para cada miembro hay dos posibilidades: o se unifica con el primer argumento del predicado superior o es diferente de él, en cuyo caso se aplica una restricción de dif :

occurrences(X, L, Os) :- occs(L, X, Os). occs([],_,[]). occs([X|R], X, [X|ROs]) :- occs(R, X, ROs). occs([X|R], Y, ROs) :- dif(Y, X), occs(R, Y, ROs).

Se ejecuta una muestra, usando YAP:

?- occurrences(1,[E1,1,2,1,E2],Fs). E1 = E2 = 1, Fs = [1,1,1,1] ? ; E1 = 1, Fs = [1,1,1], dif(1,E2) ? ; E2 = 1, Fs = [1,1,1], dif(1,E1) ? ; Fs = [1,1], dif(1,E1), dif(1,E2) ? ; no ?- occurrences(E,[E1,E2],Fs). E = E1 = E2, Fs = [E,E] ? ; E = E1, Fs = [E], dif(E,E2) ? ; E = E2, Fs = [E], dif(E,E1) ? ; Fs = [], dif(E,E1), dif(E,E2) ? ; no

Aquí hay una implementación aún más corta, lógica y pura de occurrences/3 .

Lo construimos sobre el meta-predicate tfilter/3 , el término reificado igualdad de predicado (=)/3 , y la corutina allEqual_to__lazy/2 (definida en mi respuesta anterior a esta pregunta):

occurrences(E,Xs,Es) :- allEqual_to__lazy(Es,E), tfilter(=(E),Xs,Es).

¡Hecho! Para facilitar la comparación, volvimos a ejecutar exactamente las mismas consultas que utilicé en mi respuesta anterior:

?- Fs = [1,2], occurrences(E,Es,Fs). false. ?- occurrences(E,[1,2,3,1,2,3,1],Fs). Fs = [1,1,1], E=1 ; Fs = [2,2], E=2 ; Fs = [3,3], E=3 ; Fs = [], dif(E,1), dif(E,2), dif(E,3). ?- occurrences(1,[1,2,3,1,2,3,1],Fs). Fs = [1,1,1]. ?- Es = [E1,E2], occurrences(E,Es,Fs). Es = [E, E ], Fs = [E,E], E1=E , E2=E ; Es = [E, E2], Fs = [E], E1=E , dif(E2,E) ; Es = [E1,E ], Fs = [E], dif(E1,E), E2=E ; Es = [E1,E2], Fs = [], dif(E1,E), dif(E2,E). ?- occurrences(1,[E1,1,2,1,E2],Fs). E1=1 , E2=1 , Fs = [1,1,1,1] ; E1=1 , dif(E2,1), Fs = [1,1,1] ; dif(E1,1), E2=1 , Fs = [1,1,1] ; dif(E1,1), dif(E2,1), Fs = [1,1]. ?- occurrences(1,L,[1,2]). false. ?- L = [_|_],occurrences(1,L,[1,2]). false. ?- L = [X|X],occurrences(1,L,[1,2]). false. ?- L = [L|L],occurrences(1,L,[1,2]). false.

Por fin, la consulta más general:

?- occurrences(E,Es,Fs). Es = Fs, Fs = [] ; Es = Fs, Fs = [E] ; Es = Fs, Fs = [E,E] ; Es = Fs, Fs = [E,E,E] % ... and so on ad infinitum ...

Obtenemos las mismas respuestas.

Bueno, para empezar, el nombre debería ser más declarativo, como equality_truth/2 .

El siguiente código se basa en if_/3 y (=)/3 (también equal_truth/3 como equal_truth/3 ), implementado por @false en la unión de Prolog para AUBUC :

=(X, Y, R) :- X == Y, !, R = true. =(X, Y, R) :- ?=(X, Y), !, R = false. % syntactically different =(X, Y, R) :- X /= Y, !, R = false. % semantically different =(X, Y, R) :- R == true, !, X = Y. =(X, X, true). =(X, Y, false) :- dif(X, Y). if_(C_1, Then_0, Else_0) :- call(C_1, Truth), functor(Truth,_,0), % safety check ( Truth == true -> Then_0 ; Truth == false, Else_0 ).

Comparado con las occurrences/3 , las occurrences_aux/3 auxiliares usan un orden de argumento diferente que pasa la lista Es como el primer argumento, que puede habilitar la indexación del primer argumento:

occurrences_aux([], _, []). occurrences_aux([X|Xs], E, Ys0) :- if_(E = X, Ys0 = [X|Ys], Ys0 = Ys), occurrences_aux(Xs, E, Ys).

Como señala @migfilg, el objetivo Fs=[1,2], occurrences_aux(Es,E,Fs) debería fallar, ya que es lógicamente falso: occurrences_aux(_,E,Fs) establece que todos los elementos en Fs son iguales a E Sin embargo, en sí mismo, occurrences_aux/3 no termina en casos como este.

Podemos usar un predicado auxiliar allEqual_to__lazy/2 para mejorar el comportamiento de terminación:

allEqual_to__lazy(Xs,E) :- freeze(Xs, allEqual_to__lazy_aux(Xs,E)). allEqual_to__lazy_aux([],_). allEqual_to__lazy_aux([E|Es],E) :- allEqual_to__lazy(Es,E).

Con todos los predicados auxiliares en su lugar, definamos occurrences/3 :

occurrences(E,Es,Fs) :- allEqual_to__lazy(Fs,E), % enforce redundant equality constraint lazily occurrences_aux(Es,E,Fs). % flip args to enable first argument indexing

Vamos a tener algunas consultas:

?- occurrences(E,Es,Fs). % first, the most general query Es = Fs, Fs = [] ; Es = Fs, Fs = [E] ; Es = Fs, Fs = [E,E] ; Es = Fs, Fs = [E,E,E] ; Es = Fs, Fs = [E,E,E,E] ... % will never terminate universally, but ... % that''s ok: solution set size is infinite ?- Fs = [1,2], occurrences(E,Es,Fs). false. % terminates thanks to allEqual_to__lazy/2 ?- occurrences(E,[1,2,3,1,2,3,1],Fs). Fs = [1,1,1], E=1 ; Fs = [2,2], E=2 ; Fs = [3,3], E=3 ; Fs = [], dif(E,1), dif(E,2), dif(E,3). ?- occurrences(1,[1,2,3,1,2,3,1],Fs). Fs = [1,1,1]. % succeeds deterministically ?- Es = [E1,E2], occurrences(E,Es,Fs). Es = [E, E], Fs = [E,E], E1=E , E2=E ; Es = [E, E2], Fs = [E], E1=E , dif(E2,E) ; Es = [E1, E], Fs = [E], dif(E1,E), E2=E ; Es = [E1,E2], Fs = [], dif(E1,E), dif(E2,E). ?- occurrences(1,[E1,1,2,1,E2],Fs). E1=1 , E2=1 , Fs = [1,1,1,1] ; E1=1 , dif(E2,1), Fs = [1,1,1] ; dif(E1,1), E2=1 , Fs = [1,1,1] ; dif(E1,1), dif(E2,1), Fs = [1,1].

Editar 2015-04-27

Algunas consultas más para probar si las occurrences/3 universales terminan en ciertos casos:

?- occurrences(1,L,[1,2]). false. ?- L = [_|_],occurrences(1,L,[1,2]). false. ?- L = [X|X],occurrences(1,L,[1,2]). false. ?- L = [L|L],occurrences(1,L,[1,2]). false.

La implementación de occurrences/3 continuación se basa en mis respuestas anteriores, es decir, aprovechando el mecanismo de indización de cláusulas en el primer argumento para evitar algunos puntos de elección y aborda todos los problemas planteados.

Además, hace frente a un problema en todas las implementaciones enviadas hasta ahora, incluido el referido en la pregunta, es decir, que todas ingresan un bucle infinito cuando la consulta tiene los dos primeros argumentos libres y la tercera una lista con diferentes elementos de tierra. El comportamiento correcto es fallar, por supuesto.

Uso de un predicado de comparación

Creo que para evitar puntos de elección no utilizados y mantener un buen grado de declaratividad de implementación no hay necesidad de un predicado de comparación como el propuesto en la pregunta, pero estoy de acuerdo en que esto puede ser una cuestión de gusto o inclinación.

Implementación

Tres casos exclusivos se consideran en este orden: si el segundo argumento se basa, se lo visita recursivamente; de lo contrario, si el tercer argumento se basa, se verifica y luego se visita recursivamente; de lo contrario, se generan listas adecuadas para los argumentos segundo y tercero.

occurrences(X, L, Os) :- ( nonvar(L) -> occs(L, X, Os) ; ( nonvar(Os) -> check(Os, X), glist(Os, X, L) ; v_occs(L, X, Os) ) ).

La visita al suelo El segundo argumento tiene tres casos cuando la lista no está vacía: si su encabezado y X arriba son ambos molidos y unificables X está en la cabeza de la lista resultante de ocurrencias y no hay otra alternativa; de lo contrario, hay dos alternativas con X siendo diferente de la cabeza o unificando con ella:

occs([],_,[]). occs([X|R], Y, ROs) :- ( X==Y -> ROs=[X|Rr] ; foccs(X, Y, ROs, Rr) ), occs(R, Y, Rr). foccs(X, Y, ROs, ROs) :- dif(X, Y). foccs(X, X, [X|ROs], ROs).

Verificar el tercer argumento de la tierra consiste en asegurarse de que todos sus miembros se unifican con X En principio, glist/3 podría realizar esta comprobación, pero de esta forma se evitan los puntos de elección no utilizados.

check([], _). check([X|R], X) :- check(R, X).

La visita al tercer argumento de la tierra con un segundo argumento libre debe terminar agregando variables diferentes de X a la lista generada. En cada paso de recursión hay dos alternativas: el encabezado actual de la lista generada es el encabezado actual de la lista visitada, que debe ser unificable con X o es una variable libre diferente de X Esta es una descripción solo teórica porque de hecho hay un número infinito de soluciones y la tercera cláusula nunca se alcanzará cuando el encabezado de la lista sea una variable. Por lo tanto, la tercera cláusula siguiente está comentada para evitar puntos de elección inutilizables.

Finalmente, el caso donde todos los argumentos son gratuitos se trata de una manera similar al caso anterior y teniendo un problema similar de algunos patrones de solución que no se generan en la práctica:

v_occs([], _, []). v_occs([X|R], X, [X|ROs]) :- v_occs(R, X, ROs). %% v_occs([X|R], Y, ROs) :- dif(Y, X), v_occs(R, Y, ROs). % never used

Pruebas de muestra

?- occurrences(1,[E1,1,2,1,E2],Fs). Fs = [1,1], dif(E1,1), dif(E2,1) ? ; E2 = 1, Fs = [1,1,1], dif(E1,1) ? ; E1 = 1, Fs = [1,1,1], dif(E2,1) ? ; E1 = E2 = 1, Fs = [1,1,1,1] ? ; no ?- occurrences(1,L,[1,2]). no ?- occurrences(1,L,[1,E,1]). E = 1, L = [1,1,1] ? ; E = 1, L = [1,1,1,_A], dif(1,_A) ? ; E = 1, L = [1,1,1,_A,_B], dif(1,_A), dif(1,_B) ? ; ...

Parece que lo mejor es llamar a este predicado con los mismos argumentos (=)/3 . De esta manera, las condiciones como if_/3 ahora son mucho más legibles. Y para usar más bien el sufijo _t en lugar de _truth :

memberd_t(_X, [], false). memberd_t(X, [Y|Ys], Truth) :- if_( X = Y, Truth=true, memberd_t(X, Ys, Truth) ).

Que solía ser:

memberd_truth(_X, [], false). memberd_truth(X, [Y|Ys], Truth) :- if_( equal_truth(X, Y), Truth=true, memberd_truth(X, Ys, Truth) ).