Prolog: Is f(X) = X unifiable or not?

Question

My understanding of unification is a little patchy. I understand basic unification, but I'm having issues getting my head round terms which are not unifiable.

I was watching a youtube tutorial on unification which stated if a variable is trying to be unified against a term which contains that variable, then it is not unifiable.

However when I type ?- f(X) = X into prolog, it returns something along the lines of... f(f(f(f(f(f(...)))))) ?

I understand why this is... but I don't understand if this means it is unifiable or not, as I would have expected it just to return 'no' if it wasn't unifiable. Am I right in thinking that trying to unify f(X) = X fails the occurs check, thus making them not unifiable?

Answer 1

Yes, you are right: In logic, a variable x is of course not syntactically unifiable with the term f(x) on the grounds that the variable itself occurs as a strict subterm of f(x).

For this reason, the so-called occurs check causes the unification to fail.

As is correctly noted in that article, Prolog implementations typically omit the occurs check for efficiency reasons, and that can lead to unsound inferences.

However, you can always perform unification with occurs check in Prolog by using the ISO predicate unify_with_occurs_check/2. Exactly as expected, the unification you are asking about fails in that case:

?- unify_with_occurs_check(X, f(X)).
false.

Note that in some Prolog systems, you can set a flag to enable the occurs check for all unifications.

For example, in SWI-Prolog:

?- set_prolog_flag(occurs_check, true).
true.

?- X = f(X).
false.

I recommend you enable this flag to get sound results.

Unifications that require the occurs check often indicate programming errors. For this reason, you can set the flag to throw errors instead of failing silently.

See also the related question linked to by @false in the comments above, and the cited reference.