occurs check

programming A feature of some implementations of

unification which causes unification of a logic variable V

and a structure S to fail if S contains V.

Binding a variable to a structure containing that variable

results in a cyclic structure which may subsequently cause

unification to loop forever. Some implementations use extra

pointer comparisons to avoid this.

Most implementations of Prolog do not perform the occurs

check for reasons of efficiency. Without occurs check the

complexity of unification is

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

with occurs check it's

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

In theorem proving unification without the occurs check can

lead to unsound inference. For example, in Prolog it is

quite valid to write

X = f(X).

which 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.

Weijland calls unification without occur check, "complete

unification". The reference below describes a complete

unification algorithm in terms of Colmerauer's consistency

algorithm.

["Semantics for Logic Programs without Occur Check",

W.P. Weijland, Theoretical Computer Science 71 (1990) pp

155-174].

(1996-01-11)