sistemas - Mejor práctica de Prolog: verificar si una variable ya está vinculada.

reglas en prolog

Question

Publiqué esta solución a una pregunta, pero un me dejó un comentario diciendo:

Los predicados para verificar si "variable" es libre o ya está vinculada deben cambiar la estrategia para derivar uniones correctas para otras "variables" (es decir, acelerar, o hacer posible derivarlas). Lo mismo para los predicados dinámicos: se pueden usar para acelerar algo, pero no se deben usar como disparadores del comportamiento cambiante de algo.

Me pregunto por qué es esto. ¿Por qué es una mala práctica verificar si algo ya está definido para otra cosa? ¿Crees que es una mala práctica? ¿Hay otras opciones que serían "mejores prácticas"?

Aquí estaba mi solución:

% ================================
% Ensures that all variables are unique.
% ================================
% Base case: Assigned variables unique values
used([], Nin, Nin).
% Have already assigned a value to this variable
used([A|B], Nin, Nout) :-
integer(A), % <----------------- THIS IS THE LINE IN QUESTION
helper(B,Nin,Nout).
% Have not assigned a value to this variable yet
% Assign it and remove it from the list.
used( [A|B] , Nin, Nout) :-
member(A,Nin),
delete(Nin,A,Temp),
helper(B,Temp,Nout).

Answer 1

El problema fundamental de los predicados como integer/1 , atom/1 etc. es que no son monótonos .

Tome por ejemplo ?- integer(5). que tiene éxito Pero un objetivo más general ,? ?- integer(X). ¡ falla !

Para la depuración declarativa y las explicaciones generadas automáticamente, esperamos que si un objetivo tiene éxito, toda generalización de ese objetivo no debe fallar.

Lo "correcto" (es decir, si quieres buenos predicados monotónicos que tengan sentido declarativo) sería que el integer/1 generara un error de instanciación en consultas como ?- integer(X). con el argumento de que no tiene suficiente información para responder la pregunta en este momento. En lugar de integer/1 , debe usar must_be/2 de la library(error) para obtener este comportamiento de sonido:

?- must_be(integer, X).
ERROR: Arguments are not sufficiently instantiated

must_be/2 comporta de forma monótona, que en general es una buena propiedad.

Extendiendo el comentario de ony: El problema es que (al menos si los resultados de la muestra anteriores son correctos) su predicado ya no es una relación verdadera porque los objetivos ahora no son conmutativos ?- X = 0, X = Y, addUnique([X,Y,3],3). tiene éxito, pero simplemente intercambiando el orden de las metas no produce el mismo resultado porque ?- X = Y, addUnique([X,Y,3], 3), X = 0. falla.

Tales fenómenos son consecuencia común del uso de predicados meta-lógicos. La solución declarativa a tales problemas son las restricciones , ver por ejemplo dif/2 . Son monótona, conmutativa y, en general, mucho más fácil de entender.