Prologue: Is f (X) = X unified or not?

Question

My understanding of unification is a bit patchy. I understand the basic unification, but I am having problems so that my members do not coincide with terms that are not unified.

I watched the YouTube unification tutorial, which said that a variable is trying to combine with a term that contains this variable, then it is not unified.

However, when I enter ?- f(X) = X into the prolog, does it return something along the lines ... f(f(f(f(f(f(...)))))) ?

I understand why this is so ... but I do not understand if this means that it is unified or not, as I expected it to simply return “no” if it is not unified. Do I correctly believe that the attempt to unify f (X) = X does not allow verification, which makes them not unified?

Answer 1

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

For this reason, the so-called check appears , which leads to a failure of the union.

As correctly noted in this article, Prolog implementations usually omit the availability check for performance reasons, which can lead to unfounded conclusions.

However, you can always perform unification with verification in Prolog using the ISO predicate unify_with_occurs_check/2 . Exactly as expected, the union you are asking about does not work in this case:

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

Please note that on some Prolog systems you can set a flag to enable checking for all unifications.

For example, in SWI-Prolog:

  ? - set_prolog_flag (occurs_check, true).
 true

 ? - X = f (X).
 false

I recommend that you enable this flag to get sound results.

Unifications requiring verification often indicate programming errors. For this reason, you can set a flag to throw errors instead of failing.

See also the related question related to @false in the comments above, and the link provided.