What are the main technical differences between Prolog and miniKanren, with respect to logic programming?

Question

When I want to read up on logic programming I always stumble over two "main" ways to do it nowadays:

• miniKanren, a minilanguage introduced in The Reasoned Schemer and popular at the moment due to core.logic.
• Prolog, the first "big" logic programming language.

What I'm interested in now: What are the principal technical differences between the two? Are they very similar in approach and implementation, or do they take completely different approaches to logic programming? Which branches of mathematics do they come from, and what are the theoretical foundations?

Solution 1

First, allow me to compliment you on your fine pw0n1e icon.

This is a tricky question to answer, largely because there are so many variants of both miniKanren and Prolog. miniKanren and Prolog are really families of languages, which makes it difficult to compare their features, or even how they are used in practice. Because of this, please take everything I'm about to say with caution: if I say that Prolog uses depth-first search, be aware that many Prolog implementations support other search strategies, and that alternate search strategies can also be encoded at the meta-interpreter level. Still, miniKanren and Prolog have different design philosophies, and make different trade-offs.

Prolog is one of the two classic languages for symbolic artificial intelligence programming (the other classic language being Lisp). Prolog excels at implementing symbolic rule-based systems in which declarative knowledge is encoded in first-order logic. The language is optimized for expressiveness and efficiency for these types of applications, sometimes at the expense of logical purity. For example, by default Prolog does not use the "occur check" in unification. From a math/logic standpoint, this version of unification is incorrect. However, the occur check is expensive, and in most cases the lack of the occur check is not a problem. This is a very pragmatic design decision, as is Prolog's use of depth-first search, and use of cut (!) to control backtracking. I'm sure these decisions were absolutely necessary when running on the hardware of the 1970s, and today are very useful when working on large problems, and when dealing with huge (often infinite!) search spaces.

Prolog supports many "extra-logical" or "non-logical" features, including cut, assert and retract, projection of variables for arithmetic using is, and so forth. Many of these features make it easier to express complex control flow, and to manipulate Prolog's global database of facts. One very interesting feature of Prolog is that Prolog code is itself stored in the global database of facts, and can be queried against at run time. This makes it trivial to write meta-interpreters that modify the behavior of Prolog code under interpretation. For example, it is possible to encode breadth-first search in Prolog using a meta-interpreter that changes the search order. This is an extremely powerful technique that is not well known outside of the Prolog world. 'The Art of Prolog' describes this technique in detail.

Tremendous effort has gone into improving Prolog implementations, most of which are based on the Warren Abstract Machine (WAM). The WAM uses a side-effecting model in which values are destructively assigned to logic variables, with these side-effects being undone upon backtracking. Many features can be added to Prolog by extending the instructions of the WAM. One disadvantage of this approach is that Prolog implementation papers can be difficult to read without a solid understanding of the WAM. On the other hand, Prolog implementer have a common model for discussing implementation issues. There has been a great deal of research in parallel Prolog, culminating in Andorra Prolog in the 1990s. At least some of these ideas live on in Ciao Prolog. (Ciao Prolog is full of interesting ideas, many of which go far beyond the Prolog standard.)

Prolog has a beautiful unification-based "pattern-matching"-style syntax that results in very succinct programs. Prologers love their syntax, just like Lispers love their s-expressions. Prolog also has a large library of standard predicates. Due to all of the engineering that has gone into making the WAM fast, there are very capable and mature Prolog implementations. As a result, many large knowledge-based systems have been written entirely in Prolog.

miniKanren was designed as a minimal logic programming language, with a small, easily understandable, and easily hackable implementation. miniKanren was originally embedded in Scheme, and has been ported to dozens of other host languages over the past decade. The most popular miniKanren implementation is 'core.logic' in Clojure, which now has many Prolog-like extensions and a number of optimizations. Recently the core of the miniKanren implementation has been simplified even further, resulting in a tiny "micro kernel" called "microKanren." miniKanren can then be implemented on top of this microKanren core. Porting microKanren or miniKanren to a new host language has become a standard exercise for programmers learning miniKanren. As a result, most popular high-level languages have at least one miniKanren or microKanren implementation.

The standard implementations of miniKanren and microKanren contain no mutation or other side-effects, with a single exception: some versions of miniKanren use pointer equality for comparison of logic variables. I consider this a "benign effect," although many implementations avoid even this effect by passing a counter through the implementation. There is also no global fact database. miniKanren's implementation philosophy is inspired by functional programming: mutation and effects should be avoided, and all language constructs should respect lexical scope. If you look carefully at the implementation you might even spot a couple of monads. The search implementation is based on combining and manipulating lazy streams, once again without using mutation. These implementation choices lead to very different trade-offs than in Prolog. In Prolog, variable lookup is constant time, but backtracking requires undoing side-effects. In miniKanren variable lookup is more expensive, but backtracking is "free." In fact, there is no backtracking in miniKanren, due to how the streams are handled.

One interesting aspect of the miniKanren implementation is that the code is inherently thread-safe and---at least in theory---trivially parallelizable. Of course, parallelizing the code without making it slower is not trivial, given that each thread or process must be given enough work to make up for the overhead of parallelization. Still, this is an area of miniKanren implementation that I hope will receive more attention and experimentation.

miniKanren uses the occur check for unification, and uses a complete interleaving search instead of depth-first search. Interleaving search uses more memory than depth-first search, but can find answers in some cases in which depth-first search will diverge/loop forever. miniKanren does support a few extra-logical operators---conda, condu, and project, for example. conda and condu can be used to simulate Prolog's cut, and project can be used to get the value associated with a logic variable.

The presence of conda, condu, and project---and the ability to easily modify the search strategy---allows programmers to use miniKanren as an embedded Prolog-like language. This is especially true for users of Clojure's 'core.logic', which includes many Prolog-like extensions. This "pragmatic" use of miniKanren seems to account for the majority of miniKanren's use in industry. Programmers who want to add a knowledge-based reasoning system to an existing application written in Clojure or Python or JavaScript are generally not interested in rewriting their entire application in Prolog. Embedding a small logic programming language in Clojure or Python is much more appealing. An embedded Prolog implementation would work just as well for this purpose, presumably. I suspect miniKanren has become popular as an embedded logic language because of the tiny and pure core implementation, along with the talks, blog posts, tutorials, and other educational materials that have come out since 'The Reasoned Schemer' was published.

In addition to the use of miniKanren as a pragmatic embedded logic programming language similar in spirit to Prolog, miniKanren is being used for research in "relational" programming. That is, in writing programs that behave as mathematical relations rather than mathematical functions. For example, in Scheme the append function can append two lists, returning a new list: the function call (append '(a b c) '(d e)) returns the list (a b c d e). We can, however, also treat append as a three-place relation rather than as a two-argument function. The call (appendo '(a b c) '(d e) Z) would then associate the logic variable Z with the list (a b c d e). Of course things get more interesting when we place logic variables in other positions. The call (appendo X '(d e) '(a b c d e)) associates X with (a b c), while the call (appendo X Y '(a b c d e)) associates X and Y with pairs of lists that, when appended, are equal to (a b c d e). For example X = (a b) and Y = (c d e) are one such pair of values. We can also write (appendo X Y Z), which will produce infinitely many triples of lists X, Y, and Z such that appending X to Y produces Z.

This relational version of append can be easily expressed in Prolog, and indeed is shown in many Prolog tutorials. In practice, more complex Prolog programs tend to use at least a few extra-logical features, such as cut, which inhibit the ability to treat the resulting program as a relation. In contrast, miniKanren is explicitly designed to support this style of relational programming. More recent versions of miniKanren have support for symbolic constraint solving (symbolo, numbero, absento, disequality constraints, nominal logic programming) to make it easier to write non-trivial programs as relations. In practice I never use any of the extra-logical features of miniKanren, and I write all of my miniKanren programs as relations. The most interesting relational programs are the relational interpreters for a subset of Scheme. These interpreters have many interesting abilities, such as generating a million Scheme programs that evaluate to the list (I love you), or trivially generating quines (programs that evaluate to themselves).

miniKanren makes a number of trade-offs to enable this relational style of programming, which are very different from the trade-offs Prolog makes. Over time miniKanren has added more symbolic constraints, really becoming a symbolically-oriented Constraint Logic Programming language. In many cases these symbolic constraints make it practical to avoid using extra-logical operators like condu and project. In other cases, these symbolic constraints are not sufficient. Better support for symbolic constraints is one active area of miniKanren research, along with the broader question of how to write larger and more complex programs as relations.

In short, both miniKanren and Prolog have interesting features, implementations, and uses, and I think it is worth learning the ideas from both languages. There are other very interesting logic programming languages as well, such as Mercury, Curry, and Gödel, each of which has its own take on logic programming.

I'll end with a few miniKanren resources:

The main miniKanren website: http://minikanren.org/

An interview I gave on relational programming and miniKanren, including a comparison with Prolog: http://www.infoq.com/interviews/byrd-relational-programming-minikanren

Cheers,

--Will

Solution 2

Tentative answer:

AFAIK, "The Reasoned Schemer" introduced basic logic programming in a Scheme-y syntax and functional programming style, adding in particular the constant goals "#u" (fail) and "#s" (suceeed) to the boolean values "#t" and "#f". It used the same approach to logic programming as Prolog: Unification and backtracking search. I will see whether I have some time to retrieve that book from my shelf over the weekend. The branch of mathematics is a restricted form first-order logic, in this case Horn clauses, and the Resolution Unfication. See: Computational Logic: Memories of the Past and Challenges for the Future by John Alan Robinson and The early years of logic programming by Robert Kowalski for a cold start.

Comments

[false]

What do these two citations have to do with Kanren, or MiniKanren?

[Profpatsch]

Excuse me if I’m blown away right now. I just started the first thought experiments in logic and constraint-based programming and that’s the reply I get. :) Actually, as you mentioned in your answer, too, I had a strong suspicion logic computation was a perfect candidate to implement as a Monad; turns out it’s more of a MonadPlus and there is indeed a paper and reference implementation by your colleague Friedman! So I’m reading that and playing with it now, any thoughts about it?

[William E. Byrd]

I suspect you would also find the microKanren paper and code interesting: webyrd.net/scheme-2013/papers/HemannMuKanren2013.pdf and github.com/jasonhemann/microKanren

[William E. Byrd]

Also, I organize a weekly miniKanren uncourse on Google Hangouts, Sundays at 3pm Eastern time (GMT -5:00). I always tweet the link from my @webyrd Twitter account, if you would like to join us. Previous recorded hangouts are at: youtube.com/playlist?list=PLO4TbomOdn2cks2n5PvifialL8kQwt0aW

[Profpatsch]

Indeed, (define (mplus …) …) :). This has sprung out of the '05 paper, I assume?

[William E. Byrd]

I think it's basically the same search monad as in the '05 paper. Also, see 'Embedding Prolog in Haskell' by Seres and Spivey: spivey.oriel.ox.ac.uk/~mike/silvija/seres_haskell99.pdf

[Robert Oschler]

@WilliamE.Byrd - Awesome answer! Assuming there is one, what is the best miniKanren implementation that can be embedded in a C/C++ program? Also, does miniKanren have Prolog's generative nature? That is, the ability to leave a variable in an expression unground and the core engine will generate all the possible values for the unground variable given the current relations declared by the program?

[William E. Byrd]

Good question, Robert. I haven't seen any implementations for C or C++ yet. It should be straight forward to port microKanren to C++, now that it has lambdas. C seems trickier, since it doesn't have closures. A simple miniKanren-to-C compiler might be more useful than an embedding.

[William E. Byrd]

In a miniKanren program written as a relation, you can place logic variables anywhere in a query and miniKanren will try to instantiate those variables with legal values. I usually write my relations to produce answers that are as general as possible. For example, instead of an infinite stream of integers bound to some logic variable X, I generally prefer the single answer that X is an unbound logic variable representing some integer.

[Zachary K]

Well there are (or at least used to be ) Scheme to C compilers, gambit for one had one. So I guess you could use one of those to do something with running a miniKanren on C

[CMCDragonkai]

Would love to see this kind of comparison on your website, but also I've been learning Mercury, and I would like to know what the main differences are too between MiniKanren and Mercury?

[Robert Oschler]

@WilliamE.Byrd Robert here again. Does miniKanren have the generational trait that Prolog has? I'm referring to one of my favorite aspects of Prolog, where you can leave a variable ungrounded and by repeatedly failing the goal, have all the possible values for the ungrounded variable(s) be provided by the Prolog inference engine. Does MiniKanren have that behavior?

[William E. Byrd]

Hey Robert! miniKanren will try to give the most general answer when possible, with a fresh (uninstantiated) variable being most general. If the most general answers really are ground, passing a logic variable to a miniKanren query will indeed generate all possible ground instantiations.

[CMCDragonkai]

By the way, what's the reason behind naming functions like appendo instead of just append?

[user1025901]

See the last question: "Which branches of mathematics do they come from, and what are the theoretical foundations?"

[aoeu256]

Having code change the interpreter, and then maybe revert the previous interpreter sounds powerful in both Lisp and Prolog, I want to know more about this. I want to implement an ambiguous eval that tries to reorder your expressions / or function definition so that it works on error. This will help me avoid dumb mistakes when coding. Also it'd be nice to implement a good google-like search database on minikanren to find code from a huge database of open-source code, and to help reduce the size of code via looking at your code and telling you other ways of implementing it.

[X10D]

what-data-would-have-to-be-passed-to-minikanren-to-get-eval?‌​: stackoverflow.com/questions/61574010/…

[IFcoltransG]

@CMCDragonkai The o is for relations as opposed to regular functions. There's more info in 'Relational Programming in miniKanren' Byrd et al., section 1.5 Typographical Conventions.