Occurs Check

In computer science, the occurs check is a part of algorithms for syntactic unification. It causes unification of a logic variable V and a structure S to fail if S contains V.

In theorem proving, unification without the occurs check can lead to unsound inference. For example, the Prolog goal

X = f(X).

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.

By default, Prolog implementations omit the occurs check for reasons of efficiency. The worst case complexity of unifying term1 with term2

O(max(size(term1), size(term2)))

is reduced without occurs check to

O(min(size(term1), size(term2)))

In the frequent case of variable-term unifications, an O(size(term)) runtime shrinks to O(1).

A naive omission of the occurs check leads to the creation of cyclic structures and may cause unification to loop forever. Modern implementations use rational tree unification to avoid looping.

ISO Prolog implementations have the built-in predicate unify_with_occurs_check/2 for sound unification but are free to use unsound or even looping algorithms when unification is invoked otherwise. Implementations offering sound unification for all unifications (optionally, via a runtime flag) are ECLiPSe, XSB and SWI-Prolog.

Weijland (1990) defines a complete unification algorithm in terms of Colmerauer's consistency algorithm.