Do modern Prolog compilers optimize away the occurs check automatically, when it's safe?

Question

Edit: This question assumes you enabled the occurs check. It's not about setting Prolog flags.

There was a bunch of papers 30 years ago about optimizing away the occurs check automatically, when it's safe (about 90% of predicates, in typical codebases). Different algorithms were proposed. Do modern Prolog compilers (such as SWI Prolog) do anything like that (when the occurs check is turned on)? What algorithms do they favor?

As an example, would they remove the occurs check when compiling a predicate such as this:

less(0, s(_)).
less(s(X), s(Y)) :- less(X, Y).

(from the discussion below this answer)

Answer 1

There are a variety of optimizations that can optimize away the occurs check when the occurs check flag is set to "true". This is necessary to make sound unification feasible for common cases. A typical optimization is the detection of linearity of a head:

linear(Head) :-
   term_variables(Head, Vars),
   term_singletons(Head, Singletons),
   Vars == Singletons.

In this case the occurs check can be omitted when invoking a clause. We can make the test for the less/2 example whether the heads are linear or not. It turns out that both heads are linear:

?- linear(less(0, s(_))).
true.

?- linear(less(s(X), s(Y))).
true.

So a Prolog system can totally omit the occurs check for the predicate less/2 and nevertheless produce sound unification. This optimization is for example seen in Jekejeke Prolog when inspecting the intermediate code. The instruction unify_linear is used:

?- vm_list(less/2).

less(0, s(A)).
  0  unify_linear _0, 0
  1  unify_linear _1, s(A)
less(s(X), s(Y)) :-
   less(X, Y).
  0  unify_linear _0, s(X)
  1  unify_linear _1, s(Y)
  2  goal_last less(X, Y)

In contrast to the instruction unify_term, the instruction unify_linear does not perform an occurs check, even when the occurs check flag is set to true.

Ritu Chadha; David A. Plaisted (1994). "Correctness of unification without occur check in prolog". The Journal of Logic Programming. 18 (2): 99–122. doi:10.1016/0743-1066(94)90048-5.

Answer 2

SWI Prolog does not switch on the occurs check unless you specifically ask it to:

• By using unify_with_occurs_check/2 instead of = locally. (Note that this means head unification is not affected, i.e. still runs without occurs check - I think?)
• By switching on occurs check globally thorugh setting the flag occurs_check: set_prolog_flag(occurs_check,true)

Is this a problem? I don't think so.

Consider the related case of having assertions in other programming languages (or even in Prolog for that matter: assertion/1, I heartily recommend it).

When you develop, you will have those "switched on" to verify constraints at runtime at some CPU cost. Once you are sure your program works (by consruction, prrof, and testing), you will "switch them off". Interfaces between your program and any caller (who may be malicious, confused or buggy) may still be guarded by must_be/2 checks so that interface contracts are enforced.

The case of the occurs check would be similar: If you suspect that cyclic data structures may occur and lead to problems, switch 'occurs check' on. Code you program so that everything works right (and you are sure that it works right, preferably by construction and proof). Then switch it off again.

Answer 3

Whats also popular, using a distinction inside the variables, like "fresh" and "stale" variables. "fresh" variables typically don't need an occurs check.

The distinction can be made dynamically. Here are some results, the dynamic distinction ("Freshness") can be also combined with some static analysis ("Linear"):

The above graph shows the result of a heuristic based on reference counting. The below paper discusses using one bit, i.e. tagging variables as UNBOUND or NEW_UNBOUND.

The Occur-Check Problem Revisited - Beer, 1988
https://core.ac.uk/download/pdf/82747799.pdf