How does Prolog match "X = father (X)"?

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

?- father(X) = X.


The prologue responded as follows:

X = father(X).


But the book says that Prolog should respond like this:

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


Why is this happening?


source to share

1 answer


The Prologue is probably old.

The Prolog interpreter is most likely much newer. Also, your interpreter is smart enough to write the looping term very compactly.

Longer story

The Prolog execution engine is based on syntactic unification of conditions. Union is similar to pattern matching . However, no more than one side of the equation sign may occur in pattern matching. With only variables can be on both sides.

This allows you to create cyclical terms i.e. terms that contain themselves as a subterm.

You can explicitly disallow the creation of these terms during unification by performing a " check check " which causes unification to fail these cases. The built-in Prolog predicate unify_with_occurs_check/2

does this as its name suggests, and fails in such cases.

Your initial request:

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


Using the built-in predicate unify_with_occurs_check/2


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


Set the flag occurs_check

to do all the unifications to do the presence 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"




All Articles