"not provable", what does this to do with unification?

Question

I found one interesting point in nominal unification. Just after proposition 2.16 of Nominal Unification by Urban, Pitts, and Gabbay, it said the following, which I found confusing:

For non-ground terms, the relation $=_{\alpha}$ and $\approx$ differ! For example, $a.\!X=_{\alpha} b.\!X$ always holds, whereas $\emptyset\vdash a.\!X \approx b.\!X$ is not provable unless $a = b$.

The $=_{\alpha}$ is the standard $\alpha$-equivalence and $\approx$ is defined in the paper.

It seems to me that $\vdash a.\!X \approx b.\!X$ has a unifier which is ${a \# x},[X:=(a \, b)X]$ no matter what $a$ and $b$ are according to the unification algorithm in the same paper.

So, I am trying to understand why the paper said the above lines? what is the relationship between something is "not provable " but has a unifier? or I am misunderstanding something?

Hoping someone could clarify this point for me, thanks in advance!

Answer 1

They mean you can't use the rules in Figure 2 defining $\approx$ (and $\#$) to derive $\emptyset\vdash a.\!X\approx b.\!X$. If you attempt to do it you'll use $\approx$-abstraction-2 followed by $\approx$-suspension at which point you'll not be able to satisfy the premise as $\nabla$ is empty but the disagreement set is $\{a,b\}$. There are no other applicable rules, so there is no derivation.

Conceptually, though conceptual understanding is not needed to answer this question, what's happening is with an empty freshness environment we're free to replace $X$ with $a$ (or $b$) but $a.\!a \neq_\alpha b.\!a$. This is what it means in the sentences following that quote by $\alpha$-equivalence not being preserved by substitution. The freshness constraints in $\nabla$ are what disallow such substitutions. So in an empty freshness environment $a.\!X$ and $b.\!X$ can't be unified as their instances need not be $\alpha$-equivalent.

I recommend getting more familiar with inductively defined judgements and derivations, as e.g. discussed in Chapter 2 of Robert Harper's Practical Foundations for Programming Languages. You should do the exercises there, and write out the complete derivations for the examples in the Nominal Unification paper. Ultimately, checking derivability like this should be as straightforward and mechanical as checking $(x+3)(x-1) = x^2+2x-3$.