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!

No correct solution

Licensed under: CC-BY-SA with attribution
Not affiliated with cs.stackexchange
scroll top