occurs check

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)