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).
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.