Occurs check
Encyclopedia
In computer science
, the occurs check is a part of algorithm
s for
syntactic unification
. It causes unification of a logic variable V and a structure S to fail if S contains V.
In theorem proving, unification without the occurs check can lead to unsound inference. For example, the Prolog
goal
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
.
By default, Prolog implementations omit the occurs check for reasons of efficiency.
The worst case complexity of unifying term1
with term2
is reduced without occurs check to
In the frequent case of variable-term unifications, an O(size(term)) runtime shrinks
to O(1).
A naive omission of the occurs check leads to the creation of cyclic structures
and may cause unification to loop forever.
Modern implementations use rational tree unification to avoid looping.
ISO Prolog implementations have the built-in predicate unify_with_occurs_check/2
for sound unification but are free to use unsound or even looping algorithms
when unification is invoked otherwise.
Implementations offering sound unification
for all unifications (optionally, via a runtime flag) are ECLiPSe
and SWI-Prolog
.
Weijland (1990) defines a complete unification algorithm in terms of Colmerauer's consistency algorithm.
Computer science
Computer science or computing science is the study of the theoretical foundations of information and computation and of practical techniques for their implementation and application in computer systems...
, the occurs check is a part of algorithm
Algorithm
In mathematics and computer science, an algorithm is an effective method expressed as a finite list of well-defined instructions for calculating a function. Algorithms are used for calculation, data processing, and automated reasoning...
s for
syntactic unification
Unification
Unification, in computer science and logic, is an algorithmic process by which one attempts to solve the satisfiability problem. The goal of unification is to find a substitution which demonstrates that two seemingly different terms are in fact either identical or just equal...
. It causes unification of a logic variable V and a structure S to fail if S contains V.
In theorem proving, unification without the occurs check can lead to unsound inference. For example, the Prolog
Prolog
Prolog is a general purpose logic programming language associated with artificial intelligence and computational linguistics.Prolog has its roots in first-order logic, a formal logic, and unlike many other programming languages, Prolog is declarative: the program logic is expressed in terms of...
goal
- X = f(X).
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
Identity function
In mathematics, an identity function, also called identity map or identity transformation, is a function that always returns the same value that was used as its argument...
.
By default, Prolog implementations omit the occurs check for reasons of efficiency.
The worst case complexity of unifying term1
with term2
- O(max(size(term1), size(term2)))
is reduced without occurs check to
- O(min(size(term1), size(term2)))
In the frequent case of variable-term unifications, an O(size(term)) runtime shrinks
to O(1).
A naive omission of the occurs check leads to the creation of cyclic structures
and may cause unification to loop forever.
Modern implementations use rational tree unification to avoid looping.
ISO Prolog implementations have the built-in predicate unify_with_occurs_check/2
for sound unification but are free to use unsound or even looping algorithms
when unification is invoked otherwise.
Implementations offering sound unification
for all unifications (optionally, via a runtime flag) are ECLiPSe
ECLiPSe
ECLiPSe is a software system for the development and deployment of Constraint Programming applications, e.g. in the areas of optimization, planning, scheduling, resource allocation, timetabling, transport etc....
and SWI-Prolog
SWI-Prolog
SWI-Prolog is an open source implementation of the programming language Prolog, commonly used for teaching and semantic web applications.It has a rich set of features, libraries forconstraint logic programming,multithreading,unit testing,GUI,...
.
Weijland (1990) defines a complete unification algorithm in terms of Colmerauer's consistency algorithm.