next up previous contents
Next: Lists Are Terms Up: Prolog Syntax Previous: Compound Terms and

The Occurs Check

This is an aside. If we try to unify two expressions we must generally avoid situations where the unification process tries to build infinite structures. Consider:


and try:
?- data(Y,Y).

First we successfully match the first arguments and Y is bound to X. Now we try to match Y with name(X). This involves trying to unify name(X) with X. What happens is an attempt to identify X with name(X) which yields a new problem ---to match name(X) against name(name(X)) and so on. We get a form of circularity which most Prolog systems cannot handle.

To avoid this it is necessary, that, whenever an attempt is made to unify a variable with a compound term, we check to see if the variable is contained within the structure of the compound term.

This check is known as the occurs check. If we try to unify two terms and we end up trying to unify a variable against a term containing that variable then the unification should fail.

Most Prolog implementations have deliberately missed out the occurs check ---mostly because it is computationally very expensive.

Consequently, the goal X=f(X) will usually succeed where it should really fail. The most common way in which this error might manifest itself is when the system tries to print out the binding for X. This usually results in an attempt to print an infinite term.

?- X=f(X).


Paul Brna
Mon May 24 20:14:48 BST 1999