Word:

occurs check

(programming)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].
Browse
occupation license
occupational
occupational disease
occupational group
occupational hazard
occupational safety and health act
Occupational Safety and Health Administration
occupational therapy
Occupavit
occupied
Occupier
Occupy
occupying
Occur
Occurrence
Occurrent
-- occurs check --
Occurse
Occursion
OCD
OCE
Ocean
ocean bottom
ocean current
ocean floor
ocean liner
ocean perch
ocean pout
Ocean State
ocean sunfish
ocean trip
oceanaut
oceanfront
Definitions Index: # A B C D E F G H I J K L M N O P Q R S T U V W X Y Z

About this site and copyright information - Online Dictionary Home - Privacy Policy