Search code examples
prologunification

Most General Unifier (Prolog)

Have a quick question regarding m.g.u (most general unifier) in prolog.

We are asked what the m.g.u is of:

f(X, g(Y, h(Z))) = f(Z, g(P, h(a))).

With 2 possible answers

1. θ = {X/Z,Y/P,Z/a}.
2. θ = {X/a,Y/P,Z/a}.

I argued that the second answer was the most general unifier, however, it appears that the first answer is correct.

I have tried both substitutions and they both yield the same result, however the second answer was with fewer substitutions which is why I argued that it was the m.g.u

Any help would be appreciated, thanks!

   +-----------X
   |
   |     +-----Y
   |     |
f--+--g--+
         |
         +--h--Z
         
         
   +-----------Z
   |
   |     +-----P
   |     |
f--+--g--+
         |
         +--h--a
Solution

  • The definition of an mgu is that there is no decomposition θ = λτ where λ,τ are non-trivial (not the identity, the names of freshly introduced variables don't matter). There exists a substitution of 1 that results in 2 (I can edit the solution later, if you don't find it) such that 2 can not be the most general substitution.

    There's one more caveat: if you apply θ = {X/Z,Y/P,Z/a} to X you will end up with Z, not a. A substitution always happens simultaneously.