What is a simple worst case for occurs check in Prolog?

Question

Many papers do note that an equational unification problem such as below, might run in exponential time, when occurs_check=true. There is no stipulation that this is a top-level query or a clause body, its just the equational unification problem:

   X1 = f(X0, X0),
   X2 = f(X1, X1),
   ..
   Xn-1 = f(Xn-2, Xn-2),
   Xn = f(Xn-1, Xn-1).

If true this could be a worst case for occurs check, since normal variable sharing unification is linear. Does every Prolog system necessarely feature this equational unification problem as a worst case?

If the Prolog system does not have an occurs_check=true flag, one could try unify_with_occurs_check/2 in place of (=)/2.

Answer 1

Here is a comparison. I tested the equational unification problem inside a clause body. Link to source code of the test and the benchmark results is at the end of this answer:

test :-
    B = f(A, A),
    C = f(B, B),
    D = f(C, C),
    X = f(D, D).

Etc..

Jekejeke Prolog 1.4.6 and SWI-Prolog 8.3.17 is still linear. Jekejeke Prolog uses a static analysis, doesn't work always. SWI-Prolog does it dynamically, I guess side effect of dealing with cyclic terms. But GNU Prolog 1.4.5 is exponential. I was using n=4, 6, 8 and 10:

Open Source:

Linear or Exponential?
https://gist.github.com/jburse/2d5fd1d3dd8436acceca52fdfc537581#file-size-pl

Answer 2

Not yet completely verified hypothesis. There is some confirmation that we can look at the VM code. There is the danger that I am still looking, looking, looking, … and I don’t see anything.

Here is a suspicion of mine for SWI-Prolog. Concerning this
equational unification problem, now inside a clause body:

X1 = f(X0, X0),
X2 = f(X1, X1),
..
Xn-1 = f(Xn-2, Xn-2),
Xn = f(Xn-1, Xn-1).

Only one equation is optimized away when occurs_check=true? This would
explain the differing LIPS count and the differing performance:

/* (=)/2, occurs_check=false */
% % 2,000,000 inferences, 0.222 CPU in 0.226 seconds (98% CPU, 9007995 Lips)

/* unify_with_occurs_check/2 */
% % 12,000,000 inferences, 1.382 CPU in 1.411 seconds (98% CPU, 8680009 Lips)

/* (=)/2, occurs_check=true */
% 11,000,000 inferences, 1.264 CPU in 1.270 seconds (100% CPU, 8704963 Lips)

Oki, Doki.