資料來源 : Free On-Line Dictionary of Computing

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)