Yes, it does unify, and it does so because g(Y)
is a term to be evaluated, as well as a
-- in the first example you pointed.
You can check the evaluation in a prolog interpreter:
?- f(g(Y),h(c,d)) = f(X,h(W,d)).
X = g(Y),
W = c.
The unification process works in a depth-first fashion, unifying members and returning each of the available answer, until no further combination is possible.
This means the unification method is called for f(g(Y),h(c,d)) = f(X,h(W,d))
, that finds out the available matchings: g(Y) = X, h(c, d) = h(W, d)
.
Then, the unification is performed upon g(Y) = X
, that, since there's no further possible reduction, returns X = g(Y)
.
Then, the same method is called upon the matching h(c, d) = h(W, d)
, which gives you c = W
, and no other matching, resulting, thus, in W = c
.
The answers, after unification, are returned, and it's usually returned false
to point when no matching/further matching is possible.
As pointed by CapelliC, the variable Y
, after the unification process, is still unbound. The unification is performed upon unbound variables, which means:
the unification of
h(c, d) = h(W, d)
returnsh(_) = h(_)
, and this allows the unification to continue, sinceh
is a term, and not an unbound var;the unification of
d = d
is a matching of terms, and does not form an attribution -- or binding;the unification of
c = W
forms an attribution, and the variableW
is bound to the termc
, since it was not bound before -- a comparison would be performed otherwise;the unification of
X = g(Y)
simply binds the unbound variableX
to the termg(Y)
, andg(Y)
is a term with an unbound variable, since there's no available unification tog(Y)
.
Regards!