microLogic

The purpose of a logic program is to take an expression with some unknowns in it and try to find values for those unknowns that make the expression true. Here's an example logic program in English with an unknown x:

Either x is the beginning of the list ["banana", "orange", "apple"],
or x is the number 1.

(The two values of x that make this expression true are 1 and banana)

These unknowns are called logic variables, or lvars for short. Since we're going to write our logic programs in Clojure, we need a way to represent them in that context.

(defrecord LVar [id])
(defn lvar [id] (LVar. id))
(defn lvar? [x] (instance? LVar x))

An lvar's id could be anything, but we use it like a serial number. The first lvar gets created with id 0, the next with id 1, and so on. There is some special syntax to help with that, which we'll see later on.

In the course of running a logic program, we'll be deciding on values for logic variables and testing those values against other parts of the program to see if it meets all the necessary criteria. The values are stored in a data structure called a substitution map (s-map for short).

A substitution map is just a regular clojure hash-map with lvars as its keys. Again consider this example:

Either x is the beginning of the list ["banana", "orange", "apple"],
or x is the number 1.

{ (lvar 0) "banana" } is one substitution map that will make this expression true (as long as x is lvar 0).

There is a twist to the substitution map: in addition to regular values, lvars can be used in the value position as well. (This is called a triangular substitution) Here is an example which implies a triangular substitution:

x is the beginning of the list [y, "orange", "apple"].
y is the string "banana".

One substitution map which makes this expression true is

{ (lvar 0) (lvar 1)
  (lvar 1) "banana" }

unify is the way we build up substitution maps. Given two terms u and v, and an existing substitution map s-map, unify produces a new substitution map with mappings that will make u and v equal.

A term is simply something you can pass to unify. This is indeed a circular definition. But really, you can pass anything you like as a term. It's just that some types of terms have specialized behavior. LVars do, for example. When we add support for sequences, they will as well. Anything not handled explicitly is still a valid term, but it's just treated as an opaque value.

Let's walk through some examples.

• First, if either u or v is an lvar, the unifying them with a value just like assigning a value to that lvar in the substitution map.

  > (unify (lvar 0) "banana" {})
  {(lvar 0) "banana"}
  
  > (unify "banana" (lvar 0) {})
  {(lvar 0) "banana"}
  

• But what if the lvar already has a value? Then there are two possibilities. Either the two values agree:

  > (unify (lvar 0) "banana"
           {(lvar 0) "banana"})
  {(lvar 0) "banana"}
  

  Or they do not, leading to a contradiction:

  > (unify (lvar 0) "banana"
           {(lvar 0) "mango"})
  nil
  

• When there's something unrelated in the substitution map, we'll just add to it:

  > (unify (lvar 0) "banana"
           {(lvar 9) "squirrels"})
  {(lvar 0) "banana"
   (lvar 9) "squirrels"}
  

• Finally, if we unify two variables that can't be resolved to a value in the substitution map (these variables are called fresh) we add a new entry.

  > (def new-s (unify (lvar 1) (lvar 2)
                      {(lvar 0) (lvar 1)}))
  {(lvar 0) (lvar 1)
   (lvar 1) (lvar 2)}
  
  > (walk (lvar 0) new-s)
  (lvar 2)
  
  > (walk (lvar 1) new-s)
  (lvar 2)
  

  You can see from the example that unification is transitive; if a unifies with b, and b unifies with c, then a unifies with c.

That's it for the basic cases. They seem pretty trivial, but our unifier has one more nice feature: extensibility. By extending the IUnifyTerms protocol, you can add specialized unification behavior for any other data type as well. For example, once we add support for sequences below you'll be able to do this:

> (unify [(lvar 0) 2 3] ["banana" 2 3] {})
{(lvar 0) "banana"}

Here's the implementation of unify:

(defn unify [u v s-map]
  (let [u (walk u s-map),    v (walk v s-map)
        u-is-lvar (lvar? u), v-is-lvar (lvar? v)]
    (cond
      ;; Terms that walk to equal values always unify, but add nothing
      ;; to the substitution map
      (= u v) s-map

      ;; Unifying an lvar term with some other value creates a new entry in
      ;; the substitution map
      u-is-lvar (add-substitution s-map u v)
      v-is-lvar (add-substitution s-map v u)

      ;; Unifying two terms that walk to non-lvar values is delegated
      ;; to the polymorphic unify-terms function, from IUnifyTerms.
      :default (unify-terms u v s-map))))

Here are the basic IUnifyTerms definitions for Object and nil. If we get dispatched to either of these definitions, we know that neither u nor or v walks to an lvar, that the values aren't equal, and we aren't doing some kind of extended unification that's defined elsewhere. Thus, they must not unify.

(extend-protocol IUnifyTerms
  Object (unify-terms [u v s-map] nil)
  nil    (unify-terms [u v s-map] nil))

As we've alluded to above, when you run a logic program you can get more than one result. MiniKanren's approach to this is really unique, and is one of the most interesting parts of the program.

I told you before that the output of a logic program is a set of substitutions. That was a small lie, which we will now refine into the actual implementation.

delay-goal will wrap the given goal in a new one which, when executed, simply returns a thunk that wraps the goal. Recall that goal functions return streams, and that a function is a valid kind of stream (an immature stream). The goal will finally be executed when the thunk is evaluated by realize-stream-head.

This is especially useful when defining recursive goals.

(defmacro delay-goal [goal]
  `(fn delayed-goal-outer [state#]
     (fn delayed-goal-inner [] (~goal state#))))

We also define extended versions of the ldisj and lconj functions. These handle multiple goal parameters, instead of just two. They also automatically wraps each goal with delay-goal, so you don't need to worry about adding delays yourself.

(This does have a performance cost, but speed is not the point of this implementation)

(defmacro ldisj+
  ([goal] `(delay-goal ~goal))
  ([goal & goals] `(ldisj (delay-goal ~goal) (ldisj+ ~@goals))))

(defmacro lconj+
  ([goal] `(delay-goal ~goal))
  ([goal & goals] `(lconj (delay-goal ~goal) (lconj+ ~@goals))))

In miniKanren, reification refers to extracting the desired values from the stream of states you get as a result of executing a goal.

When there are logic variables in the output which were not assigned a value, they are named _.0, _.1, and so on.

(defn reify-name [n]
  (symbol (str "_." n)))

reify-s-map creates a substitution map with reified values in it. It bases this on the supplied s-map parameter, but adds entries for each unknown that appears in the supplied term v, using values from reify-name.

(defn reify-s [v s-map]
  (reify-s* (walk v s-map) s-map))

(extend-protocol IReifySubstitution
  LVar
  (reify-s* [v s-map] (let [n (reify-name (count s-map))]
                        (add-substitution s-map v n)))

  Object
  (reify-s* [v s-map] s-map)

  nil
  (reify-s* [v s-map] s-map))

deep-walk is like walk, but instead of simply returning any non-lvar value, it will attempt to assign values to any lvars embedded in it. For example, (deep-walk a {a (1 2 c), c 3)} will give (1 2 3). (once we have the sequence extensions, which are defined below)

(defn deep-walk [v s-map]
  (deep-walk* (walk v s-map) s-map))

(extend-protocol IDeepWalk
  LVar   (deep-walk* [v s-map] v)
  Object (deep-walk* [v s-map] v)
  nil    (deep-walk* [v s-map] v))

Finally, we can define the actual reifier. Given a state, this will give you the reified value of the first lvar that was defined. If you're using the run macro defined below, this will be the first query variable.

(defn reify-state-first-var [{:keys [s-map]}]
  (let [v (deep-walk (lvar 0) s-map)]
    (deep-walk v (reify-s v {}))))

Define the regular miniKanren conde form, a disjunction of conjunctions (an 'or' of 'ands'). Supposing that a and b are lvars,

(conde
  [(=== a 1) (=== b 2)]
  [(=== a 7) (=== b 12)})

will produce two results: {a 1, b 2} and {a 7, b 12}. (If you've never used miniKanren or core.logic before: 'e' means 'either'. Yes, the naming is odd. But really, it's best to remember that it's an 'or of ands' and to get used to the name)

(defmacro conde
  [& clauses]
  `(ldisj+ ~@(map (fn [clause]
                    `(lconj+ ~@clause))
                  clauses)))

The fresh macro allocates some new logic variables and makes them available in its body. Really, it's a more convenient syntax for call-fresh. fresh lets you declare multiple logic variables at once, and it takes care of the function declaration mechanics for you.

(defmacro fresh
  [var-vec & clauses]
  (if (empty? var-vec)
    `(lconj+ ~@clauses)
    `(call-fresh (fn [~(first var-vec)]
                   (fresh [~@(rest var-vec)]
                     ~@clauses)))))

The body of fresh is a list of goals that is passed to lconj+, a logical 'and'. This goal:

(fresh [x y]
  (=== x 1)
  (=== y 2))

Will give one result, {x 1, y 2}.

We define a small utility to invoke a goal with an empty state, as you might do when running a logic program from the top:

(defn call-empty-state [goal]
  (goal empty-state))

Finally, the run* macro gives us a lazy sequence of readable (reified) values.

(defmacro run* [fresh-var-vec & goals]
  `(->> (fresh [~@fresh-var-vec] ~@goals)
     call-empty-state
     stream-to-seq
     (map reify-state-first-var)))

The first parameter is a vector of logic variables which will be allocated and made available in the body; the first of these is reified and returned as a lazy sequence. This is called the 'query variable', and is often named 'q' by convention.

> (run* [q]
    (conde
      [(=== q 1)]
      [(=== q 7)]))
(1 7)

If you only want a few values (for example, if you know there are an infinite number of results), (run n [q] <<goals>>) can do that. It's equivalent to running take on the output of run*.

(defmacro run [n fresh-var-vec & goals]
  `(take ~n (run* ~fresh-var-vec ~@goals)))

When we unify sequences, we'd like to be able to indicate that an lvar should be associated with the tail of a sequence. In the scheme implementation, this is easy: by placing an lvar in the tail position of a linked list node (the cdr position of a cons node), the unification happens naturally when walking down the list.

Since Clojure disallows putting non-list items in linked-list cells (so-called 'improper lists'), we have to find another way to do it. core.logic solves this problem by defining its own LCons data type which does allow improper lists. We take a different approach here.

Whenever you want an improper list in the context of a logic program, you can signify it with the 'dot' sigil. For example: [1 2 dot a]. This is meant to evoke the Scheme and Common LISP notation for improper lists: (1 2 . 3). This will typically be transparent to the user on the programming side, since such lists will be automatically constructed by the 'conso' goal below.

(deftype Dot [])
(def dot (Dot.))

There are times when the user may see an improper list as the result of a query. In this case, print the sigil as "."

(defmethod print-method Dot [l ^java.io.Writer w]
  (.write w "."))

The first extension point is the unifier; we need to define what it means to unify a sequence with something else.

The basic case is simple: if unifying a sequence with another sequence, then we should unify each element together. Recursively, this means unifying their first elements and then the rest of the sequence.

The unifier also needs to be aware of the dot-notation described above. If either u or v is a sequence beginning with a dot, the its second item must be an lvar which should be unified with the other variable. For example, if we start with (=== [1 2 3] [1 . a]), it will recurse down to (=== [2 3] [. a]). Detecting that, we can call (=== [2 3] a), which gives the desired result.

(extend-protocol IUnifyTerms
  clojure.lang.Sequential
  (unify-terms [u v s]
    (cond
      (= dot (first u)) (unify (second u) v s)
      (= dot (first v)) (unify u (second v) s)
      (seq v) (->> s
                (unify (first u) (first v))
                (unify (rest u) (rest v))))))

Next, we need to extend the reifier. When calling reify-s, we need to look for occurrences of logic variables inside of given parameter. This extends reify-s to make a recursive call on the first element of the sequence, then on the remaining elements.

(extend-protocol IReifySubstitution
  clojure.lang.Sequential
  (reify-s* [v s-map]
    (if (seq v)
      (reify-s (rest v) (reify-s (first v) s-map))
      s-map)))

Deep-walk needs to be extended as well. As above, we we handle sequences beginning with 'dot' as a special case, go recursing back with the second item of the sequence. For any other sequences, we effectively map the deep-walk function over the sequence.

(extend-protocol IDeepWalk
  clojure.lang.Sequential
  (deep-walk* [v s-map]
    (cond
      (and (= dot (first v))
           (sequential? (second v)))
      (deep-walk (second v) s-map)

      (seq v)
      (cons (deep-walk (first v) s-map)
            (deep-walk (rest v)  s-map))

      :default v)))

Now we can define some user-level goals for sequences. First, conso says that out is the sequence with the head first and the tail rest.

(defn conso [first rest out]
  (if (lvar? rest)
    (=== [first dot rest] out)
    (=== (cons first rest) out)))

firsto simply says that first is the head of out.

(defn firsto [first out]
  (fresh [rest]
    (conso first rest out)))

And resto, likewise, says that rest is the tail of out.

(defn resto [rest out]
  (fresh [first]
    (conso first rest out)))

emptyo is a way to say that s must be an empty sequence.

(defn emptyo [s]
  (=== '() s))

appendo says that out is the result of appending the sequence parameters seq1 and seq1.

(defn appendo [seq1 seq2 out]
  (conde
    [(emptyo seq1) (=== seq2 out)]
    [(fresh [first rest rec]
       (conso first rest seq1)
       (conso first rec out)
       (appendo rest seq2 rec))]))

You can do some interesting things with appendo. For example, this program will find all the ways you can append two lists to create [1 2 3 4 5]:

> (run* [q]
    (fresh [x y]
      (appendo x y [1 2 3 4 5])
      (=== q [x y])))

((() (1 2 3 4 5))
 ((1)  (2 3 4 5))
 ((1 2)  (3 4 5))
 ((1 2 3)  (4 5))
 ((1 2 3 4)  (5))
 ((1 2 3 4 5) ()))

• The microKanren paper: http://webyrd.net/scheme-2013/papers/HemannMuKanren2013.pdf
• The microKanren scheme implementation: https://github.com/jasonhemann/microKanren
• core.logic, Clojure's real miniKanren implementation: https://github.com/clojure/core.logic
• Will Byrd's dissertation on miniKanren: https://github.com/webyrd/dissertation-single-spaced/raw/master/thesis.pdf
• Chris Grand on the lazy stream monad, and mplus in particular: http://clj-me.cgrand.net/2012/01/30/the-reasoned-scheduler/
• The Reasoned Schemer: http://mitpress.mit.edu/books/reasoned-schemer

Polymorphic dispatch via protocols is used in place of cond with type checks, where possible.

Clojure-native data types are used where appropriate

• The substitution map is a clojure map instead of an alist
• There is an LVar defrecord, instead of using a vector of the lvar id.
• We have an explicit StreamNode data type, rather building on the built-in list type.
• Clojure doesn't allow improper lists; we emulate it with the 'dot' sigil.

Many names have changed to be compatible with clojure, and to be more approachable to those without knowledge of Scheme, monads or miniKanren.