Prolog matching vs miniKanren unification

Question

In Prolog - Programming for Artificial Intelligence, Bratko says the following on page 58.

"Matching in Prolog corresponds to what is called unification in logic. However, we avoid the word unification because matching, for for efficiency reasons in most Prolog systems, is implemented in a way that does not exactly correspond to unification. Proper unification requires the so-called occurs check: does a given variable occur in a given term? The occurs check would make matching inefficient."

My questions is if unification in miniKanren suffers this efficiency penalty or how is this problem solved?

Answer 1

In Prolog, the occurs check is optional. In SWI Prolog, you can turn it globally on, off, or configure Prolog to raise an error when the occurs check succeeds (which is very useful for debugging programs that are intended to run with the occurs check turned off)

On the other hand, in miniKanren, the occurs check is non-optional.

Answer 2

There are several misconceptions here. First, sound unification is available also in Prolog, using the ISO predicate unify_with_occurs_check/2.

Second, this sound unification can be enabled in some Prolog systems by default for all unifications. See for example the occurs_check Prolog flag in SWI-Prolog.

Third, it is easy to construct examples where enabling the occurs check makes your program orders of magnituted faster than disabling the check.

Fourth, using the term matching to describe unifications that omit the occurs check is a very bad idea: Matching means one-way unification in functional languages. In Prolog, unifications always work in all directions, also if the occurs check is disabled.

So, for the Prolog part of the question, I highly recommend to enable the occurs check to test your programs, if your Prolog system supports it. Usually, a unification where an occurs check is required indicates a programming error in Prolog programs. For this reason, you can for example set the flag in such a way that the system throws an exception where it would otherwise create a cyclic term.