prologoccurs-check

Why `f(a)=a` fails but `f(X)=X` succeeds in prolog?


I came across following:

?- f(X) = X.
X = f(X).

?- f(a) = a.
false.

Why unification works for f(X) = X, but not for f(a) = a? Is it because first simply says name return value of f(X) as X, whereas second tries to check if return value of f(a) is a? But f() is undefined here!! Also, I guess, there is no such concept as "return value" in prolog. Then, whats going on here?


Solution

  • In your first example, X is a variable (identifier starts with capital letter, look it up). A free variable unifies with anything. (almost anything. you are creating a cyclic term, this will not work if you try to "unify with occurs check", look it up).

    In your second example, a is an atom. It only unifies with a free variable or with itself. Since f(a) is not a the unification fails.

    You are correct that there is no such thing as "return value". You might treat the success or failure of a goal as the "return value", but I don't know how much this helps.

    Either way, there is no f() in Prolog. This is not a function. You don't need to define it. It is just a compound term (look it up). It is a data structure, in a way.