prolog - Problemas de integración de la reificación

clpfd reification

Question

Ofrecí el siguiente código basado en clpfd para la pregunta reciente Segregating Lists in Prolog :

list_evens_odds([],[],[]).
list_evens_odds([X|Xs],[X|Es],Os) :-
X mod 2 #= 0,
list_evens_odds(Xs,Es,Os).
list_evens_odds([X|Xs],Es,[X|Os]) :-
X mod 2 #= 1,
list_evens_odds(Xs,Es,Os).

Es conciso y puro, pero puede dejar atrás muchos puntos de elección innecesarios. Considerar:

?- list_evens_odds([1,2,3,4,5,6,7],Es,Os).

La consulta anterior deja atrás un punto de elección inútil para cada elemento no impar en [1,2,3,4,5,6,7] .

Implementación alternativa

El uso de la técnica de reificación demostrada por @false en la unión Prolog para AUBUC puede reducir la cantidad de puntos de elección innecesarios. La implementación podría cambiar a:

list_evens_odds([],[],[]).
list_evens_odds([X|Xs],Es,Os) :-
if_(#<=>(X mod 2 #= 0), (Es=[X|Es0],Os= Os0),
(Es= Es0, Os=[X|Os0])),
list_evens_odds(Xs,Es0,Os0).

Para interactuar directamente con clpfd-reification, la implementación de if_/3 podría adaptar así:

if_( C_1, Then_0, Else_0) :-
call(C_1,Truth01),
indomain(Truth01),
( Truth01 == 1 -> Then_0 ; Truth01 == 0, Else_0 ).

Por supuesto, (=)/3 también necesitaría adaptarse a esta convención.

La línea de fondo

Entonces me pregunto: ¿es una buena idea usar 0 y 1 como valores de verdad en lugar de false y true ?

¿Me están perdiendo problemas a lo largo de ese camino? ¡Ayuda por favor! ¡Gracias de antemano!

Answer 1

En SWI-Prolog, puede usar zcompare/3 :

:- use_module(library(clpfd)).
list_evens_odds([], [], []).
list_evens_odds([X|Xs], Es, Os) :-
Mod #= X mod 2,
zcompare(Ord, 0, Mod),
ord_(Ord, X, Es0, Es, Os0, Os),
list_evens_odds(Xs, Es0, Os0).
ord_(=, X, Es0, [X|Es0], Os, Os).
ord_(<, X, Es, Es, Os0, [X|Os0]).

Consulta de ejemplo:

?- list_evens_odds([1,2,3,4,5,6,7], Es, Os).
Es = [2, 4, 6],
Os = [1, 3, 5, 7].

Answer 2

He reconsiderado mi "doble uso" propuesto de if_/3 y ahora siento que estoy mejorando.

Los comentarios de @false y @lurker y la respuesta de @mat han contribuido bastante a mi comprensión. ¡Gracias!

Los "conocimientos" que obtuve no son dramáticos; todavía me gustaría compartirlos con usted:

1. La adaptación de if_/3 como lo hice es if_/3 y puede ser similar a la de algunos LOC.
2. Sin embargo, mezcla dos conceptos que son procesalmente bastante diferentes entre sí: por defecto, clpfd se propaga y luego se retrasa. La igualdad del término reificado OTOH obliga a elegir de inmediato.
3. Por lo tanto, es más limpio separar estos dos casos de uso. Y, por supuesto, "la limpieza es de hecho junto a la Divinidad" ...

Answer 3

La solución directa (que funciona para cualquier condición clp (fd) que pueda ser reificada) parece ser

:- use_module(library(clpfd)).
list_evens_odds([],[],[]).
list_evens_odds([X|Xs],Es,Os) :-
B #<==> (X mod 2 #= 0),
freeze(B, (B=1 -> Es=[X|Es0],Os=Os0 ; Es=Es0,Os=[X|Os0])),
list_evens_odds(Xs,Es0,Os0).

Si 0/1 o verdadero / falso se utilizan como valores de verdad realmente no importa aquí. La razón por la cual la convención 0/1 es preferida en los solucionadores de aritmética es simplemente que usted puede reutilizar fácilmente los valores de verdad en las restricciones aritméticas, por ejemplo, sumarlos, etc.