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.

Algorithm

When a variable $x$ is to be unified with a term $t$ (where $x\neq t$), the occurs check simply causes the unification to fail if $t$ contains $x$. This check is expressed in the following algorithm.

  function occurscheck(variable x, term t)
      if (x occurs in t)
         fail
      else
         succeed

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

Application in theorem proving

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.

Prolog implementation

Unification without occurs check leading to cycle

By default, Prolog implementations omit the occurs check for reasons of efficiency, which can lead to circular data structures and looping. By not performing the occurs check, the worst case complexity of unifying a term $t_{1}$ with term $t_{2}$ is reduced from

$O\left({{\textbf {max}}\left({{\textbf {size}}(t_{1}),{\textbf {size}}(t_{2})}\right)}\right)$

to

$O\left({{\textbf {min}}\left({{\textbf {size}}(t_{1}),{\textbf {size}}(t_{2})}\right)}\right)$

In the frequent case of variable-term unifications, an $O({\textbf {size}}(t))$ for term $t$ 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. See image for an example run of the unification algorithm given in Unification_(computer_science)#A_unification_algorithm, trying to solve the goal $cons(x,y){\stackrel {?}{=}}cons(1,cons(x,cons(2,y)))$, however without the occurs check rule (6th rule); applying the 5th rule instead leads to a cyclic graph (i.e. an infinite term) in the last step.

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.

References

• "Semantics for Logic Programs without Occur Check", W.P. Weijland, Theoretical Computer Science 71 (1990) pp 155–174.

This article is based on material taken from the Free On-line Dictionary of Computing prior to 1 November 2008 and incorporated under the "relicensing" terms of the GFDL, version 1.3 or later.