Did you know ... Search Documentation:
Predicate unifiable/3
Availability:built-in
unifiable(@X, @Y, -Unifier)
If X and Y can unify, unify Unifier with a list of Var = Value, representing the bindings required to make X and Y equivalent.73This predicate was introduced for the implementation of dif/2 and when/2 after discussion with Tom Schrijvers and Bart Demoen. None of us is really happy with the name and therefore suggestions for a new name are welcome. This predicate can handle cyclic terms. Attributed variables are handled as normal variables. Associated hooks are not executed.
Tags are associated to your profile if you are logged in
Tags:
Dragan Ivanovic said (2021-01-27T14:03:04):0 upvotes 0 0 downvotes
Picture of user Dragan Ivanovic.

Hi, when running a very classical example of rational tree unification, I get the following:

?- f(X, Y, X) = f(g(X), g(Y), Y).
X = Y, Y = g(Y).

However, with unifiable/3, I have this:

?- unifiable(f(X, Y, X), f(g(X), g(Y), Y), U).
U = [Y=g(Y), X=g(X)].

The result of unifiable/3 is exactly what I expected from the Prolog-II-style base reduction algorithm, but the first response is more accurate. Why do these two differ? Can you please point me to the specification of the SWI Prolog unification algorithm used in =/2 ?