Search code examples
prologoccurs-check

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


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


Solution

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