prolog - Restricciones duplicadas en CLP(FD) y con dif/2

clpfd

Question

En SWI-Prolog, la siguiente consulta da este resultado:

?- X mod 2 #= 0, X mod 2 #= 0.
X mod 2#=0,
X mod 2#=0.

Si bien es correcto, obviamente no hay necesidad de la segunda restricción

Similar:

?- dif(X,0), dif(X,0).
dif(X, 0),
dif(X, 0).

¿No hay forma de evitar tales restricciones duplicadas? (Obviamente, la forma más correcta sería no escribir el código que conduce a esa situación, pero no siempre es tan fácil).

Answer 1

Solo para dif/2 , la vinculación puede probarse sin recurrir a ningún elemento interno:

difp(X,Y) :-
( X /= Y -> true
; dif(X, Y)
).

Answer 2

Pocos sistemas de programación restrictiva implementan la contracción también relacionada con la factorización en la demostración del teorema de resolución, ya que el etiquetado CLP no es SMT . La contracción es una regla estructural , y se lee de la siguiente manera, suponiendo que las restricciones se almacenan antes de la (| -) / 2 en forma negada.

G, A, A |- B
------------ (Left-Contraction)
G, A |- B

También podríamos extenderlo al caso en que las dos A sean equivalentes. Lo más probable es que esto no se implemente, ya que es costoso. Por ejemplo, Jekejeke Minlog ya implementa la contracción para CLP (FD), es decir, dominios finitos. Encontramos consultas similares a la primera consulta del PO:

?- use_module(library(finite/clpfd)).
% 19 consults and 0 unloads in 829 ms.
Yes
?- Y+X*3 #= 2, 2-Y #= 3*X.
3*X #= -Y+2
?- X #< Y, Y-X #> 0.
X #=< Y-1

Básicamente normalizamos a A1 * X1 + .. + An * Xn # = B respectivamente A1 * X1 + .. + An * Xn # = <B donde gcd (A1, .., An) = 1 y X1, .., Xn son léxicamente ordenado, y luego verificamos si ya existe la misma restricción en el almacén de restricciones. Pero para CLP (H), es decir, los términos del dominio Herbrand, aún no hemos implementado la contracción. Todavía estamos deliberando sobre un algoritmo eficiente:

?- use_module(library(term/herbrand)).
% 2 consults and 0 unloads in 35 ms.
Yes
?- neq(X,0), neq(X,0).
neq(X, 0),
neq(X, 0)

La contracción para dif / 2 significaría implementar un tipo de (==) / 2 a través de la instanciación definida en la restricción dif / 2. es decir, necesitaríamos aplicar una prueba recursiva siguiendo el emparejamiento de variables y términos definidos en la restricción dif / 2 contra todas las demás restricciones dif / 2 que ya están en el almacén de restricciones. Probar la subsunción en lugar de la contracción también tendría más sentido.

Probablemente solo sea factible implementar contracción o subsunción para dif / 2 con la ayuda de alguna técnica de indexación apropiada. En Jekejeke Minlog, por ejemplo, para CLP (FD) indexamos en X1, pero aún no nos dimos cuenta de la indexación para CLP (H). Lo primero que deberíamos averiguar es una forma normal de las restricciones dif / 2; consulte también este problema aquí .

Answer 3

Puede evitar publicar restricciones redundantes o eliminarlas con una setof/3 tipo setof/3 . Ambos son muy específicos de la implementación. La mejor interfaz para tal fin es ofrecida por SICStus. Otras implementaciones como YAP o SWI copiaron más o menos esa interfaz, omitiendo algunas partes esenciales . Un intento reciente de superar las deficiencias de SWI fue rechazado.

Evite publicar restricciones

En SICStus, puede usar frozen/2 para este propósito:

| ?- dif(X,0), frozen(X,Goal).
Goal = prolog:dif(X,0),
prolog:dif(X,0) ? ;
no
| ?- X mod 2#=0, frozen(X, Goal).
Goal = clpfd:(X in inf..sup,X mod 2#=0),
X mod 2#=0,
X in inf..sup ? ;
no

De lo contrario, copy_term/3 podría ser lo suficientemente bueno, siempre que las restricciones no estén demasiado interconectadas entre sí.

Eliminar las restricciones redundantes

Aquí, una construcción similar a un setof junto con call_residue_vars/1 y copy_term/3 es probablemente el mejor enfoque. De nuevo, la implementación original está en SICStus ....