Unification of an expression : Example

Question

Trying to learn Unification process, and while reading in a website about it, i found this example.

1. Find the MGU of {p(f(a), g(Y)) and p(X, X)}

        Sol: S0 => Here, Ψ1 = p(f(a), g(Y)), and Ψ2 = p(X, X)
              SUBST θ= {f(a) / X}
              S1 => Ψ1 = p(f(a), g(Y)), and Ψ2 = p(f(a), f(a))
              SUBST θ= {f(a) / g(y)}, Unification failed.
   

Unification is not possible for these expressions.

I wanna know if this Unification failure isn't only due to the chosen Substitution ? For example why they didn't substitute: X / f(a) and then X / g(y) to get p(X,X) and p(X,X) ?

Answer 1

To unify p(f(a), g(Y)) = p(X, X) would require that f(a) = X and g(Y) = X but f and g are distinct, so this fails.

There is no choice about substitutions or anything here, it must fail.

Answer 2

The problem is that $X$ occurs twice in the second expression, and by the definition of substitution, all occurrences of the variable must be replaced at once. Applying the substitution only to some of the occurrences of the variable while leaving the others unchanged, or choosing two different bindings for the same variable, is not possible. If we substitute the first $X$ with $f(a)$, we have to do it in the same step for the second $X$, too.
In the solution they did substitute $X/f(a)$ first, but after that the result is $P(X[f(a)/X],X[f(a)/X]) = P(f(a), f(a))$, with the second $X$ also already substituted by $f(a)$, so that it is no longer free to substitute by $g(Y)$.