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)
Nearby terms:
occam 2 « Occam's Razor « occlude « occurs check
» OCL » OCLC » OC-n
|
