The big star of the logic-programming world at Clojure/conj 2011 was undeniably clojure.core.logic. David Nolen, Ambrose Bonnaire-Sergeant, and others have done great work on this library, but they have been focused on features, not documentation.

The definitive documentation is actually a book, The Reasoned Schemer, written in 2005 by the creators of the miniKanren logic programming system, on which core.logic is based. The Reasoned Schemer is still a good book, but its examples are in Scheme, not Clojure, and there are some small but significant differences between the implementation presented there and the one in core.logic.

Suffice to say, getting started with core.logic can be a daunting experience. This post will not attempt to explain everything about logic programming, but I will try to give you a leg up running core.logic for the first time, then introduce a few basic commands. I will assume no prior experience with Scheme or any logic programming system. This introduction is not quite enough to begin writing interesting programs in core.logic: that will have to wait for another post.

Quick Start

Create a new Leiningen project:

  lein new logicfun
  cd logicfun

Edit project.clj to match the following:

  (defproject logicfun "1.0.0-SNAPSHOT"
    :dependencies [[org.clojure/clojure "1.3.0"]
                   [org.clojure/core.logic "0.6.6"]])

Run lein repl and start typing:

  user=> (use 'clojure.core.logic)

You will see a warning like this:

  WARNING: == already refers to: #'clojure.core/== in namespace:
  user, being replaced by: #'clojure.core.logic/==

You can ignore the warning. Core.logic reuses the == symbol to mean unify. We'll get to examples of unification in a moment.

Writing Logic Programs

The main entry point of every core.logic program is the run macro:

  (run number-of-results [variable] & goals)

Basically, this is asking the logic engine to find all possible values of variable that meet the criteria specified in the goals. It will stop after it has found number-of-results values.

A variant called run* omits the number-of-results argument: it will keep going until it finds all possible solutions. Be aware that the set of all possible solutions may be infinite, in which case run* will never return!

The result of a logic program is always a list of values, which may include unbound variables, represented by symbols like _.0, _.1, and so on. An empty logic program returns a single unbound variable:

  user=> (run 1 [q])
  (_.0)

We asked, in effect, "What is one possible value of q?" without saying anything more about the value of q. (Logic programming examples often use q, which you can think of as the "query variable.") Not surprisingly, core.logic replied that q can be anything, indicated by the unbound variable _.0.

A slightly longer example specifies a condition for q:

  user=> (run 1 [q] (== 4 q))
  (4)

This program asked "What is one possible value of q such that q can be unified with 4?" We got the obvious answer: q is 4. In this instance, we used unification to declare that two things must be equal.

The expressions in the body of run, known as "goals" in logic-speak, are AND-ed together. If we specify goals that are impossible to satisfy, we get an empty list of results:

  user=> (run 1 [q] (== 4 q) (== 5 q))
  ()

The variable q cannot be both 4 and 5 at the same time, so the program returns an empty list.

conde

We can introduce the notion of OR into a logic program with the conde macro, which is similar to Clojure's cond, except that each clause consists of one or more expressions inside a vector. (Syntactically, this is more like Scheme's cond.)

  user=> (run 1 [q]
              (conde [(== 4 q)]
                     [(== 5 q)]))
  (4)

Here we said, "Give me values of q such that q is 4 OR q is 5." So why did we only get one response? Because we only asked for one! If we ask for two values, we get both:

  user=> (run 2 [q]
              (conde [(== 4 q)]
                     [(== 5 q)]))
  (4 5)

Notice that, unlike Clojure's cond, processing does not stop after the first clause matches. As long as more values are wanted, all conde clauses will eventually be tried. The e in conde stands for "every line."

The expressions inside each vector we give to conde are AND-ed together just like expressions inside run:

  user=> (run 2 [q]
              (conde [(== 4 q) (== 7 q)]
                     [(== 5 q)]))
  (5)

The first conde clause in that program says that q must be both 4 AND 7, which is impossible, so it produces no results. Even though we asked for two results, core.logic was only able to find one, from the second conde clause.

fresh

The fresh macro introduces new variables into our logic program, similar to how let introduces new local variables into a normal Clojure program. Unlike let, we don't supply any initial values for the logic variables in fresh.

  user=> (run 1 [q]
              (fresh [a b]
                (== a 4)
                (== b 5)
                (== q [a b])))
  ([4 5])

This example creates two new logical variables a and b, places constraints on each, then says that the query variable q is a vector containing a and b. This demonstrates another feature of the unification operator ==: it can be used to gather up values in data structures. This is useful when we want multiple results, since we can never have more than one query variable in run.

The unification process is similar to Clojure's destructuring forms, but it is more general because it works in both directions. That is, the order of expressions doesn't matter to the == operator. This program is the same as the previous one:

  user=> (run 1 [q]
              (fresh [a b]
                (== 4 a)
                (== b 5)
                (== [a b] q)))
  ([4 5])

Some logic programming systems, such as Prolog and Datalog, do not require logic variables to be declared before they are used, so they have no equivalent of fresh.

Logic, Scheme, and Clojure

This post came out of my first serious attempt to learn how core.logic works. I have tried hard not to say anything incorrect or misleading, but experts would doubtless quibble with some of my terminology.

If core.logic has one weakness, it's that it is essentially a direct port of the miniKanren implementation in Scheme. The syntax is Scheme-ish rather than Clojure-ish. It even defines its own cons operator to behave more like Scheme's cons. Some of these differences may be necessary for the implementation to work, but it makes the learning curve just a bit steeper. Also, most of the introductions to core.logic assume some prior experience with Scheme and/or The Reasoned Schemer. Hopefully, once the foundations of a working logic system are complete, the authors or other contributors will be able to make it more accessible.

I hope to extend this series further in the coming weeks, as I learn more about how to write programs in core.logic. I will also investigate other logic languages, such as Datalog (via Cascalog).