What does Prolog do if you X = f(X)?

Question

What does it mean in Prolog comparing a predicate to an unbound variable?

Answer 1

In Prolog, (=)/2 it not a comparison, but a fundamental operation, called unification.

The expression you show in your question title, if called when X is a free variable, will create a cyclic term. In SWI-Prolog

?- X=f(X),write(X).
@(S_1,[S_1=f(S_1)])
X = f(X).

Cyclic terms are problematic to handle, usually are created by programming errors: the behaviour of SWI-Prolog (and others) can be controlled using a global flag, see occurs_check.

Answer 2

The result of the X = f(X) goal depends on the Prolog implementation, In some systems, as Carlo pointed out in his answer, the result can be controlled by a user settable flag. The unification predicate, (=)/2, may be implemented with or without what's called the occurs check. This check verifies if a variable in one operand occurs in a sub-term in the other operand. When the unification predicate implements this check, the goal X = f(X) fails. But, for performance reasons, the unification predicate is often implemented without this check. The ISO Prolog standard specifies an alternative unification predicate, aptly named unify_with_occurs_check/2, that can be used when goals such as this one can lead to trouble.

Nowadays, several implementations support the cyclic terms, also known as rational terms, that are created by goals such as X = f(X). These include CxProlog, ECLiPSe, SICStus Prolog, SWI-Prolog, and YAP. Note, however, that the level of support for rational terms varies across system. The minimal support will be (1) to be able to create rational terms (without a stack overflow!), (2) to be able to unify two rational terms, and (3) to be able to print query bindings that include rational terms in a non-ambiguous way. With these three features you can e.g. implement coinductive logic programming, which is useful for several classes of problems.