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

Question

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

Answer 1

The result of the goal X = f(X) depends on the implementation of Prolog. On some systems, as Carlo pointed out in his answer, the result can be controlled using a user-set flag. The unification predicate, (=)/2 , can be implemented with or without the so-called presence check. This check checks if a variable exists in one operand in a sub-member of another operand. When the unification predicate implements this check, the target X = f(X) fails. But, for performance reasons, the join predicate is often implemented without this check. The ISO Prolog standard specifies an alternative unification predicate, aptly named unify_with_occurs_check/2 , which can be used when targets such as this can lead to problems.

Currently, several implementations support cyclic terms, also known as rational terms created by goals such as X = f(X) . These include CxProlog, ECLiPSe, SICStus Prolog, SWI-Prolog and YAP. Please note, however, that the level of support for rational terms varies by system. Minimum support will be to (1) be able to create rational terms (without!), (2) be able to unify two rational terms, and (3) be able to print query bindings that include rational terms in an unambiguous way. Using these three functions, you can, for example, implement co-inductive logic programming, which is useful for several classes of problems.

Answer 2

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

The expression that you specify in the title of the question, if called when X is a free variable, will create a circular term. In SWI-Prolog

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

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