Unification of terms in Prolog

Question

I have the follow terms :

T1 = f(f(3,Z,2),f(I,Z,G),Z)

T2 = f(F,f(R,f(5,2),D),f(3,2,F))

I have to unify that terms.

My idea is:

G=(3,Z,2)

I=(5,2)

I=(3,2,F)

I know how to unify in simple examples. Anyone that can shed some light on this one for me ? Thanks

Answer 1

Developing intuitions for unification is really valuable, both in and outside of the Prolog world. So I think it is very valuable to spend time learning how to find unifying terms by hand! A wonderful thing about unification is that you can reason through unification of simple terms using your geometric intuition!

Consider this lovely illustration from the wikipedia article on unification for some inspiration:

Given two partial structures, t1 and t2 we can find the unifier by comparing the parts of the structures to match up missing bits in one with present bits in the other. In Prolog, the missing bits to a structure are the variables.

Returning to your question, let's do some ascii art to make the structure of your two terms more apparent.

T1 = f( f(3, R, 2), f(A, R      ,I), A          )
%    |  |           | |  |       |   | 
T2 = f( N         , f(E, f(5, 2),S), f(3, 2, N) )

This presents the exact same compound terms, only they are spaced out, and I've added pipes matching up the parts of the terms which must coordinate in order to figure out the unification. Note that the pipes also connect terms which are not variables. This is important, because if there were any mismatched ground terms in the structure then our unification would simply fail.

Reading from left to right, the first variable we encounter is N. Following the pipe, we see that N must be unified with the compound term f(3, R, 3), or else the structures couldn't possible match, and unification would fail. So we know that N = f(3, R, 3).

The next variables that occur are A and E. Indeed, these are coordinated, so we know that A = E, but we don't yet have enough information to say more.

The next variable we see is R. That is coordinated with the compound term f(5, 2), so we must have, R = f(5, 2). This gives us the first unification of a variable with a ground term! Since we know the ground term that must unify with R, we can also fill in the missing hole from our previous unification for N: N = f(3, R, 4) = f(3, f(5, 2) 3).

Continue on in this way, and you'll end up with the same result Prolog will find for you, as illustrated by Daniel Lyons' answer!

May you have much fun in your future unifications :)

Answer 2

I'm kind of surprised you didn't just ask Prolog to do it for you:

?- T1 = f(f(3,R,2),f(A,R,I),A), T2 = f(N,f(E,f(5,2),S),f(3,2,N)), T1=T2.                                                             
T1 = T2, T2 = f(f(3, f(5, 2), 2), f(f(3, 2, f(3, f(5, 2), 2)), f(5, 2), S), f(3, 2, f(3, f(5, 2), 2))),
R = f(5, 2),
A = E, E = f(3, 2, f(3, f(5, 2), 2)),
I = S,
N = f(3, f(5, 2), 2).