Prolog Best Practice: checking if a variable is already bound.

Question

I sent this solution to a question, but ony left me a comment saying:

Predicates in order to check whether a "variable" is free or already connected should have a strategy for obtaining the unification right for other "variables" (that is, speed up or make it possible to derive them). The same is for dynamic predicates - they can be used to speed up something, but they should not use the behavior of something as a trigger for changing.

I wonder why this is so. Why does bad practice verify that something is already defined for something else? Do you think this is bad practice? Are there other options that would be “best practice”.

Here is my solution:

% ================================ % 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

The main problem of predicates like integer/1 , atom/1 , etc. lies in the fact that they are not monotonous .

Take for example ?- integer(5). that succeeds. But a more general goal ?- integer(X). fails !

For declarative debugging and automatically generated explanations, we expect that if a goal is successful, every generalization of that goal should not fail.

"Correct" (i.e. if you want nice monotone predicates that make declarative sense), it would be for integer/1 to create an instance creation error, for example ?- integer(X). on the grounds that she does not have enough information to answer the question at this time. Instead of integer/1 you should use must_be/2 from library(error) to get this sound behavior:

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

must_be/2 behaves monotonously, which is usually a good property.

Extending the comment: the problem is that (at least if the results above are correct), your predicate is no longer a true relation, since goals are now not commutative ?- X = 0, X = Y, addUnique([X,Y,3],3). succeeds, but simply exchanges the order of goals does not give the same result, because ?- X = Y, addUnique([X,Y,3], 3), X = 0. fails.

Such phenomena are a common consequence of the use of meta-logical predicates. A declarative solution to such problems is limitations , see, for example, dif/2 . They are monotonous, commutative, and generally much easier to understand.