3

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?

false
  • 10,264
  • 13
  • 101
  • 209
Rnj
  • 1,067
  • 1
  • 8
  • 23
  • Say `set_prolog_flag(occurs_check, true)` and you get what you (reasonably) expect. Otherwise `unify_with_occurs_check(f(X), X)` in place of `f(X) = X`. – false Feb 23 '21 at 08:01
  • @false With occurs check, you get what _you_ expect ;-) OP doesn't seem to expect anything in particular. – TA_intern Feb 23 '21 at 08:13
  • @TA_intern: He drew an analogy to another case. Very reasonably so. – false Feb 23 '21 at 08:26
  • Am new to both logic and prolog. So please correct if wrong: Unification with occurs check first check if the structure contains the variable with which it has to unify. If it does, it fails unification. If does not then unification proceeds. By default, in prolog, unification is done without occur check. We have to either set `occurs_check` flag to always do unification with occurs check or we can use `unify_with_occurs_check()` to unify once with occurs check. – Rnj Feb 23 '21 at 10:49
  • 1
    Right! There is a third option, `set_prolog_flag(occurs_check, error)` which produces an error, should the occurs check be of relevance. And, finally, even a fourth option, `X = s(X), acyclic_term(X)` which ensures that `X` is not an infinite, rational tree which it is in this case. – false Feb 23 '21 at 11:17

1 Answers1

1

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.

TA_intern
  • 2,222
  • 4
  • 12
  • Am new to both logic and prolog. So please correct if wrong: Unification with occurs check first check if the structure contains the variable with which it has to unify. If it does, it fails unification. If does not then unification proceeds. By default, in prolog, unification is done without occur check. We have to either set `occurs_check` flag to always do unification with occurs check or we can use `unify_with_occurs_check()` to unify once with occurs check. – Rnj Feb 23 '21 at 10:48
  • @Rnj I guess it depends on the details of the Prolog implementation you are using. Unification with occurs check in SWI-Prolog _does not create a cyclic term_. About the flags and such, see the comment by user false. – TA_intern Feb 23 '21 at 14:22