prolog - different/2-¿existe una definición pura y determinada?

prolog-dif logical-purity (8)

¡Aquí hay otro intento! Utilizamos el constructo de control monótona if-then-else if_/3 , en combinación con el predicado de membresía de la lista memberd_t/3 , y la indexación del primer argumento para evitar la creación de puntos de opción inútiles.

different(Xs,Ys) :- different_aux(Xs,Ys,Xs,Ys). different_aux([],[_|_],Xs0,Ys0) :- different_aux(Ys0,[],Ys0,Xs0). % swap Xs/Ys pair different_aux([X|Xs],Ys,Xs0,Ys0) :- if_(memberd_t(X,Ys0), different_aux(Ys,Xs,Ys0,Xs0), % variant: different_aux(Xs,Ys,Xs0,Ys0) true).

Primero, ejecutamos una consulta que esperamos fallar :

?- different([1,2,3],[2,3,1]). false.

Las siguientes consultas son similares a la consulta de error dada anteriormente; cada uno tiene un solo elemento "diferente" x colocado en diferentes índices en el primer [1,2,3] o en el segundo listado [2,3,1] :

?- different([4,2,3],[2,3,1]), different([1,2,3],[4,3,1]), different([1,4,3],[2,3,1]), different([1,2,3],[2,4,1]), different([1,2,4],[2,3,1]), different([1,2,3],[2,3,4]). true. % all subgoals succeed deterministically

¡DE ACUERDO! Vamos a ejecutar otra consulta (bastante general) que utilicé en mi respuesta anterior :

?- different([A,B],[X,Y]). A=X , B=X , dif(Y,X) ; A=X , dif(B,X), dif(Y,B) ; A=Y , dif(B,X), dif(Y,X) ; dif(A,X), dif(A,Y).

¡Compacto! ¡Una gran mejora sobre lo que presenté antes !

different(Xs, Ys) :- member(X, Xs), non_member(X, Ys). different(Xs, Ys) :- member(Y, Ys), non_member(Y, Xs).

Si bien esta definición que usa member/2 y non_member/2 es casi ¹ perfecta desde un punto de vista declarativo, produce soluciones redundantes para ciertas consultas y deja puntos de elección alrededor.

¿Qué es una definición que mejora esto (de una manera pura, probablemente usando if_/3 y (=)/3 ) de manera que exactamente el mismo conjunto de soluciones se describe por different/2 pero está determinado al menos para las consultas de campo (por lo tanto, no dejar abiertos los puntos de elección inútiles) y omite (si es posible) cualquier respuesta redundante?

¹ _{En realidad, different([a|nonlist],[]), different([],[b|nonlist]) éxito.} _{Podría igualmente fallar.} _{Entonces, una solución que falla para ambos está bien (quizás incluso más fina).}

¡Primer intento!

El siguiente código se basa en los metadatos tfilter/3 y tpartition/4 , el constructo de control monótona if-then-else if_/3 , el conectivo lógico not_t/3 reificado not_t/3 y el predicado de igualdad del término reificado if_/3 :

different([],[_|_]). different([X|Xs0],Ys0) :- tpartition(=(X),Ys0,Es,Ys1), if_(Es=[], true, (tfilter(not_t(=(X)),Xs0,Xs1),different(Xs1,Ys1))).

Consulta de muestra:

?- different([A,B],[X,Y]). A=Y , dif(B,Y), X=Y ; A=X , B=X , dif(X,Y) ; A=X , dif(B,X), dif(B,Y), dif(X,Y) ; A=Y , B=Y , dif(X,Y) ; A=Y , dif(B,X), dif(B,Y), dif(X,Y) ; dif(A,X), dif(A,Y).

Observemos el determinismo cuando trabajamos con datos de tierra:

?- different([5,4],[1,2]). true.

El enfoque anterior se siente como un paso en la dirección correcta ... Pero, tal como está, no lo llamaría perfecto.

(Muy inspirado por la última respuesta de @ repeat, los nombres siguen siendo demasiado torpes)

different(Xs, Ys) :- if_(tnotexists_inlist_t(list_memberd_t(Ys), Xs), true, tnotexists_inlist_t(list_memberd_t(Xs), Ys)). tnotexists_inlist_t(_P_2, [], false). tnotexists_inlist_t(P_2, [E|Es], T) :- if_(call(P_2, E), tnotexists_inlist_t(P_2, Es, T), T = true).

Conerning soluciones que utilizan if_ , yo diría que un enfoque alternativo sería utilizar la negación constructiva desde el principio. La negación constructiva ya se investigó en los años 80, un pionero fue David Chan, y aún aparece de vez en cuando.

Supongamos que tenemos un intérprete Prolog que tiene una negación constructiva (~)/2 . Esta negación constructiva (~)/2 se puede usar para definir un if-entonces-else declarativo de la siguiente manera, vamos a llamar a este operador (~->)/2 :

(A ~-> B; C) :- (A, B); (~A, C).

Si el intérprete de Prolog también ha incorporado la implicación (=>)/2 además de la negación constructiva, uno podría definir alternativamente un declarativo if-then-else de la siguiente manera, llamemos a este operador (~=>)/2 :

(A ~=> B; C) :- (A => B), (~A => C).

Tenga en cuenta el cambio de disyunción (;)/2 a conjunción (,)/2 . Pregúntele a las personas del Diagrama Binario de Decisiones (BDD) por qué son lógicamente equivalentes. Procesalmente hay matices, pero a través de la puerta trasera de la implicación implícita para cierta A, la segunda variante de si-entonces-más también introducirá la no determinación.

Pero, ¿cómo podríamos hacer e introducir, por ejemplo, la negación constructiva en un intérprete de Prolog? Una manera directa sería delegar la negación constructiva a un solucionador de restricciones. Si el solucionador de restricciones ha reificado la negación, esto se puede hacer de la siguiente manera:

~ A :- #/ A.

Pero no hay tantos solucionadores de restricciones alrededor, que permitirían un uso sensato para ejemplos como member/2 etc. Dado que a menudo proporcionan negación reificada solo para dominios tales como enteros finitos, racionales, etc. Pero para un predicado como member/2 necesitaríamos una negación reificada para el universo de Herbrand.

También tenga en cuenta que los enfoques habituales para la negación constructiva también suponen que la implicación de la regla ordinaria obtiene otra lectura. Esto significa que generalmente bajo negación constructiva, podríamos elegir la definición ordinaria de member/2 y obtener resultados de consulta tales como:

?- ~ member(X, [a,b,c]). dif(X, a), dif(X, b), dif(X, c).

Pero de nuevo, la negación cosificada difícilmente funcionará con predicados definidos, por lo que la siguiente consulta probablemente no funcione:

?- #/ member(X, [a,b,c]). /* typically won''t work */

Si lo anterior resulta exitoso que cualquiera de los declarativos if-then-else como (~->)/2 o (~=>)/2 tendrán un uso menos frecuente, ya que las definiciones de predicados ordinarios ya ofrecerán interpretación declarativa por el intérprete Prolog . Pero, ¿por qué la negación constructiva no está muy extendida? Una razón podría ser el gran espacio de diseño de un intérprete Prolog de este tipo. Noté que tendríamos las siguientes opciones:

Encadenamiento hacia atrás: Básicamente escupiríamos el intérprete de vainilla solve/1 en dos predicados solvep/1 y solven/1 . solvep/1 es responsable de resolver los objetivos positivos y solven/1 es responsable de resolver los objetivos negativos. Cuando intentemos esto, tarde o temprano veremos que necesitamos un tratamiento más cuidadoso de los cuantificadores y probablemente terminemos con un método de eliminación de cuantificadores para el dominio de Herbrand.

Forward Chaining: También notaremos que en el encadenamiento hacia atrás nos topamos con problemas para el modelado de cláusulas con disyunción o cuantificador existencial en la cabeza. Esto tiene que ver con el hecho de que el cálculo secuencial adecuado para Prolog tiene solo una fórmula en el lado derecho. Entonces, o vamos multimédica en el lado derecho y perdemos coherencia, o usamos encadenamiento directo.

Conjuntos mágicos: Pero el encadenamiento directo polucionará los espacios de solución de una manera descontrolada. Entonces, podríamos necesitar alguna forma de combinación de encadenamiento hacia adelante y hacia atrás. No me refiero sólo a eso, que deberíamos poder cambiar dinámicamente entre los dos durante el proceso de solución, pero quiero decir que necesitamos también un medio para generar conjuntos que dirijan el proceso de encadenamiento hacia adelante.

También se observan más problemas en esta respuesta here . Esto no significa que tarde o temprano se encontrará una fórmula para ajustar todo este problema y los pares de soluciones juntos, pero podría llevar algo más de tiempo.

Adiós

De regreso a las raíces! Esta variante está muy cerca del código dado por el OP en la pregunta.

Lo siguiente se basa en if_/3 y memberd_t/3 .

different(Xs,Ys) :- if_(some_absent_t(Xs,Ys), true, some_absent_t(Ys,Xs,true)). some_absent_t([] ,_ ,false). some_absent_t([X|Xs],Ys,Truth) :- if_(memberd_t(X,Ys), some_absent_t(Xs,Ys,Truth), Truth=true).

Aquí hay una consulta de tierra:

Y aquí está la consulta (más general) que utilicé en respuestas anteriores:

?- different([A,B],[X,Y]). A=X , B=X , dif(Y,X) ; A=X , dif(B,X), dif(B,Y) ; A=Y , B=Y , dif(Y,X), dif(Y,X) ; A=Y , dif(B,X), dif(B,Y), dif(Y,X) ; dif(A,X), dif(A,Y).

La siguiente recompensa en negrita (+500) fue ofrecida no hace mucho tiempo:

^{Aquí todavía falta una respuesta idiomática.} ^{Por ejemplo, or_t / 3 debería ser más bien (;) / 3.} ^{Hay algo mas.}

¡Desafío aceptado! Esta respuesta es una continuación de esta respuesta previa .

Usamos la conexión lógica reificada (;)/ 3 , que se puede definir así:
'';''(P_1,Q_1,T) :- if_(P_1, T=true, call(Q_1,T)).
A continuación, definimos el meta-predicate call_/1 . Es útil con los predicados reificados utilizados en esta respuesta. Con su nombre y su semántica, ¡ call_/1 sigue if_/3 , and_/2 y or_/2 !
call_(P_1) :- call(P_1,true).
Usando (;)/3 , call_/1 , y some_absent_t/3 implementamos different/2 :
different(As,Bs) :- call_((some_absent_t(As,Bs) ; some_absent_t(Bs,As))).

¡Hecho! Eso es.

Vamos a volver a ejecutar las consultas que usamos en las respuestas anteriores.

^{?- different([5,4],[1,2]).
true.
?- different([1,2,3],[2,3,1]).
false.
?- different([4,2,3],[2,3,1]), different([1,4,3],[2,3,1]), different([1,2,4],[2,3,1]),
different([1,2,3],[4,3,1]), different([1,2,3],[2,4,1]), different([1,2,3],[2,3,4]).
true.}

Las mismas consultas, las mismas respuestas ... ¡Me parece bien !

Llevemos al límite --- con la ayuda de list_nonmember_t/3 , exists_in_t/3 y list_nonmember_t/3 !

some_absent_t(Xs,Ys,Truth) :- exists_in_t(list_nonmember_t(Ys),Xs,Truth). different(Xs,Ys) :- or_(some_absent_t(Xs,Ys), some_absent_t(Ys,Xs)).

Próximo competidor del certamen de belleza del código! -)

Esta respuesta muestra una variación refactorizada del código que se muestra en una respuesta anterior . Utiliza la conjunción y la disyunción reificadas:

and_(P_1,Q_1) :- and_t(P_1,Q_1,true). or_(P_1,Q_1) :- or_t(P_1,Q_1,true). and_t(P_1,Q_1,Truth) :- if_(P_1, call(Q_1,Truth), Truth=false). or_t(P_1,Q_1,Truth) :- if_(P_1, Truth=true, call(Q_1,Truth)).

Tenga en cuenta las dos versiones para "y" y "o"; los que tienen el sufijo _t tienen un argumento adicional para el valor de verdad, los que no tienen el sufijo no lo hacen y asumen que Truth=true debería contener.

En base a and_t/3 y en el predicado de desigualdad de término reificado tpartition/4 , definimos nonmember_t/3 :

nonmember_t(X,Ys,Truth) :- list_nonmember_t(Ys,X,Truth). list_nonmember_t([] ,_, true). list_nonmember_t([Y|Ys],X,Truth) :- and_t(dif(X,Y), list_nonmember_t(Ys,X), Truth).

Ahora, definamos some_absent_t/3 , different_t/3 y different/2 , así:

some_absent_t([] ,_ ,false). some_absent_t([X|Xs],Ys,Truth) :- or_t(nonmember_t(X,Ys), some_absent_t(Xs,Ys), Truth). different_t(Xs,Ys,Truth) :- or_t(some_absent_t(Xs,Ys), some_absent_t(Ys,Xs), Truth). different(Xs,Ys) :- different_t(Xs,Ys,true).

¿Todavía corre ?

?- different([A,B],[X,Y]). A=X , B=X , dif(Y,X) ; A=X , dif(B,X), dif(B,Y) ; A=Y , B=Y , dif(Y,X), dif(Y,X) ; A=Y , dif(B,X), dif(B,Y), dif(Y,X) ; dif(A,X), dif(A,Y). % same result as before ?- different([4,2,3],[2,3,1]), different([1,2,3],[4,3,1]), different([1,4,3],[2,3,1]), different([1,2,3],[2,4,1]), different([1,2,4],[2,3,1]), different([1,2,3],[2,3,4]). true. % same result as before

Se ve bien !

En general, ¡no es una gran mejora con respecto a las respuestas existentes, sino que el código de la OMI es algo más legible, y una versión reificada de different/2 como una bonificación adicional!