What occurs-check optimizations is SWI Prolog using?

To quote the SICStus Prolog manual:

The usual mathematical theory behind Logic Programming forbids the
creation of cyclic terms, dictating that an occurs-check should be
done each time a variable is unified with a term. Unfortunately, an
occurs-check would be so expensive as to render Prolog impractical as
a programming language.

However, I ran these benchmarks (The Prolog ones) and saw fairly minor differences (less than 20%) in SWI Prolog between the occurs check (OC) being on and off:

OC is off: :- set_prolog_flag(occurs_check, false). in .swiplrc (restarted)

?- run_interleaved(10).
% 768,486,984 inferences, 91.483 CPU in 91.483 seconds (100% CPU, 8400298 Lips)

?- run(1).
'Program'            Time     GC
boyer               0.453  0.059
browse              0.395  0.000
chat_parser         0.693  0.000
crypt               0.481  0.000
fast_mu             0.628  0.000
flatten             0.584  0.000
meta_qsort          0.457  0.000
mu                  0.523  0.000
nreverse            0.406  0.000
poly_10             0.512  0.000
prover              0.625  0.000
qsort               0.574  0.000
queens_8            0.473  0.000
query               0.494  0.000
reducer             0.595  0.000
sendmore            0.619  0.000
simple_analyzer     0.620  0.000
tak                 0.486  0.000
zebra               0.529  0.000
           average  0.534  0.003

OC is on: :- set_prolog_flag(occurs_check, true). in .swiplrc (restarted)

?- run_interleaved(10).
% 853,189,814 inferences, 105.545 CPU in 105.580 seconds (100% CPU, 8083669 Lips)

?- run(1).
'Program'            Time     GC
boyer               0.572  0.060
browse              0.618  0.000
chat_parser         0.753  0.000
crypt               0.480  0.000
fast_mu             0.684  0.000
flatten             0.767  0.000
meta_qsort          0.659  0.000
mu                  0.607  0.000
nreverse            0.547  0.000
poly_10             0.541  0.000
prover              0.705  0.000
qsort               0.660  0.000
queens_8            0.491  0.000
query               0.492  0.000
reducer             0.867  0.000
sendmore            0.629  0.000
simple_analyzer     0.757  0.000
tak                 0.550  0.000
zebra               0.663  0.000
           average  0.634  0.003

Are these benchmarks not representative of real-world usage? (I remember reading somewhere that they were specifically chosen to be “fairly representative”) Is SWI Prolog implementing some optimization tricks, that SICStus people aren’t aware of, that make the cost of OC minor? If so, are they published? (I found a bunch of papers about this from the '90s, but I don’t know if they are state-of-the-art)

This question is also being discussed on StackOverflow.

1 Like

There is not that much rocket science in this respect in SWI-Prolog. Just like any Prolog system the compiler translates most (head) unification into dedicated instructions. Quite a few do not need an occurs check as we know we are unifying to a fresh variable, a ground term, etc. For those that call the general unification function (i.e., we do not know enough to do better), we do the normal unification and then we examine the trail. Each trailed (bound) variable is checked against the term it was bound to.

That is pretty much old school. I think what hits us is that in practice a vast majority of the unifications do not use the general unification procedure and even if they do, the variable is often bound to something simple and thus the check is cheap.

But, one can design programs that suffer really badly from the occurs check. Also, the benchmarks are not very representative. Very few touch unifying large terms AFAIK.


I’d be curious to see a “worst-case” for the occurs check in SWI Prolog.

Anything doing unification of a non-fresh variable against a huge term. That is quite likely to happen in programs handling huge terms. As long as the terms being processed have modest size the occurs check is fine. The error flag has helped be a couple of times to figure out why a program was producing cyclic terms :slight_smile:

Beginners try X = f(X) often enough :slight_smile:

Being inspired by the example, I have tested on the unification without OC as follows. It is very impressive that SWI-Prolog unification is very fast,which seems to be aware of structure sharing. Great! I though it was naive (but exponential order). Sorry for possibly distracting comment.

eqns(0, X, X=f(Y, Y)):-!.
eqns(N, X, (X=f(Y, Y), Eqs)):- N0 is N - 1,
	eqns(N0, Y, Eqs).
% ?- N = 20, eqns(N, X, R), eqns(N, Y, R1), call(R), call(R1),time(X=Y).
%@ % 1 inferences, 0.000 CPU in 0.000 seconds (56% CPU, 111111 Lips)
%@ N = 20,
%@ X = Y, Y = f(f(f(f(f(f(f(f(f(f(..., ...), f(..., ...)), f(f(..., ...), f(..., ...))), f(f(f(..., ...), f(..., ...)), f(f(..., ...), f(..., ...)))),  

Simply the first time the variable is introduced. It doesn’t try to do anything smart at the moment. Don’t try this at the toplevel as the goal is not compiled, so none of this works. To get more insight use vm_list/1, profile/1 and possibly an external profiling tool such as valgrind.

That is required to be able to unify cyclic terms. I’ve implemented that when adding attributed variables as programs using constraints often involve cyclic terms. Bart Demoen shared with me how to do it (which you find explained in pl-prims.c).

The call time(X=Y) doesn’t test OC, it only tests unification:

X and Y will be similar trees each a different variable in the leaves.
To test OC you need to try to unify a variable with a tree.

If you look at the VM code, you see that the binding for B is a first binding, as is dealing with the first argument of f(A,A). The second argument unifies A with the second argument of the f(A,A) term. Surely it could detect this will not create a cycle, but it doesn’t.

There are way more important things to improve then minimizing occurs checks. Of course, if someone really depends on this stuff and is able to invest, the order may change :slight_smile:

It only counts predicate calls and redos. Inlined virtual machine instructions are not counted.

I did not refer to any reordering? Why do you say that?

Here is a suspicion of mine. Concerning this equational unification problem:

Only one equation is optimized away when occurs_check=true? Right? Is this seen in the vm_list/1 which one is optimized? You only wrote “you look at the VM code”. There is the danger that I am still looking, looking, looking, … and I don’t see anything.

What should I look for in the VM code? Maybe I will figure out my self. This would explain the differing LIPS count and the differing performance. Right? It would explain the differences between /* unify_with_occurs_check/2 */ and /* (=)/2, occurs_check=true */.