Search code examples
prologunification

Unification in Prolog

This is a question from a past exam about unification in Prolog. we were supposed to say if they unified and then the instantiations. 

f(a,g(b,a)) and f(X,g(Y,X))

This unifies quite a = X, g(b,a) = g(Y,X) and is quite straight forward

f(g(Y),h(c,d)) and f(X,h(W,d))

I dont think this one unifies because of g(Y) =/ X, though h(c,d) does unify with h(W,d). Though is it possible that X = g(Y) since uppercase X looks until it finds a solution?

Solution

  • 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) returns h(_) = h(_), and this allows the unification to continue, since h 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 variable W is bound to the term c, since it was not bound before -- a comparison would be performed otherwise;

    • the unification of X = g(Y) simply binds the unbound variable X to the term g(Y), and g(Y) is a term with an unbound variable, since there's no available unification to g(Y).

    Regards!