Computer Science Stack Exchange is a question and answer site for students, researchers and practitioners of computer science. It only takes a minute to sign up.
Sign up to join this community
In unification, there is a "occur-check". Such as $X = a \, X$ fails to find a substitution for $X$ since it appears on right hand side too. The first-order unification, higher-order unification all have occur-check.
the paper nominal unification described a kind of unification based on nominal concepts. But I did not mention "occur-check" at all.
So, I am thinking why? does it has occur-check?
Yes, it has the occur check. The ~variable transformation rule of nominal unification has a condition which states
provided X does not occur in t
what it is saying is exactly occur check.