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?

  • $\begingroup$ We expect references to fulfill the minimal scholarly requirements and be as robust over time as possible. Please take some time to improve your post in this regard. We have collected some advice here. Thank you! $\endgroup$
    – D.W.
    Nov 25, 2016 at 16:31

1 Answer 1


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.


Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.