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.
Famous quotes containing the words occurs and/or check:
“Of course, some men are very effective caregivers [of elderly parents]. But this situation occurs far less frequently for males than females, because it is a role reversal. For women, caregiving is an expected duty; for men, it is an unexpected expression of love or devotion.”
—Tish Sommers (20th century)
“If he had been sent to check out Bluebeard’s castle, he would have come back with a glowing report about the admirable condition of the cutlery.”
—Mary McGrory (b. 1918)