<commit_before>#+title: microLogic
#+HTML_HEAD: <link rel="stylesheet" type="text/css" href="http://thomasf.github.io/solarized-css/solarized-light.min.css" />

* Introduction
This is a literate Clojure implementation of miniKanren, a logic
programming system.  It's meant to be an introduction to the inner
workings of miniKanren and and of core.logic.

For maximum enjoyment, the reader should be familiar with Clojure, and
in particular with protocols. In lieu of that, basic understanding of
lisp syntax and a read through something like
http://clojure-doc.org/articles/language/polymorphism.html should be
sufficient.

This code was derived substantially from microKanren; for more
information, see the bibliography at the end.

* Functional Core
** COMMENT Header
#+begin_src clojure :tangle "src/micro_logic/core.clj" :noweb yes :comments org
  (ns micro-logic.core
    (:require [micro-logic.protocols :refer :all]))
#+end_src

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

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

(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.

#+begin_src clojure :tangle "src/micro_logic/core.clj" :comments org
  (defrecord LVar [id])
  (defn lvar [id] (LVar. id))
  (defn lvar? [x] (instance? LVar x))
#+end_src

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.

** Substitutions and Walking
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 neccessary 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:

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

~{ (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:

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

One substitution map which makes this expression true is
#+begin_src clojure
  { (lvar 0) (lvar 1)
    (lvar 1) "banana" }
#+end_src

*** Adding entries
Although a substitution map is nothing but a regular clojure map, we
need some utility functions to deal with some subtleties of its behavior.
The first is for adding add new entries:

#+begin_src clojure :tangle "src/micro_logic/core.clj" :comments org
  (defn add-substitution [s-map lvar value]
    (when s-map
      (assoc s-map lvar value)))
#+end_src

If you try to add something to a ~nil~ substitution map, we just
return ~nil~. The ~nil~ substitution map is output when there are no
substitutions that can make an expression true. We'll see where
this is important when we start to build up substitution maps.

*** Looking up values
The other thing we do with a substitution map is to look up what value
is associated with an lvar. It's just a hash-map, so why don't we just
use the ~get~ function for this? Two reasons:

1. If there is an lvar on the right-hand side, we need to look up that
   value, following such references until we get to a non-lvar.

2. The operation we want is actually "give me the value of this
   object, given this substitution map". So if you call it with a
   value that's not an lvar, it should just give you that value back.

The function is called /walk/, since it follows lvar references on the
right-hand side.

#+begin_src clojure :tangle "src/micro_logic/core.clj" :comments org
  (extend-protocol IWalk
    LVar
    (walk [u s-map] (if-let [val (get s-map u)]
                      (recur val s-map)
                      u))
    Object
    (walk [u s-map] u)

    nil
    (walk [u s-map] nil))
#+end_src

Here are some example ~walk~ invocations:
#+begin_src clojure
  > (def s-map { (lvar 0) (lvar 1)
                 (lvar 1) "banana" })

  > (walk (lvar 0) s-map)
  "banana"

  > (walk (lvar 1) s-map)
  "banana"

  > (walk "mango" s-map)
  "mango"
#+end_src


You might notice that it is easy to construct a substitution map with
a loop in it: ~(walk a {a b, b a})~ will not terminate. Most implementations
would handle that with a check in ~add-substitution~, but we omit it here
for simplicity.

** Unification
~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 somthing 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.

  #+begin_src clojure
    > (unify (lvar 0) "banana" {})
    {(lvar 0) "banana"}

    > (unify "banana" (lvar 0) {})
    {(lvar 0) "banana"}
  #+end_src

- But what if the lvar already has a value? Then there are two
  possibilities. Either the two values agree:
  #+begin_src clojure
    > (unify (lvar 0) "banana"
             {(lvar 0) "banana"})
    {(lvar 0) "banana"}
  #+end_src

  Or they do not, leading to a contradiction:
  #+begin_src clojure
    > (unify (lvar 0) "banana"
             {(lvar 0) "mango"})
    nil
  #+end_src

- When there's something un-related in the substitution map,
  we'll just add to it:
  #+begin_src clojure
    > (unify (lvar 0) "banana"
             {(lvar 9) "squirrels"})
    {(lvar 0) "banana"
     (lvar 9) "squirrels"}
  #+end_src

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:

#+begin_src clojure
  > (unify [(lvar 0) 2 3] ["banana" 2 3] {})
  {(lvar 0) "banana"}
#+end_src

Here's the implementation of ~unify~:
#+begin_src clojure :tangle "src/micro_logic/core.clj" :comments org
  (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
        ;; Unifying two lvars adds no information to the substitution map
        (and u-is-lvar v-is-lvar (= u v)) s-map

        ;; Unifying an lvar 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)

        ;; two non-lvar values always unify if they're equal
        (= u v) s-map

        ;; Unifying two non-lvars is delegated to the polymorphic
        ;; unify-terms function, from IUnifyTerms.
        :default (unify-terms u v s-map))))
#+end_src

Here are the basic IUnifyTerms definitions for Object and nil.  If we
get dispatched to either of these definitions, we know that neither u
or v is 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.

#+begin_src clojure :tangle "src/micro_logic/core.clj" :comments org
(extend-protocol IUnifyTerms
  Object (unify-terms [u v s-map] nil)
  nil    (unify-terms [u v s-map] nil))
#+end_src

** Lazy Streams
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.

*** Motivation
First, I'll try to convince you that we need to make a special lazy
stream mechanism. We'll start with a more formal definition of what we
mean by a "logic program":

*THE DEFINITION OF A LOGIC PROGRAM*

1. In miniKanren, /the output of a logic program is a set of
   substitutions/ that make that program true.

2. A logic program is built by combining smaller logic programs using
   the conjunction (and) and disjunction (or) operators.

Now, let's consider this logic program in particular:
#+begin_src
  Define Natural(x) to be true when either:
    - x is the number 0
    - x is greater than 0, and Natural(x - 1) is true
#+end_src

Clearly there are an infinite number of substitution maps that make
this program true - ~{(lvar 0) 0}~, ~{(lvar 0) 1}~, ~{(lvar 0) 2}~,
and so on. That is, it has an inifinitely large set of solutions.

Here's another motivating example:
#+begin_src
  Define Diverge(x) to be true when Diverge(x) is true
#+end_src

As you can probably guess from the name, this is a program which has
no valid output. But it's a program you can write all the same, and it
will take forever to produce no output. The example is contrived, but
you can get into such a situation surprisingly (distressingly) easily
when writing actual progrems.

So we now know that:
1. There are logic programs with infinitely many solutions
2. There are logic programs which diverge

And, we want to compose such programs together in a sane way, to make
more complex programs. We need a way to fairly take results from
programs with infinitely many solutions, and to continue to service a
part of the program which might diverge while continuing to work on
its more productive brethren.

This is the motivation for lazy streams.

*** Definition of a lazy stream
There are three kinds of lazy streams:
- Empty
- Mature (head realized)
- Immature (head unrealized)

A mature stream is one in which the first element of the stream has a
definite value that has already been computed. An immature stream, on
the other hand, does not yet have a computed head. Instead if has a
function which it can used to compute a mature (or empty) stream when
you need it.

You can manipulate a stream with these functions:
- Merge two of them together with ~merge-streams~
- Map a function over it with ~mapcat-stream~, as long as that
  function itself produces streams.
- Realize its head with ~realize-stream-head~. This will transition it
  to either immature or empty, performing any necessary work along the
  way.
- Convert it to a Clojure lazy sequence, with ~stream-to-seq~

*** Empty stream
#+begin_src clojure :tangle "src/micro_logic/core.clj" :comments org
  (def empty-stream
    (reify IStream
      (merge-streams [this other-stream] other-stream)
      (mapcat-stream [this g] this)
      (realize-stream-head [this] this)
      (stream-to-seq [this] '())))
#+end_src

*** Mature streams (StreamNode)
A mature streams is represented by an instance of StreamNode.  This is
kind of like a linked list: /head/ is the realized value that can be
taken from the stream, and /next/ is the stream which follows.  But
these streams are polymorphic; /next/ isn't necessarily a StreamNode,
just some other thing which extends the IStream protocol.

Note that if we have only StreamNodes (i.e. fully realized streams),
~merge-streams~ is equivalent to ~concat~ and ~mapcat-stream~ to
~mapcat~.

#+begin_src clojure :tangle "src/micro_logic/core.clj" :comments org
  (deftype StreamNode [head next]
    IStream
    (merge-streams [this other-stream] (StreamNode. head
                                                    (merge-streams next other-stream)))
    (mapcat-stream [this g] (merge-streams (g head)
                                           (mapcat-stream next g)))
    (realize-stream-head [this] this)

    (stream-to-seq [this] (lazy-seq (cons head (stream-to-seq next)))))

  (defn make-stream [s] (StreamNode. s empty-stream))
#+end_src

*** Immature streams (IFn)
An immature stream is represented by a thunk (a function of no
arguments).

Executing the thunk does one unit of work and returns a new
stream. This may in turn be a function, so you might have to keep
calling the returned function many times until you get down to a
realized value. This is exactly what ~realize-stream-head~ does here,
by way of ~trampoline~.

**** Merging
Merging is tricky - this is the code that interleaves values from two
infinite streams, and what makes sure a branch that diverges doesn't
tie up the whole program.
#+begin_src clojure
  clojure.lang.IFn
  (merge-streams [this other-stream]
    #(merge-streams other-stream (this)))
#+end_src

Working from the inside out: we know that 'this' is a function because
we're extending IStream onto IFn; calling it will perform one 'unit of
work', whatever that might be. It returns a stream.  Then we merge
that stream with other-stream, the second parameter of this merge
operation, /but the order is reversed/.

Finally, the above operation is all wrapped in a thunk. So we end up with a
function that:

- performs the work for the first thing you constructed it with
- returns a new stream, putting the second thing you constructed it
  with at the head.

An imaginary repl session may make this clearer:
#+begin_src clojure
    > (def a #(make-stream (+ 1 1)))
    > (def b #(stream (+ 10 20))
    > (def s (merge-streams a b))
    #(merge-streams #(make-stream (+ 10 20) (#(make-stream (+ 1 1))))

    > (def s' (s))
    #(merge-streams (StreamNode. 2 nil) (#(make-stream (+ 10 20))))

    > (def s'' (s'))
    (StreamNode. 2 (StreamNode. 30))
#+end_src

**** Mapping
~mapcat-stream~ is somewhat simpler.

#+begin_src clojure
  clojure.lang.IFn
  (mapcat-stream [this g]
    #(mapcat-stream (this) g))
#+end_src

The basic concept here is pretty straightforward: make a new thunk
which, when executed later, will do some work and then mapcat ~g~ over
the result.  The thunk is used instead of just exeuting the function
directly because ~mapcat-stream~ may be used inside a recusive
function, which might diverge. This won't keep the function from
diverging, but it will allow its execution to be interleaved with the
rest of the program.

**** Definition
Here is the whole definition of IStream for functions:

#+begin_src clojure :tangle "src/micro_logic/core.clj" :comments org
  (extend-protocol IStream
    clojure.lang.IFn
    (merge-streams [this other-stream]
      #(merge-streams other-stream (this)))

    (mapcat-stream [this g]
      #(mapcat-stream (this) g))

    (realize-stream-head [this]
      (trampoline this))

    (stream-to-seq [this]
      (stream-to-seq (realize-stream-head this))))
#+end_src

*** Differences from Clojure's lazy sequences
This is very similar to Clojure's lazy sequence facility; why not just
use that? Well, there are cases where you are combining the results of
two logic programs (with merge-streams), but one of them might
diverge. (Remember the example above?) The lazy stream system shown
here handles that case by giving each stream equal processing time,
evaluating its thunks as they come. In this sense, lazy streams are a
scheduling system for processes which may return multiple outputs.

** Goals
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.

*** Interpreter state
A /state/ is a record containing a substitution map *s-map* and the id
of the next unused logic variable, /next-id/.
#+begin_src clojure :tangle "src/micro_logic/core.clj" :comments org
  (defrecord State [s-map next-id])

  (defn make-state [s-map next-id] (State. s-map next-id))
  (def empty-state (make-state {} 0))
  (defn with-s-map [state s-map] (assoc state :s-map s-map))
  (defn with-next-id [state next-id] (assoc state :next-id next-id))
#+end_src

*** Goal functions
A goal is a function which, given a state, returns a stream of
states. It encapsulates a logic program. Give it an input state, and
it will give you one output state for each way it can make that goal
true (or /succeed/ in the parlance of miniKanren and The Reasoned
Schemer), given the information in the input state.

*** Basic goal constructors
Rather than dealing with goals directly, we usually use
/goal constructors/; given some parameter (usually a unification term or
another goal), they will return a goal function which closes over
it.

The most fundamental goal constructor is for unification.  Given two
terms /u/ and /v/, this creates a goal that will unify them. The goal
takes an existing state and returns (as a lazy stream) either a state
with bindings for the lvars in /u/ and /v/ (using ~unify~), or nothing
at all if /u/ and /v/ cannot be unified.

#+begin_src clojure :tangle "src/micro_logic/core.clj" :comments org
  (defn === [u v]
    (fn unify-goal [{:keys [s-map] :as state}]
      (if-let [s-map' (unify u v s-map)]
        (make-stream (with-s-map state s-map'))
        empty-stream)))
#+end_src

/call-fresh/ is a higher-order goal constructor that encapsulates the
allocation of logic variables. You pass it your own
/goal-constructor/, which takes as its single parameter the lvar that
you want to use.  /call-fresh/ will make a new goal that allocates it
for you, passing it in to your code.  /goal-constructor/. For a more
convenient way to do this, see the /fresh/ macro below.

#+begin_src clojure :tangle "src/micro_logic/core.clj" :comments org
  (defn call-fresh [goal-constructor]
    (fn fresh-goal [{:keys [s-map next-id] :as state}]
      (let [goal (goal-constructor (lvar next-id))]
       (goal (with-next-id state (inc next-id))))))
#+end_src

One way to combine smaller goals into a new one is with logical
disjuction, the 'or' operation. ~ldisj~ which constructs a new goal
that succeeds whenever /goal-1/ or /goal-2/ succeeds.  Another way to
look at this is that it interleaves the results of /goal-1/ and
/goal-2/, using ~merge-streams~.

#+begin_src clojure :tangle "src/micro_logic/core.clj" :comments org
  (defn ldisj [goal-1 goal-2]
    (fn disj-goal [state]
      (merge-streams (goal-1 state) (goal-2 state))))
#+end_src

You can also combine goals with logical conjunction, the 'and'
operation. ~lconj~ constructs a new goal that succeeds when both
/goal-1/ and /goal-2/ succeed. It does this by running goal-2 on each
output of goal-1. You can think of this as being like function
composition for functions with multiple outputs.

#+begin_src clojure :tangle "src/micro_logic/core.clj" :comments org
(defn lconj [goal-1 goal-2]
  (fn conj-goal [state]
    (mapcat-stream (goal-1 state) goal-2)))
#+end_src

* Sugar
At this point, we have everything we need to do logic programming!
But it's very inconvenient. Here we define some syntax to make the
task more bearable.

** Auxilliary macros
/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.

#+begin_src clojure :tangle "src/micro_logic/core.clj" :comments org
  (defmacro delay-goal [goal]
    `(fn delayed-goal-outer [state#]
       (fn delayed-goal-inner [] (~goal state#))))
#+end_src

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)

#+begin_src clojure :tangle "src/micro_logic/core.clj" :comments org
  (defmacro ldisj+
    ([goal] `(delay-goal ~goal))
    ([goal & goals] `(ldisj (delay-goal ~goal) (ldisj+ ~@goals))))
#+end_src

#+begin_src clojure :tangle "src/micro_logic/core.clj" :comments org
  (defmacro lconj+
    ([goal] `(delay-goal ~goal))
    ([goal & goals] `(lconj (delay-goal ~goal) (lconj+ ~@goals))))
#+end_src

** Reificiation
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.

#+begin_src clojure :tangle "src/micro_logic/core.clj" :comments org
  (defn reify-name [n]
    (symbol (str "_." n)))
#+end_src

/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/.
#+begin_src clojure :tangle "src/micro_logic/core.clj" :comments org
  (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))
#+end_src

/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)
#+begin_src clojure :tangle "src/micro_logic/core.clj" :comments org
  (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))
#+end_src

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.
#+begin_src clojure :tangle "src/micro_logic/core.clj" :comments org
  (defn reify-state-first-var [{:keys [s-map]}]
    (let [v (deep-walk (lvar 0) s-map)]
      (deep-walk v (reify-s v {}))))
#+end_src

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

#+begin_src clojure
  (conde
    [(=== a 1) (=== b 2)]
    [(=== a 7) (=== b 12)})
#+end_src

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)

#+begin_src clojure :tangle "src/micro_logic/core.clj" :comments org
  (defmacro conde
    [& clauses]
    `(ldisj+ ~@(map (fn [clause]
                      `(lconj+ ~@clause))
                    clauses)))
#+end_src

The ~fresh~ macro allocates some new logic variables and makes them
available in its boday. 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.

#+begin_src clojure :tangle "src/micro_logic/core.clj" :comments org
  (defmacro fresh
    [var-vec & clauses]
    (if (empty? var-vec)
      `(lconj+ ~@clauses)
      `(call-fresh (fn [~(first var-vec)]
                     (fresh [~@(rest var-vec)]
                       ~@clauses)))))
#+end_src

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

#+begin_src clojure
  (fresh [x y]
    (=== x 1)
    (=== y 2))
#+end_src

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:
#+begin_src clojure :tangle "src/micro_logic/core.clj" :comments org
  (defn call-empty-state [goal]
    (goal empty-state))
#+end_src

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

#+begin_src clojure :tangle "src/micro_logic/core.clj" :comments org
  (defmacro run* [fresh-var-vec & goals]
    `(->> (fresh [~@fresh-var-vec] ~@goals)
       call-empty-state
       stream-to-seq
       (map reify-state-first-var)))
#+end_src

The first parameter is a vector of logic varialbes which will be
alocated 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.

#+begin_src clojure
  > (run* [q]
      (conde
        [(=== q 1)]
        [(=== q 7)]))
  (1 7)
#+end_src

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*.

#+begin_src clojure :tangle "src/micro_logic/core.clj" :comments org
  (defmacro run [n fresh-var-vec & goals]
    `(take ~n (run* ~fresh-var-vec ~@goals)))
#+end_src

* Sequences
The base logic programming system has unification and reification
support for only lvars and basic values. But it's done in an
extensible way. We'll now proceed to add sequence support to the base
language.

** COMMENT Header
#+begin_src clojure :tangle "src/micro_logic/sequence.clj" :comments org
  (ns micro-logic.sequence
    (:require [micro-logic.core :refer :all]
              [micro-logic.protocols :refer :all]))
#+end_src

** Extending the core
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.

Whenver 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.

#+begin_src clojure :tangle "src/micro_logic/sequence.clj" :comments org
  (deftype Dot [])
  (def dot (Dot.))
#+end_src

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

#+begin_src clojure :tangle "src/micro_logic/sequence.clj" :comments org
  (defmethod print-method Dot [l ^java.io.Writer w]
    (.write w "."))
#+end_src

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.

#+begin_src clojure :tangle "src/micro_logic/sequence.clj" :comments org
  (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))))))
#+end_src

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

#+begin_src clojure :tangle "src/micro_logic/sequence.clj" :comments org
  (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)))
#+end_src

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.

#+begin_src clojure :tangle "src/micro_logic/sequence.clj" :comments org
  (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)))
#+end_src

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

#+begin_src clojure :tangle "src/micro_logic/sequence.clj" :comments org
  (defn conso [first rest out]
    (if (lvar? rest)
      (=== [first dot rest] out)
      (=== (cons first rest) out)))
#+end_src

/firsto/ simply says that /first/ is the head of /out/.

#+begin_src clojure :tangle "src/micro_logic/sequence.clj" :comments org
  (defn firsto [first out]
    (fresh [rest]
      (conso first rest out)))
#+end_src

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

#+begin_src clojure :tangle "src/micro_logic/sequence.clj" :comments org
  (defn resto [rest out]
    (fresh [first]
      (conso first rest out)))
#+end_src

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

#+begin_src clojure :tangle "src/micro_logic/sequence.clj" :comments org
  (defn emptyo [s]
    (=== '() s))
#+end_src

/appendo/ says that /out/ is the result of appending the sequence parameters
/seq1/ and /seq1/.
#+begin_src clojure :tangle "src/micro_logic/sequence.clj" :comments org
  (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))]))
#+end_src

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]~:

#+begin_src clojure
  > (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) ()))
#+end_src

* Back matter
** Bibliography
- 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
- <NAME>'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

** Differences from microKanren
Polymorphic dispatch via protocols is used in place of `(cond)` with
type checks, where possible.

Clojure-native datatypes are used where appropriate
- The substitution map is a clojure map instead of an alist
- There is an LVar defrecrord, instead of using a vector of c
- 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 more clojure-like:

|uKanren | microLogic          |
|--------|---------------------|
|mplus   | merge-streams       |
|bind    | mapcat-stream       |
|pull    | realize-stream-head |
|mzero   | empty-stream        |
|unit    | stream              |
|Zzz     | delay-goal          |
|conj    | lconj               |
|disj    | ldisj               |
|==      | =====               |

** Differences from core.logic

|core.logic | microLogic           |
|-----------|----------------------|
|mplus      | merge-streams        |
|bind       | mapcat-stream        |
|pull       | realize-stream-head  |
|mzero      | empty-stream         |
|unit       | stream               |
|==         | =====                |<commit_msg>Better docs<commit_after>#+title: microLogic
#+HTML_HEAD: <link rel="stylesheet" type="text/css" href="http://thomasf.github.io/solarized-css/solarized-light.min.css" />

* Introduction
This is a literate Clojure implementation of miniKanren, a logic
programming system which can be embedded in functional programming
languages.  It's meant to be an introduction to the inner workings of
miniKanren and and of core.logic, helping you to understand more
completely what's happening when you use those systems.

For maximum enjoyment, the reader should be familiar with Clojure, and
in particular with protocols. In lieu of that, basic understanding of
lisp syntax and a read through something like
http://clojure-doc.org/articles/language/polymorphism.html should be
sufficient.

This code was derived substantially from microKanren; for much more
information, see the bibliography at the end.

* Functional Core
** COMMENT Header
#+begin_src clojure :tangle "src/micro_logic/core.clj" :noweb yes :comments org
  (ns micro-logic.core
    (:require [micro-logic.protocols :refer :all]))
#+end_src

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

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

(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.

#+begin_src clojure :tangle "src/micro_logic/core.clj" :comments org
  (defrecord LVar [id])
  (defn lvar [id] (LVar. id))
  (defn lvar? [x] (instance? LVar x))
#+end_src

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.

** Substitutions and Walking
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 neccessary 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:

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

~{ (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:

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

One substitution map which makes this expression true is
#+begin_src clojure
  { (lvar 0) (lvar 1)
    (lvar 1) "banana" }
#+end_src

*** Adding entries
Although a substitution map is nothing but a regular clojure map, we
need some utility functions to deal with some subtleties of its behavior.
The first is for adding add new entries:

#+begin_src clojure :tangle "src/micro_logic/core.clj" :comments org
  (defn add-substitution [s-map lvar value]
    (when s-map
      (assoc s-map lvar value)))
#+end_src

If you try to add something to a ~nil~ substitution map, we just
return ~nil~. The ~nil~ substitution map is output when there are no
substitutions that can make an expression true. We'll see where
this is important when we start to build up substitution maps.

*** Looking up values
The other thing we do with a substitution map is to look up what value
is associated with an lvar. It's just a hash-map, so why don't we just
use the ~get~ function for this? Two reasons:

1. If there is an lvar on the right-hand side, we need to look up that
   value, following such references until we get to a non-lvar.

2. The operation we want is actually "give me the value of this
   object, given this substitution map". So if you call it with a
   value that's not an lvar, it should just give you that value back.

The function is called /walk/, since it follows lvar references on the
right-hand side.

#+begin_src clojure :tangle "src/micro_logic/core.clj" :comments org
  (extend-protocol IWalk
    LVar
    (walk [u s-map] (if-let [val (get s-map u)]
                      (recur val s-map)
                      u))
    Object
    (walk [u s-map] u)

    nil
    (walk [u s-map] nil))
#+end_src

Here are some example ~walk~ invocations:
#+begin_src clojure
  > (def s-map { (lvar 0) (lvar 1)
                 (lvar 1) "banana" })

  > (walk (lvar 0) s-map)
  "banana"

  > (walk (lvar 1) s-map)
  "banana"

  > (walk "mango" s-map)
  "mango"
#+end_src


You might notice that it is easy to construct a substitution map with
a loop in it: ~(walk a {a b, b a})~ will not terminate. Most implementations
would handle that with a check in ~add-substitution~, but we omit it here
for simplicity.

** Unification
~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 somthing 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.

  #+begin_src clojure
    > (unify (lvar 0) "banana" {})
    {(lvar 0) "banana"}

    > (unify "banana" (lvar 0) {})
    {(lvar 0) "banana"}
  #+end_src

- But what if the lvar already has a value? Then there are two
  possibilities. Either the two values agree:
  #+begin_src clojure
    > (unify (lvar 0) "banana"
             {(lvar 0) "banana"})
    {(lvar 0) "banana"}
  #+end_src

  Or they do not, leading to a contradiction:
  #+begin_src clojure
    > (unify (lvar 0) "banana"
             {(lvar 0) "mango"})
    nil
  #+end_src

- When there's something un-related in the substitution map,
  we'll just add to it:
  #+begin_src clojure
    > (unify (lvar 0) "banana"
             {(lvar 9) "squirrels"})
    {(lvar 0) "banana"
     (lvar 9) "squirrels"}
  #+end_src

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:

#+begin_src clojure
  > (unify [(lvar 0) 2 3] ["banana" 2 3] {})
  {(lvar 0) "banana"}
#+end_src

Here's the implementation of ~unify~:
#+begin_src clojure :tangle "src/micro_logic/core.clj" :comments org
  (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
        ;; Unifying two lvars adds no information to the substitution map
        (and u-is-lvar v-is-lvar (= u v)) s-map

        ;; Unifying an lvar 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)

        ;; two non-lvar values always unify if they're equal
        (= u v) s-map

        ;; Unifying two non-lvars is delegated to the polymorphic
        ;; unify-terms function, from IUnifyTerms.
        :default (unify-terms u v s-map))))
#+end_src

Here are the basic IUnifyTerms definitions for Object and nil.  If we
get dispatched to either of these definitions, we know that neither u
or v is 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.

#+begin_src clojure :tangle "src/micro_logic/core.clj" :comments org
(extend-protocol IUnifyTerms
  Object (unify-terms [u v s-map] nil)
  nil    (unify-terms [u v s-map] nil))
#+end_src

** Lazy Streams
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.

*** Motivation
First, I'll try to convince you that we need to make a special lazy
stream mechanism. We'll start with a more formal definition of what we
mean by a "logic program":

*THE DEFINITION OF A LOGIC PROGRAM*

1. In miniKanren, /the output of a logic program is a set of
   substitutions/ that make that program true.

2. A logic program is built by combining smaller logic programs using
   the conjunction (and) and disjunction (or) operators.

Now, let's consider this logic program in particular:
#+begin_src
  Define Natural(x) to be true when either:
    - x is the number 0
    - x is greater than 0, and Natural(x - 1) is true
#+end_src

Clearly there are an infinite number of substitution maps that make
this program true - ~{(lvar 0) 0}~, ~{(lvar 0) 1}~, ~{(lvar 0) 2}~,
and so on. That is, it has an inifinitely large set of solutions.

Here's another motivating example:
#+begin_src
  Define Diverge(x) to be true when Diverge(x) is true
#+end_src

As you can probably guess from the name, this is a program which has
no valid output. But it's a program you can write all the same, and it
will take forever to produce no output. The example is contrived, but
you can get into such a situation surprisingly (distressingly) easily
when writing actual progrems.

So we now know that:
1. There are logic programs with infinitely many solutions
2. There are logic programs which diverge

And, we want to compose such programs together in a sane way, to make
more complex programs. We need a way to fairly take results from
programs with infinitely many solutions, and to continue to service a
part of the program which might diverge while continuing to work on
its more productive brethren.

This is the motivation for lazy streams.

*** Definition of a lazy stream
There are three kinds of lazy streams:
- Empty
- Mature (head realized)
- Immature (head unrealized)

A mature stream is one in which the first element of the stream has a
definite value that has already been computed. An immature stream, on
the other hand, does not yet have a computed head. Instead if has a
function which it can used to compute a mature (or empty) stream when
you need it.

You can manipulate a stream with these functions:
- Merge two of them together with ~merge-streams~
- Map a function over it with ~mapcat-stream~, as long as that
  function itself produces streams.
- Realize its head with ~realize-stream-head~. This will transition it
  to either immature or empty, performing any necessary work along the
  way.
- Convert it to a Clojure lazy sequence, with ~stream-to-seq~

*** Empty stream
#+begin_src clojure :tangle "src/micro_logic/core.clj" :comments org
  (def empty-stream
    (reify IStream
      (merge-streams [this other-stream] other-stream)
      (mapcat-stream [this g] this)
      (realize-stream-head [this] this)
      (stream-to-seq [this] '())))
#+end_src

*** Mature streams (StreamNode)
A mature streams is represented by an instance of StreamNode.  This is
kind of like a linked list: /head/ is the realized value that can be
taken from the stream, and /next/ is the stream which follows.  But
these streams are polymorphic; /next/ isn't necessarily a StreamNode,
just some other thing which extends the IStream protocol.

Note that if we have only StreamNodes (i.e. fully realized streams),
~merge-streams~ is equivalent to ~concat~ and ~mapcat-stream~ to
~mapcat~.

#+begin_src clojure :tangle "src/micro_logic/core.clj" :comments org
  (deftype StreamNode [head next]
    IStream
    (merge-streams [this other-stream] (StreamNode. head
                                                    (merge-streams next other-stream)))
    (mapcat-stream [this g] (merge-streams (g head)
                                           (mapcat-stream next g)))
    (realize-stream-head [this] this)

    (stream-to-seq [this] (lazy-seq (cons head (stream-to-seq next)))))

  (defn make-stream [s] (StreamNode. s empty-stream))
#+end_src

*** Immature streams (IFn)
An immature stream is represented by a thunk (a function of no
arguments).

Executing the thunk does one unit of work and returns a new
stream. This may in turn be a function, so you might have to keep
calling the returned function many times until you get down to a
realized value. This is exactly what ~realize-stream-head~ does here,
by way of ~trampoline~.

**** Merging
Merging is tricky - this is the code that interleaves values from two
infinite streams, and what makes sure a branch that diverges doesn't
tie up the whole program.
#+begin_src clojure
  clojure.lang.IFn
  (merge-streams [this other-stream]
    #(merge-streams other-stream (this)))
#+end_src

Working from the inside out: we know that 'this' is a function because
we're extending IStream onto IFn; calling it will perform one 'unit of
work', whatever that might be. It returns a stream.  Then we merge
that stream with other-stream, the second parameter of this merge
operation, /but the order is reversed/.

Finally, the above operation is all wrapped in a thunk. So we end up with a
function that:

- performs the work for the first thing you constructed it with
- returns a new stream, putting the second thing you constructed it
  with at the head.

An imaginary repl session may make this clearer:
#+begin_src clojure
    > (def a #(make-stream (+ 1 1)))
    > (def b #(stream (+ 10 20))
    > (def s (merge-streams a b))
    #(merge-streams #(make-stream (+ 10 20) (#(make-stream (+ 1 1))))

    > (def s' (s))
    #(merge-streams (StreamNode. 2 nil) (#(make-stream (+ 10 20))))

    > (def s'' (s'))
    (StreamNode. 2 (StreamNode. 30))
#+end_src

**** Mapping
~mapcat-stream~ is somewhat simpler.

#+begin_src clojure
  clojure.lang.IFn
  (mapcat-stream [this g]
    #(mapcat-stream (this) g))
#+end_src

The basic concept here is pretty straightforward: make a new thunk
which, when executed later, will do some work and then mapcat ~g~ over
the result.  The thunk is used instead of just exeuting the function
directly because ~mapcat-stream~ may be used inside a recusive
function, which might diverge. This won't keep the function from
diverging, but it will allow its execution to be interleaved with the
rest of the program.

**** Definition
Here is the whole definition of IStream for functions:

#+begin_src clojure :tangle "src/micro_logic/core.clj" :comments org
  (extend-protocol IStream
    clojure.lang.IFn
    (merge-streams [this other-stream]
      #(merge-streams other-stream (this)))

    (mapcat-stream [this g]
      #(mapcat-stream (this) g))

    (realize-stream-head [this]
      (trampoline this))

    (stream-to-seq [this]
      (stream-to-seq (realize-stream-head this))))
#+end_src

*** Differences from Clojure's lazy sequences
This is very similar to Clojure's lazy sequence facility; why not just
use that? Well, there are cases where you are combining the results of
two logic programs (with merge-streams), but one of them might
diverge. (Remember the example above?) The lazy stream system shown
here handles that case by giving each stream equal processing time,
evaluating its thunks as they come. In this sense, lazy streams are a
scheduling system for processes which may return multiple outputs.

** Goals
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.

*** Interpreter state
A /state/ is a record containing a substitution map *s-map* and the id
of the next unused logic variable, /next-id/.
#+begin_src clojure :tangle "src/micro_logic/core.clj" :comments org
  (defrecord State [s-map next-id])

  (defn make-state [s-map next-id] (State. s-map next-id))
  (def empty-state (make-state {} 0))
  (defn with-s-map [state s-map] (assoc state :s-map s-map))
  (defn with-next-id [state next-id] (assoc state :next-id next-id))
#+end_src

*** Goal functions
A goal is a function which, given a state, returns a stream of
states. It encapsulates a logic program. Give it an input state, and
it will give you one output state for each way it can make that goal
true (or /succeed/ in the parlance of miniKanren and The Reasoned
Schemer), given the information in the input state.

*** Basic goal constructors
Rather than dealing with goals directly, we usually use
/goal constructors/; given some parameter (usually a unification term or
another goal), they will return a goal function which closes over
it.

The most fundamental goal constructor is for unification.  Given two
terms /u/ and /v/, this creates a goal that will unify them. The goal
takes an existing state and returns (as a lazy stream) either a state
with bindings for the lvars in /u/ and /v/ (using ~unify~), or nothing
at all if /u/ and /v/ cannot be unified.

#+begin_src clojure :tangle "src/micro_logic/core.clj" :comments org
  (defn === [u v]
    (fn unify-goal [{:keys [s-map] :as state}]
      (if-let [s-map' (unify u v s-map)]
        (make-stream (with-s-map state s-map'))
        empty-stream)))
#+end_src

/call-fresh/ is a higher-order goal constructor that encapsulates the
allocation of logic variables. You pass it your own
/goal-constructor/, which takes as its single parameter the lvar that
you want to use.  /call-fresh/ will make a new goal that allocates it
for you, passing it in to your code.  /goal-constructor/. For a more
convenient way to do this, see the /fresh/ macro below.

#+begin_src clojure :tangle "src/micro_logic/core.clj" :comments org
  (defn call-fresh [goal-constructor]
    (fn fresh-goal [{:keys [s-map next-id] :as state}]
      (let [goal (goal-constructor (lvar next-id))]
       (goal (with-next-id state (inc next-id))))))
#+end_src

One way to combine smaller goals into a new one is with logical
disjuction, the 'or' operation. ~ldisj~ which constructs a new goal
that succeeds whenever /goal-1/ or /goal-2/ succeeds.  Another way to
look at this is that it interleaves the results of /goal-1/ and
/goal-2/, using ~merge-streams~.

#+begin_src clojure :tangle "src/micro_logic/core.clj" :comments org
  (defn ldisj [goal-1 goal-2]
    (fn disj-goal [state]
      (merge-streams (goal-1 state) (goal-2 state))))
#+end_src

You can also combine goals with logical conjunction, the 'and'
operation. ~lconj~ constructs a new goal that succeeds when both
/goal-1/ and /goal-2/ succeed. It does this by running goal-2 on each
output of goal-1. You can think of this as being like function
composition for functions with multiple outputs.

#+begin_src clojure :tangle "src/micro_logic/core.clj" :comments org
(defn lconj [goal-1 goal-2]
  (fn conj-goal [state]
    (mapcat-stream (goal-1 state) goal-2)))
#+end_src

* Sugar
At this point, we have everything we need to do logic programming!
But it's very inconvenient. Here we define some syntax to make the
task more bearable.

** Auxilliary macros
/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.

#+begin_src clojure :tangle "src/micro_logic/core.clj" :comments org
  (defmacro delay-goal [goal]
    `(fn delayed-goal-outer [state#]
       (fn delayed-goal-inner [] (~goal state#))))
#+end_src

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)

#+begin_src clojure :tangle "src/micro_logic/core.clj" :comments org
  (defmacro ldisj+
    ([goal] `(delay-goal ~goal))
    ([goal & goals] `(ldisj (delay-goal ~goal) (ldisj+ ~@goals))))
#+end_src

#+begin_src clojure :tangle "src/micro_logic/core.clj" :comments org
  (defmacro lconj+
    ([goal] `(delay-goal ~goal))
    ([goal & goals] `(lconj (delay-goal ~goal) (lconj+ ~@goals))))
#+end_src

** Reificiation
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.

#+begin_src clojure :tangle "src/micro_logic/core.clj" :comments org
  (defn reify-name [n]
    (symbol (str "_." n)))
#+end_src

/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/.
#+begin_src clojure :tangle "src/micro_logic/core.clj" :comments org
  (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))
#+end_src

/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)
#+begin_src clojure :tangle "src/micro_logic/core.clj" :comments org
  (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))
#+end_src

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.
#+begin_src clojure :tangle "src/micro_logic/core.clj" :comments org
  (defn reify-state-first-var [{:keys [s-map]}]
    (let [v (deep-walk (lvar 0) s-map)]
      (deep-walk v (reify-s v {}))))
#+end_src

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

#+begin_src clojure
  (conde
    [(=== a 1) (=== b 2)]
    [(=== a 7) (=== b 12)})
#+end_src

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)

#+begin_src clojure :tangle "src/micro_logic/core.clj" :comments org
  (defmacro conde
    [& clauses]
    `(ldisj+ ~@(map (fn [clause]
                      `(lconj+ ~@clause))
                    clauses)))
#+end_src

The ~fresh~ macro allocates some new logic variables and makes them
available in its boday. 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.

#+begin_src clojure :tangle "src/micro_logic/core.clj" :comments org
  (defmacro fresh
    [var-vec & clauses]
    (if (empty? var-vec)
      `(lconj+ ~@clauses)
      `(call-fresh (fn [~(first var-vec)]
                     (fresh [~@(rest var-vec)]
                       ~@clauses)))))
#+end_src

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

#+begin_src clojure
  (fresh [x y]
    (=== x 1)
    (=== y 2))
#+end_src

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:
#+begin_src clojure :tangle "src/micro_logic/core.clj" :comments org
  (defn call-empty-state [goal]
    (goal empty-state))
#+end_src

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

#+begin_src clojure :tangle "src/micro_logic/core.clj" :comments org
  (defmacro run* [fresh-var-vec & goals]
    `(->> (fresh [~@fresh-var-vec] ~@goals)
       call-empty-state
       stream-to-seq
       (map reify-state-first-var)))
#+end_src

The first parameter is a vector of logic varialbes which will be
alocated 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.

#+begin_src clojure
  > (run* [q]
      (conde
        [(=== q 1)]
        [(=== q 7)]))
  (1 7)
#+end_src

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*.

#+begin_src clojure :tangle "src/micro_logic/core.clj" :comments org
  (defmacro run [n fresh-var-vec & goals]
    `(take ~n (run* ~fresh-var-vec ~@goals)))
#+end_src

* Sequences
The base logic programming system has unification and reification
support for only lvars and basic values. But it's done in an
extensible way. We'll now proceed to add sequence support to the base
language.

** COMMENT Header
#+begin_src clojure :tangle "src/micro_logic/sequence.clj" :comments org
  (ns micro-logic.sequence
    (:require [micro-logic.core :refer :all]
              [micro-logic.protocols :refer :all]))
#+end_src

** Extending the core
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.

Whenver 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.

#+begin_src clojure :tangle "src/micro_logic/sequence.clj" :comments org
  (deftype Dot [])
  (def dot (Dot.))
#+end_src

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

#+begin_src clojure :tangle "src/micro_logic/sequence.clj" :comments org
  (defmethod print-method Dot [l ^java.io.Writer w]
    (.write w "."))
#+end_src

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.

#+begin_src clojure :tangle "src/micro_logic/sequence.clj" :comments org
  (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))))))
#+end_src

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

#+begin_src clojure :tangle "src/micro_logic/sequence.clj" :comments org
  (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)))
#+end_src

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.

#+begin_src clojure :tangle "src/micro_logic/sequence.clj" :comments org
  (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)))
#+end_src

** Sequence goals
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/.

#+begin_src clojure :tangle "src/micro_logic/sequence.clj" :comments org
  (defn conso [first rest out]
    (if (lvar? rest)
      (=== [first dot rest] out)
      (=== (cons first rest) out)))
#+end_src

/firsto/ simply says that /first/ is the head of /out/.

#+begin_src clojure :tangle "src/micro_logic/sequence.clj" :comments org
  (defn firsto [first out]
    (fresh [rest]
      (conso first rest out)))
#+end_src

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

#+begin_src clojure :tangle "src/micro_logic/sequence.clj" :comments org
  (defn resto [rest out]
    (fresh [first]
      (conso first rest out)))
#+end_src

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

#+begin_src clojure :tangle "src/micro_logic/sequence.clj" :comments org
  (defn emptyo [s]
    (=== '() s))
#+end_src

/appendo/ says that /out/ is the result of appending the sequence parameters
/seq1/ and /seq1/.
#+begin_src clojure :tangle "src/micro_logic/sequence.clj" :comments org
  (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))]))
#+end_src

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]~:

#+begin_src clojure
  > (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) ()))
#+end_src

* Back matter
** Bibliography
- 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
- <NAME>'s dissertation on miniKanren: https://github.com/webyrd/dissertation-single-spaced/raw/master/thesis.pdf
- <NAME> 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

** Differences from microKanren
Polymorphic dispatch via protocols is used in place of ~cond~ with
type checks, where possible.

Clojure-native datatypes 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.

|uKanren | microLogic          |
|--------|---------------------|
|c       | id                  |
|mplus   | merge-streams       |
|bind    | mapcat-stream       |
|pull    | realize-stream-head |
|mzero   | empty-stream        |
|unit    | stream              |
|Zzz     | delay-goal          |
|conj    | lconj               |
|disj    | ldisj               |
|==      | =====               |

** Differences from core.logic

| core.logic | microLogic          |
|------------+---------------------|
| mplus      | merge-streams       |
| bind       | mapcat-stream       |
| pull       | realize-stream-head |
| mzero      | empty-stream        |
| unit       | stream              |
| ==         | =====               |
{'fraction_non_alphanumeric': 0.09817969696516446, 'fraction_numerical': 0.00568377282857442, 'mean_word_length': 3.34283858395583, 'pattern_counts': {'":': 2, '<': 12, '<?xml version=': 0, '>': 54, 'https://': 6, 'lorem ipsum': 0, 'www.': 0, 'xml': 0}, 'pii_count': 0, 'substrings_counts': 0, 'word_list_counts': {'cursed_substrings.json': 9, 'profanity_word_list.json': 0, 'sexual_word_list.json': 0, 'zh_pornsignals.json': 0}}
{'dir': 'git-commits-cleaned', 'id': '447567', 'n_tokens_mistral': 22192, 'n_tokens_neox': 20864, 'n_words': 9431}