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?

Vandervelde

Answer 1

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.

Geodetic

"A unification where an occurs check is required indicates a programming error": you could be even more explicit about that point. I still have to see a good practical example of Prolog code that needs cyclic terms. Do you know of such examples? – Abnegate

A related question: can you show or link to realistic examples where occurs check makes the program faster, resp. slower? I have to admit that I have never attempted to use cyclic terms, and simply used the vanilla unification (without occurs check) because I assumed that it did not matter. – Abnegate

I have once seen an ingenious application of cyclic terms by Stefan Kral, where he used cyclic terms to represent the infinite tape of a Turing machine (initially filled with 0), starting with Tape = [0|Tape], and proceeding from there. For a realistic example that works hundreds of times faster with occurs check, see Ulrich Neumerkel at al. "Declarative Language Extensions for Prolog Courses". – Geodetic

@Boris: A "practical" example for infinite trees is the current implementation of CHR in SWI. – Zionism

@Boris Coinduction makes a good case for cyclic terms. See e.g. github.com/LogtalkDotOrg/logtalk3/tree/master/examples/… for several examples. – Susumu

If neither “matching” not “unification” are a good words to designate this case, what could be a good word? Could “assignment” be a better word? – Viridian

Answer 2

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.

Margarethe