occurs check

1 definition found

occurs check - Free On-line Dictionary of Computing (26 May 2007) :

  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)