Can the unification algorithm in Prolog recurse infinitely?

Question

I am using swi-prolog to produce some examples for students in the context of a Prolog course. Regarding unification I want to draw their attention to the dangers of infinite recursion in the unification process. However, mature Prolog implementations like swi-prolog are smart enough to avoid infinite recursion of the unification process in most cases. Is this true in all cases, or can more intricate examples be constructed where unification would still recurse infinitely?

?- foo(bar(X)) = X.
X = foo(bar(X)).

?- foo(X) = X.
X = foo(X).

?- foo(X) = Y, X = Y.
X = Y, Y = foo(Y).

?- foo(X) = Y, X = foo(Y).
X = Y, Y = foo(foo(Y)).

As a related side-question, why does (again, I used swi-prolog) unification binds X to Y in the following example? I didn't expect that.

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

Answer 1

It all depends on what you understand by unification algorithm and by Prolog.

Your examples suggest that you are interested in syntactic unification. Here, unification is well defined and terminating as long as it is NSTO (not subject to occurs-check). All Prologs agree here.

Many Prologs offer rational tree unification. SWI offers it since 5.3 of 2004. And also this algorithm is terminating. Given these assumptions, the answer to your question is no, it cannot recurse infinitely.

However, the usefulness of rational trees for programming is rather limited. Its major motivation were efficiency considerations. Namely, variable-term unifications with occurs-check cost up to the size of term, only sometimes they can be reduced to constant cost. But they are always constant for rational trees.

As your interest is rather focused towards teaching, consider to avoid the creation of infinite trees by changing the unification algorithm like so (SWI since 5.6.38, Scryer) :

?- set_prolog_flag(occurs_check, error).
true.

?- X = f(X).
ERROR: =/2: Cannot unify _G2368 with f(_G2368): would create an infinite tree

For the time of development of a program, this flag can be left enabled. And it will help students to locate errors. As long as there is no such error, the program will produce exactly the same result also with rational tree unification.

So much for syntactic unification. In general, in the presence of constraints or coroutines there is no guarantee for termination. Think of

inf :- inf.

?- freeze(X, inf), X = 1.

For your side-question, this is a particularity of SWI's top level which helps to spot identical terms in an answer.

?- X = 1, Y = 1.
X = Y, Y = 1.

Answer 2

Is this true in all cases, or can more intricate examples be constructed where unification would still recurse infinitely?

AFAIK no.

I can't recall seeing where =/2 did not work as expected. Granted my expectations are of how SWI-Prolog does =/2 as noted below.

---

As a related side-question, why does (again, I used swi-prolog) unification binds X to Y in the following example? I didn't expect that.

See these comments in the SWI-Prolog C code for cyclic terms.

/* - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - -
Cyclic term unification. The algorithm has been  described to me by Bart
Demoen. Here it is (translated from dutch):
I created my own variation. You only need it during general unification.
Here is a short description:  suppose  you   unify  2  terms  f(...) and
f(...), which are represented on the heap (=global stack) as:
     +-----+          and     +-----+
     | f/3 |                  | f/3 |
     +-----+                  +-----+
      args                     args'
Before working on args and args', change  this into the structure below,
using a reference pointer pointing from functor  of the one to the other
term.
     +-----+          and      +-----+
     | ----+----------------->| f/3 |
     +-----+                  +-----+
      args                     args'
If, during this unification you  find  a   compound  whose  functor is a
reference to the term at the right hand you know you hit a cycle and the
terms are the same.
Of course functor_t must be different from ref. Overwritten functors are
collected in a stack and  reset   regardless  of whether the unification
succeeded or failed.
Note that we need to  dereference  the   functors  both  left and right.
References at the right are rare, but possible. The trick is to use both
sharing and cycles, where the cycles at the left are shorter:
t :-
    X = s(X),       Y = y(X,X),
    A = s(s(s(A))), B = y(A,A),
    Y = B.
While unifying the first argument of y/2, the left-walker crosses to the
right after the first cycle  and  creates   references  in  A, which are
processed by the right-walker when entering the second argument of y/2.
Initial measurements show a performance degradation for deep unification
of approx. 30%. On the other hand,  if subterms appear multiple times in
a term unification can be much faster. As only a small percentage of the
unifications of a realistic program are   covered by unify() and involve
deep unification the overall impact of performance is small (< 3%).
- - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - */