More Core.logic

This is a reprise of an earlier post where I explained how to make Clojure’s core.logic library parallel using fork/join. Since then, I implemented a new monads library using Clojure’s protocols. So showing their effect on the code was in order. A couple of nice little surprises came out of the effort.

The core

There a couple core pieces to miniKanren. The unifier, a lazy stream implementation and a variant of the sequence monad. For a variety of reasons, (mostly performance, I believe) David chose to not use an actual monad in his implementation and instead used protocols to great effect.

Combining these three components in the proper way you get an engine that searches a space shaped like a tree.

(For more information about the following, read “The Reasoned Schemer”)

This tree is built up using a few simple functions. The most basic operation is == named ‘unify’. This establishes that two things can be substituted for each other. The result of an == expression is called a goal.

The macro fresh allows for the introduction of logic variables and composes a series of goals into a single goal.

(def g (fresh [q x z]
          (== q false)
          (== x 10)
          (== "howdy" z)))

The function all has the effect of composing a series of goals into a single goal without creating logic variables.

(def g (all

Now, when you unify two things, you establish a relationship between then. A collection of these relationships is called a ‘substitution’. A goal actually is a function that takes a substitution as a parameter and adds one or more relationships to it.

So you have a goal, what do you do with it? Well, if you call it with an empty substitution, you’ll get back a substitution that contains relationships. Then you can query that substitution to see what value a particular logic variable might have. This is called reification and is done with the run* macro.

(run* [q]
      (== q 6))
=> [6]

You’ll notice that run* actually returned a list instead of just a single number. And that’s where some of the magic comes in. There’s another function, conde that lets you specify multiple relationships for a single logic variable.

(run* [q]
       [(== q 6)]
       [(== 8 q)]))
=> [6 8]

conde lets you specify alternatives, so that goals may return one or more substitutions. Each one could have different relationships for the same logic variables.

However, you can’t add a relationship to a substitution that violates a relationship already in there. If you try, that goal fails and produces no results.

So a goal is a function that takes a substitution and returns a list that may contain 0, 1 or many substitutions. Does that remind you of anything?

Hints of the future

If you were going to build a goal by hand, the easiest way would be to use Clojure’s ‘for’ statement.

(defn g [s]
   (for [s1 (goal1 s)
         s2 (goal2 s1)
         s3 (goal3 s2)]

This could be stated more succinctly as:

(require '[monads :as m])
(def g (m/chain [goal1 goal2 goal3]))

Searching space

So, multiple goals can be composed sequentially to make a single goal, conde is used to introduce alternatives and goals can fail. When run* comes along and passes an empty substitution to a goal, the net effect is to traverse a tree where each node of the tree is created by a conde goal and the substitutions at the leaves hold the answers to your query. Where goals fail, branches of the tree are not followed any further. You can visualize it something like this.

The s’s represent answer substitutions and the x’s represent failures.

When using the sequence monad to implement miniKanren, the search traverses the tree in a linear fashion. Starting at the root and descending to a leaf, then passing that result back up before descending another branch and getting another leaf. All results from the leaves migrate towards the root with the lists being unpacked and repacked at each node.

Here’s the key insight about this whole process. Searching each branch of the tree is totally independent from searching all other branches.

That means you could do your searching in parallel. The problem with that is how to get the answers from all the leaves to one place. Another problem is how to know when you’ve reached a leaf.

For the first, you could use the bane of functional programmers everywhere; shared mutable state and side effects. If there were a single place where you could stick the substitution whenever you hit the leaf, you’d be in business. Clojure’s atom datatype fits the bill nicely.

The second problem is actually open to a very elegant solution. What if you used a monad other than the sequence monad? The continuation monad is exactly what you want. With m/cont, a goal is a function that takes a substitution as a parameter. But instead of returning a list of substitutions, it returns a function that accepts a continuation function. When this function is called with a continuation, it calls the continuation with the new substitutions. A continuation is simply a goal that moves the search closer to the leaves. When a leaf is reached, the continuation is just a function that adds the substitution to the atom where the answers are being collected.

(def answers atom [])
(defn leaf [s]
    (swap! answers conj s))


So how do you implement such a beast? Starting with the vanilla core.logic code, the first step is to rewrite the miniKanren core using the vector monad.

(def logic-m vector)

(defn run-logic [goal]
   (goal empty-s))

(defn == [u v]
  (fn [a]
    (if-let [ap (unify a u v)]
      (succeed ap)
      (fail nil))))

(defn conde [& clauses]
  (fn [s]
    (m/plus (map #((m/chain %) s) clauses))))

(defn all [& goals]
  (m/chain goals))

(defmacro fresh [[& lvars] & goals]
  `(let [~@(lvar-binds lvars)]
     (monads.core/chain (list ~@goals))))

(defmacro run* [[x] & goals]
  `(let [~x (lvar '~x)]
     (map #(-reify % ~x)
          (run-logic (all ~@goals)))))

That’s a whole lot of code, but the main take away is that everything is written in terms of the logic-m monad, which is a variant of the sequence monad. This also was the first pleasant surprise I got. In standard core.logic, conde and all are macros. Using m/chain, m/plus and m/zero, they could be written as functions. fresh and run* have to be macros because they do some lexical bindings of lvars to symbols.

Then delete everything else. :)


Once you’ve done that, it’s a relatively easy task to change to a different monad, m/cont being the first example. However, in the general case, m/cont doesn’t implement the interface for a zero monad (m/MonadZero). So we have to define a specialized m/cont that does.

(deftype logic-monad [v mv goal]
  (deref [mv]
    (mv identity))

  (invoke [_ c]
    (if-not goal
        (c v)
        (mv (fn [v] ((goal v) c)))))

  (do-result [_ v]
    (logic-monad. v nil nil))
  (bind [mv goal]
    (logic-monad. nil mv goal))

  (zero [_]
    (logic-monad. nil (fn [_] nil) true))
  (plus-step [mv mvs]
    (logic-monad. nil
                  (fn [c]
                      (doseq [f (cons mv mvs)]
                        (f c)))
                  #(logic-monad. % nil nil))))

(defn run-logic [mv]
  (let [xs (atom [])
        leaf #(swap! xs conj %)]
    ((mv empty-s) leaf)
    (deref xs)))

Behold the power of monads!! You only need to change the monad and run-logic. Everything else just works.

The secret to this code is the implementation of invoke and plus-step. It works like this. A monadic value in the logic monad looks like a function that takes a one parameter which is a continuation function that accepts a single parameter. This continuation can be thought of as the rest of the search from this point down to a leaf. By calling a continuation with a substitution, the search moves toward the leaf. However, a logic monadic value may also be a deferred m/bind call, indicated by mv and goal being non-nil. In that case, an anonymous continuation is created which will accept a substition and call the goal with it. This returns a logic monadic value which will accept the that is passed into invoke. This anonymous continuation is then passed as a parameter to the monadic value, causing the search to continue.

The plus-step implementation is a function the creates a special kind of deferred bind. It accepts a list of logic monadic values, then creates a special deferred bind. When this new monadic value is called with a continuation, each of the monadic values are called with that continuation. So each branch of the tree is taken, one after another.

One other key piece is the implementation of zero. This function literally does nothing. When given a continuation, it does not call. Thereby halting the search down that branch. If you look back at the source of the == operator, you’ll see that the zero monadic value is returned when a unification attempt fails.

Then run-logic just takes a logic monadic value, creates an atom xs and a function that closes over that atom which adds substitutions to it. This function is executed as the leaves of the search tree.

You can visualize the effect of this change on the search process like this.

Each leaf of the tree is visited in sequence. No substitutions are passed back up towards the root.


This implementation of the continuation monad searches the entire tree before returning a list of answers. By changing the monad slightly, you can get a lazy list of answers returned which walks through the search tree as needed. Here’s the code with no further comment.

(deftype logic-monad [s mv goal]
  (invoke [_ [c thunk]]
     goal (mv [(fn anon-c [[s t]]
                 ((goal s) [c t]))
     :else (c [s thunk])))

  (do-result [_ s]
    (logic-monad. s nil nil))
  (bind [mv goal]
    (logic-monad. nil mv goal))

  (zero [_]
    (logic-monad. nil (fn [_] nil) true))
  (plus-step [mv mvs]
    (logic-monad. nil (fn [[c thunk]]
                        ((reduce (fn [t mv]
                                   (fn []
                                     (mv [c t])))
                                 (cons mv mvs))))
                  (fn [s]
                    (logic-monad. s nil nil)))))

(defn unwind [[x thunk]]
    (and x thunk) (lazy-seq
                    (cons x (unwind (thunk))))
    x [x]
    thunk (unwind thunk)))

(defn run-logic [mv]
  (unwind ((mv empty-s) [identity nil])))

The thing to notice is that the only thing that changed were the implementations of invoke, plus-step and run-logic.


So now we can make it multithreaded. Given David Nolen’s forkjoin.clj found here, it’s a breeze.

(def tasks (atom []))
(def thread-pool (fj/fjpool))

(deftype logic-monad [v mv goal]
  (invoke [_ c]
    (if-not goal
        (c v)
        (mv (fn [v] ((goal v) c)))))

  (do-result [_ v]
    (logic-monad. v nil nil))
  (bind [mv goal]
    (logic-monad. nil mv goal))

  (zero [_]
    (logic-monad. nil (fn [_] nil) true))
  (plus-step [mv mvs]
    (logic-monad. nil
                  (fn [c]
                    (doseq [t (map #(fj/fork (fj/task (% c))) mvs)]
                      (swap! tasks conj t))
                    (mv c))
                  #(logic-monad. % nil nil))))

(defn run-logic [goal]
  (let [xs (atom [])
        leaf #(swap! xs conj %)
        task (fj/task ((goal empty-s) leaf))]
     (fj/invoke thread-pool task)

     ;; wait for all tasks to finish
     (loop [ts @tasks]
       (when (seq ts)
         (doseq [t ts]
           (fj/join t)
           (swap! tasks subvec 1))
         (recur @tasks)))

     (deref xs)))

You should notice that this monad is almost identical to the continuation monad above with differences only in plus-step and run-logic. plus-step spawns off a new task for the other branches of a conde before continuing with the current one. Each new task is added to the tasks global atom. run-logic creates an atom and a leaf function as before, but then spawns a task off to start the search. The original task waits for all the search tasks to finish before extracting the answers in xs.

Future work

The final version can be found on my fork of core.logic here on the “fork-join” branch. There are also branches for the continuation, sequence and lazy continuation monads.

There are several other monads that could be used in core.logic. The state and writer monads come to mind. There’s also another one that would add an interesting feature and I’ll try to tackle that one next week sometime. Also, this work only covers a subset of core.logic. It would be interesting attempt to extend it to fully parallelize core.logic. Maybe later.

Wrapping up

The things that really stuck out to me were the ability to write the core miniKanren functionality as functions, only resorting to macros where needed. Also, the ease of completely changing the behavior by just modifying a few lines of code. And what wasn’t apparent, was the fact the several times, code I banged out quickly just worked (or nearly so) the first time I ran it. So all in all, monads rock!

Jim Duey 02 October 2012
blog comments powered by Disqus