Computing (FOLDOC) dictionary
Jump to user comments
programming A feature of some implementations of
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
with occurs check it's
lead to unsound inference. For example, in Prolog
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
, then the above equality is only valid if f is
Weijland calls unification without occur check, "complete
unification". The reference below describes a complete
unification algorithm in terms of Colmerauer's consistency
["Semantics for Logic Programs without Occur Check",
W.P. Weijland, Theoretical Computer Science 71 (1990) pp