occurs check

    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)