occurs check

Computing Dictionary

occurs check definition

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].
The Free On-line Dictionary of Computing, © Denis Howe 2010 http://foldoc.org
Cite This Source
Explore Dictionary.com
Previous Definition: occurring
Next Definition: occurse
Words Near: occurs check
More from Thesaurus.com
Synonyms and Antonyms for occurs check
More from Reference.com
Search for articles containing occurs check
More from Dictionary.com Translator
Dictionary.com Word FAQs

Dictionary.com presents 366 FAQs, incorporating some of the frequently asked questions from the past with newer queries.

Copyright © 2014 Dictionary.com, LLC. All rights reserved.
  • Please Login or Sign Up to use the Recent Searches feature