Prolog selection versus unification of MiniKanren

Question

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

“Coordination in Prolog corresponds to what is called a union in logic. However, we avoid word unification, since conformity, for reasons of efficiency, in most Prolog systems is implemented in a way that does not exactly correspond to unification. It requires a so-called presence check: does this variable have "Verification of the incident will make the match ineffective."

My questions are: if unification in miniKanren suffers from this decrease in efficiency or how is this problem solved?

Answer 1

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

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

Thirdly, it is easy to build examples in which the inclusion of verification occurs makes your programmed orders faster than disabling verification.

Fourth, using the term “match” to describe unifications that pass validation is a very bad idea: “Alignment” means one-way unification in functional languages. In Prolog, unifications always work in all directions, also if validation is disabled.

So, for part of the Prolog question, I highly recommend turning on availability checking to test your programs if your Prolog system supports it. Usually, a union is required, where the check occurs, indicates a programming error in the Prolog programs. For this reason, you can, for example, set the flag so that the system throws an exception, otherwise it would create a circular term.