Occur Check

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).