3

In Prolog I entered following query to check if they match:

?- father(X) = X.

Prolog responded with this:

X = father(X).

But in the book it is written that Prolog should respond like this:

X = father(father(father(father(father(father(...)))))))))).

Why is this happening?

repeat
  • 18,496
  • 4
  • 54
  • 166
theCaveman
  • 43
  • 7
  • 1
    The answer depends on your prolog system, but it always depends on the system's respective recursion detection. – Patrick J. S. Apr 24 '15 at 17:39
  • 1
    See also [What does Prolog do if you `X = f(X)`](http://stackoverflow.com/questions/29709501/what-does-prolog-do-if-you-x-fx) – lurker Apr 24 '15 at 20:08

1 Answers1

3

Short story

The Prolog book is probably old.

The Prolog interpreter is most likely a lot newer. Also, your interpreter is smart enough to write a cyclic term very compactly.

Longer story

At the heart of Prolog's execution mechanism lies syntactic unification of terms. Unification has similarities with pattern matching. However, with pattern matching variables may occur on at most one side of the equation sign. With unification variables may occur on both sides.

This makes it possible to construct cyclic terms, i.e., terms that contain themselves as a subterm.

It is possible to explicitly prevent these terms from being created during unification by performing an "occurs check"---causing unification to fail in these cases. The Prolog builtin predicate unify_with_occurs_check/2 does as its name suggests and fails in such cases.

Your initial query:

?- X = father(X).
X = father(X).            % unification succeeds, but creates cyclic term

Using the builtin predicate unify_with_occurs_check/2:

?- unify_with_occurs_check(X,father(X)).
false.                    % "occur check" causes unification failure

Let's set the flag occurs_check to make all unifications have an "occurs check":

?- set_prolog_flag(occurs_check,true).
true.                     % all following unifications will do "occurs check"

?- X = father(X).         % the exact same query succeeded above.
false.                    % here it fails because of the "occurs check"
repeat
  • 18,496
  • 4
  • 54
  • 166