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 of a variable and a term with the occurs check is at best linear in the sum of the term, whereas such unification without the occurs check runs in constant time. 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. The acyclic_term/1 built-in predicate can test whether a term is acyclic; subsumes_term/2 can test whether a term is subsumed by another one (see ref-lte). Additional 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.