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:
“Development, it turns out, occurs through this process of progressively more complex exchange between a child and somebody else—especially somebody who’s crazy about that child.”
—Urie Bronfenbrenner (b. 1917)
“The veto is a President’s Constitutional right, given to him by the drafters of the Constitution because they wanted it as a check against irresponsible Congressional action. The veto forces Congress to take another look at legislation that has been passed. I think this is a responsible tool for a president of the United States, and I have sought to use it responsibly.”
—Gerald R. Ford (b. 1913)