4.2.7 Occurs-Check

Prolog's unification does not have an occurs-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 cyclic term. Operations such as trying to print a cyclic term will cause a loop.

The absence of the occurs-check is not a bug or a design oversight, but a conscious design decision. The reason for this decision is that unification with the occurs-check is at best linear on the sum of the sizes of the terms being unified, whereas unification without the occurs-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 occurs-check is omitted. Thus the absence of an occurs-check is essential to Prolog's practicality as a programming language. The inconvenience caused by this restriction is, in practice, very slight.

SICStus Prolog unifies, compares (see ref-lte-cte), asserts, and copies cyclic terms without looping. The write_term/[2,3] built-in predicate can optionally handle cyclic terms. Unification with occurs-check is available as a built-in predicate; see ref-lte-met-usu. Predicates for subsumption and testing (a)cyclicity are available in a library package; see lib-terms. Other predicates usually do not handle cyclic terms well.


Send feedback on this subject.