The occur-check
Christopher John Hogger · 1990
Abstract The unification algorithm presented in the previous Theme includes in its comparison cycle the following test: else if either of e1 and e2 is a variable which occurs strictly within the other then issue “failure” and tem1inate This test is called the occur-check and its purpose is to disallow self-referential bindings such as X/f(X). Here is a simple example in which that binding would arise in the unifier if the occur-check were to be omitted: The binding X/f(X) effectively assigns to X the infinite term f(f(L)), whereas all expressions in our language are presumed to be syntactically finite. In particular, although the Herbrand domain might well be an infinite set of terms, the terms themselves are presumed to be finite.