2

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.

  • What if the OC stores the variables it follows in a hash table (so that it doesn't follow the same variable twice) and also ignores "fresh" variables. What would be the worst possible case for it then? – MWB Jan 10 '21 at 21:56
  • *"Take a fresh clause head eq(X,X), if you unify it with a goal eq(Y, f(Y)), it will be STO."* Here, you do `X = Y` first. They are both fresh. After that, they are no longer fresh. [Jan W used the term](https://swi-prolog.discourse.group/t/what-occurs-check-optimizations-is-swi-prolog-using/3461/2) – MWB Jan 11 '21 at 00:39
  • @MaxB: *it follows in a hash table* Marking is sufficient in many implementations. – false Jan 11 '21 at 12:59

2 Answers2

0

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:

enter image description here

Open Source:

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

0

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.