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?

For something to be unifiable it must be so with something else. So when you as Is f(X) = X unifiable? do you really mean, Is f(X) unifiable with X? By the way, which Prolog implementation are you using? DIfferent Prologs respond differently to f(X) = X. — lurker
If you read, for example, here and here, you'll find that the answer is: it depends. It depends upon whether your Prolog does an occurs check, or supports it as an option. According to the SWI documentation, with a query such as f(X) = X, unification succeeds, creating an infinite tree if occurs_check is set to false. If occurs_check is set to true, then unification will fail. — lurker
As I mentioned in my prior comment, X is unifiable with f(X) depending upon the system and its settings. Unless you're asking if it should be unifiable, ever, logically, which is a matter of opinion. — lurker

mat mat · Accepted Answer · 2015-11-18T10:31:29

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.

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

1 Answers