occurs checkProlog do not perform the occurs check for reasons of efficiency. Without occurs check the complexity of unification is
O(min(size(term1), size(term2)))with occurs check it's
O(max(size(term1), size(term2)))In theorem proving unification without the occurs check can lead to unsound inference. For example, in Prolog it is quite valid to write
X = f(X).which will succeed, binding X to a cyclic structure. Clearly however, if f is taken to stand for a function rather than a constructor, then the above equality is only valid if f is the identity function. Weijland calls unification without occur check, "complete unification". The reference below describes a complete unification algorithm in terms of Colmerauer's consistency algorithm. ["Semantics for Logic Programs without Occur Check", W.P. Weijland, Theoretical Computer Science 71 (1990) pp 155-174].
Last updated: 1996-01-11