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

Primer intento!

El siguiente código se basa en el meta-predicados tfilter/3 y tpartition/4, la monotonía if-then-else control de construir if_/3, la reificación unario conectivos lógicos not_t/3, y la reificación plazo predicados de igualdad (=)/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 ejemplo:

?- 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 al trabajar 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á, yo no lo llamaría perfecto.

¡Aquí hay otro intento! Utilizamos la construcción de control monótona if-then-elseif_/3, en combinación con el predicado de pertenencia a la lista reificadamemberd_t/3, y primer argumento de indexación para evitar la creación de puntos de elecció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 que falle :

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

Las siguientes consultas son similares a la consulta fallida dada anteriormente; cada una tiene un único elemento" diferente " x colocado en diferentes índices en el primero [1,2,3] o la segunda lista [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

OK! 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 !

(Muy inspirado por @repeat última respuesta , 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).

¡De vuelta a las raíces! Esta variante es muy cercana al código dado por el OP en la pregunta.

El 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:

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

Y aquí está la consulta (más general) que usé 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).

¡Siguiente concursante del concurso de belleza code!-)

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

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 "and" y "or"; las que tienen sufijo _t tienen un argumento adicional para el valor de verdad, las que no tienen el sufijo no y asumen que Truth=true debe mantenerse.

Basado en and_t/3 y en el predicado de desigualdad de término reificadodif/3, 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í: {[14]]}

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

¿Sigue funcionando ?

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

Parece bien !

En general, no es una gran mejora sobre las respuestas existentes, pero IMO código algo más legible, y una versión reificada de different/2 como un bono añadido!

La siguiente bold bounty (+500) se ofreció no hace mucho tiempo:

^{Una respuesta idiomática todavía falta aquí. Por ejemplo, or_t/3 debería ser (;)/3. Hay más que eso.}

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

1. Usamos el conectivo lógico reificado (;)/3, que se puede definir así: {[17]]}

   ';'(P_1,Q_1,T) :- if_(P_1, T=true, call(Q_1,T)).
   

2. A continuación, definimos el meta-predicado call_/1. Es útil con predicados reificados usados en esta respuesta. Con su nombre y semántica, call_/1 sigue if_/3, and_/2, y or_/2!

   call_(P_1) :- call(P_1,true).
   

3. Con (;)/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 todo.

¡Volvamos 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 preguntas, las mismas respuestas... Parece bien para mí!

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 fue investigada ya en los años 80, un pionero fue David Chan, y todavía 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 declarativo if-then-else de la siguiente manera, llamemos a este operador (~->)/2:

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

Si el intérprete Prolog también tiene una 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).

Observe el cambio de disyunción (;)/2 a conjunción (,)/2. Pregunte a las personas del Diagrama de Decisión Binaria (BDD) por qué son lógicamente equivalentes. Procedimentalmente hay matices, pero a través de la puerta trasera de la implicación incrustada para cierta A, el segundo la variante if-then-else también introducirá la indeterminación.

Pero, ¿cómo iríamos e introduciríamos, por ejemplo, la negación constructiva en un intérprete de Prolog? Una forma 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.. Ya que a menudo proporcionan negación reificada solo para dominios como enteros finitos, racionales, etc.. Pero para un predicado como member/2 necesitaríamos negación reificada para el universo de Herbrand.

También tenga en cuenta que los enfoques habituales para la negación constructiva también asumen 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 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 reificada apenas funciona fácilmente con predicados definidos, por lo que la siguiente consulta probablemente no funcionará:

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

Si lo anterior tiene éxito, cualquiera de los declarativos if-then-else como (~->)/2 o (~=>)/2 tendrá un uso menos frecuente, ya que las definiciones de predicados ordinarios ya entregarán la interpretación declarativa por el intérprete Prolog. Pero, ¿por qué la negación constructiva no se extiende ampliamente? Una razón podría ser el gran espacio de diseño de tal intérprete Prolog. Me di cuenta de que tendríamos la siguientes opciones:

Encadenamiento hacia atrás: Básicamente escupiríamos el intérprete 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 Herbrand.

Encadenamiento hacia adelante: También observe que en el encadenamiento hacia atrás nos encontraremos 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 secuente adecuado para Prolog solo tiene una fórmula en el lado derecho. Así que o bien vamos fórmula multi en el lado derecho y perderá paraconsistencia, o utilizamos el encadenamiento hacia adelante.

Conjuntos mágicos: Pero el encadenamiento hacia adelante contaminará los espacios de solución de una manera incontrolada. Así que podría necesitar alguna forma de combinación de encadenamiento hacia adelante y hacia atrás. No quiero decir con eso solo, que deberíamos ser capaces de cambiar dinámicamente entre los dos durante el proceso de solución, pero quiero decir que nead también un medio para generar conjuntos que dirigen el proceso de encadenamiento hacia adelante.

También se observan más problemas en esta respuesta aquí. Esto no significa que tarde o temprano se encontrará una fórmula, para encajar todos estos pares de problemas y soluciones juntos, pero podría tomar algunos más tiempo.

Adiós