문제

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!

올바른 솔루션이 없습니다

라이센스 : CC-BY-SA ~와 함께 속성
제휴하지 않습니다 cs.stackexchange
scroll top