What occurs-check optimizations is SWI Prolog using?

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.

2 Likes