Prolog's unification does not have an occur check; that is, when
unifying a variable against a term, the system does not check to see if the
variable occurs in the term. When the variable occurs in the term,
unification should fail, but the absence of the check means that the
unification succeeds, producing a circular term
. Trying to print a
circular term, or trying to unify circular terms, will cause a loop.
(You can always get out of a loop by typing ^c followed by an
a for abort.)
The absence of the occur check is not a bug or a design oversight, but
a conscious design decision. The reason for this decision is that
unification with the occur check is at best linear on the sum of the
sizes of the terms being unified, whereas unification without the
occur check is linear on the size of the smallest of the terms being
unified. For any programming language to be practical, basic
operations should take constant time. Unification against a variable
may be thought of as the basic operation of Prolog, and this can take
constant time only if the occur check is omitted. Thus the absence of
an occur check is essential to Prolog's practicality as a programming
language. The inconvenience caused by this restriction is, in
practice, very slight. Furthermore, the functionality is available as
library(occurs)
.