6

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?

Wolff
  • 1,051
  • 3
  • 18
  • 31
  • 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 Nov 17 '15 at 00:59
  • 3
    If you read, for example, [here](http://www.swi-prolog.org/pldoc/man?predicate=unify_with_occurs_check%2f2) and [here](http://www.swi-prolog.org/pldoc/man?section=flags#flag:occurs_check), 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 Nov 17 '15 at 01:09
  • @lurker I'm using Prolog specifically, but I'm talking more in general logic. I assumed Prolog would just be the same. – Wolff Nov 17 '15 at 01:13
  • 3
    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 Nov 17 '15 at 01:24
  • 1
    @lurker this should be an answer! – Thanos Tintinidis Nov 17 '15 at 10:13
  • Search for prolog + coinduction. E.g. see http://stackoverflow.com/questions/26963657/is-an-infinite-list-of-ones-sane – Paulo Moura Nov 17 '15 at 11:55
  • 1
    See [this answer](http://stackoverflow.com/a/33753953/772868) plus references. – false Nov 17 '15 at 12:15

1 Answers1

6

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.

Community
  • 1
  • 1
mat
  • 40,498
  • 3
  • 51
  • 78
  • 1
    Please do not forget to mention `set_prolog_flag(occurs_check, error)` which is probably the best for beginners. – false Nov 18 '15 at 11:49
  • What is an example of unsound inference when unification allows cyclic terms? – Hibou57 Oct 17 '20 at 12:31