Occurs check


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

Application in theorem proving

In theorem proving, unification without the occurs check can lead to unsound inference. For example, the Prolog goal
will succeed, binding X to a cyclic structure which has no counterpart in the Herbrand universe.
As another example,
without occurs-check, a resolution proof can be found for the non-theorem

Prolog implementation

Prolog implementations usually 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
with term
is reduced in many cases from
to
in the particular, frequent case of variable-term unifications, runtime shrinks to
A naive omission of the occurs check leads to the creation of cyclic structures
and may cause unification to loop forever.
Modern implementations, based on Colmerauer's Prolog II,
use rational tree unification to avoid looping.
See image for an example run of the unification algorithm given in Unification #A unification algorithm, trying to solve the goal, however without the occurs check rule ; applying rule "eliminate" instead leads to a cyclic graph 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, provided the algorithm works correctly for all cases that are "not subject to occurs-check".
Implementations offering sound unification for all unifications are Qu-Prolog and Strawberry Prolog and : XSB, SWI-Prolog and .