Object Commando languages, development and design

4Nov/116

The Magical Island of Kanren – core.logic Intro Part 1

Overview

Previously I blogged on Appendo the Great without going into much detail on core.logic, what it is, how to use it etc. Hopefully this blog post will begin to fix that. This post was also inspired by a tweet from Ambrose Bonnaire-Sergeant on explaining a basic logic program with an unbound variable. That tweet got me thinking about how I would explain it.

First, core.logic is a Clojure implementation of miniKanren. miniKanren is a Logic Programming library embedded in Scheme. As the site states, it's mini in that there is another Kanren system with more bells and whistles, but is quite a bit more complex. The core.logic implementation follows the Scheme version pretty closely from a library user's perspective, so examples in books/papers such as Byrd's dissertation or The Reasoned Schemer translate pretty closely to the equivalent Clojure code.

The approach taken by the miniKanren folks gives the developer a lot of power by letting them pick the right tool for the job. Embedding the logic programming paradigm into a functional language allows you to use functional tools to solve your problems and delve into logic when it makes things easier. There's no need to interface with another language, you're in Clojure and you can use it directly.

Environment

Getting core.logic incorporated into your project works the same as any other Java or Clojure library, just include it in your project dependencies. Including it in your Leiningen project.clj would look like:

  :dependencies [...
                  [org.clojure/core.logic "0.6.5"]
                  ...]

Then lein deps and you're set. The examples below assume having a namespace setup like:

(ns logic-examples.ancenstors
  (:refer-clojure :exclude [==])
  (:use [clojure.core.logic]))

The Island of Kanren

Imagine the magical island of Kanren. On this island, just declaring things makes them so. There can be multiple right answers to a question and sometimes there are no answers at all. Here, seemingly familiar operations take on a different meaning and the natives speak with a unique dialect. Your code lives in functions and macros, just like any Clojure program. The key difference is your Kanren programs are really more like puzzles that you want the Kanren-ites to solve. Your logic functions on their own aren't much good, but the Kanren natives can do amazing things with them to solve your puzzle. The only way to get answers off of the island is to send your puzzle over with a raft [ ]. Unfortunately, there are some small holes in the raft and we need to put a bucket on it before we send the raft over. I'll call this bucket q, but you can call it whatever you like. Armed with our raft and bucket we can send it over with a puzzle and the Kanren natives will solve the program and send the bucket back. This bucket will contain the things (bindings) that the natives needed to solve the program. The easiest, yet still confusing program, just declares something that is always true:

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

It may seem strange at first, but the natives of Kanren have sent back a bucket with a single value _.0 in it. In the language of Kanren, this means anything and nothing. It means to solve the puzzle I sent them (which just declares that 1 is 1) q can take on any value. The number 7, a list of strings, nil etc. This makes sense as the Kanren natives can solve the puzzle with anything since the q does not actually play a role in solving the puzzle. We could make it a little more difficult and send over another raft asking for a 1

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

Here we sent over a puzzle that could only be solved with q having the value of 1. There is no other way for the Kanren-ites to solve the puzzle (and still have it work), so they sent back a value of 1 for q. The reason I relate q to a bucket in a raft, is that's our only way of getting information off of the island. All other information stays on the island:

(run* [q]
  (fresh [x y]
    (== x "foo")
    (== y "bar")
    (== q 1)))
= > (1)

The fresh call here is just a way to get a new variable (er, new buckets). This new variable is just like q, but it always stays on the island. Note our answer is the same as before because nothing has changed with the bucket vs. the program before. It's possible that q has more than one value (examples will be below) and it's also possible for q to be a collection:

(run* [q]
  (fresh [x y]
    (== x "foo")
    (== y "bar")
    (== q [1 x y])))
= > ([1 "foo" "bar"])

The above gets the information from x and y by stuffing it in q. So q is where we want the answer to be stored since that is what comes back on the raft. If we don't put the answer in the q bucket, we won't get anything useful. It's also possible that q has no answer. We could play a trick on the Kanren-ites and send them an unsolvable puzzle:

(run* [q]
  (== q 1)
  (== q 2))
= > ()

They saw through my ruse. It's not possible to solve a puzzle where q is both 1 and 2, so they send back an empty bucket.

Less Metaphor more Examples

Above, I covered the mechanics of running a core.logic program, er, puzzle. A logic program follows some different rules, so they need to be ran inside the run* block. The above examples only used run* which asks for all possible solutions to the program. Another key point from the above program is that I never assigned a value to q. I declared that q should equal 1. The Kanren-ites needed to take it from there. Instead I could have declared it equal to anything, a string, list, character etc. To cover some of the core.logic building blocks, I'll side-step integers and lists for the time being. To demonstrate some of these basic features, I'll be using some of the relation and fact features of core.logic. First I'll start with a father and mother relation:

(defrel father Father Child)
(defrel mother Mother Child)

(facts father [['Vito 'Michael]
               ['Vito 'Sonny]
               ['Vito 'Fredo]
               ['Michael 'Anthony]
               ['Michael 'Mary]
               ['Sonny 'Vicent]
               ['Sonny 'Francesca]
               ['Sonny 'Kathryn]
               ['Sonny 'Frank]
               ['Sonny 'Santino]])

(facts mother [['Carmela 'Michael]
               ['Carmela 'Sonny]
               ['Carmela 'Fredo]
               ['Kay 'Mary]
               ['Kay 'Anthony]
               ['Sandra 'Francesca]
               ['Sandra 'Kathryn]
               ['Sandra 'Frank]
               ['Sandra 'Santino]])

From this basic setup we can ask some basic questions:

(run* [q]
  (father 'Vito q))
= > (Sonny Michael Fredo)

(run* [q]
  (father q 'Michael))
= > (Vito)

These questions use the father relation. Given Vito is the father, what values of q would satisfy the father relation? We could do the same thing for the reverse. Given a child, who's the father? Note in the first example that there are three valid solutions to the relation, and any of them are correct. If I only asked for one solution:


(run 1 [q]
  (father 'Vito q))
= > (Sonny)

I would just get Sonny.

Conde

To ask better questions, we'll need conde. First lets define as a function, what the definition of parent is:

  (defn parent [p child]
    (conde
      ((father p child))
      ((mother p child))))

(run* [q]
  (parent q 'Michael))
= > (Vito Carmela)

The function parent above uses something new. It's one of the core building blocks of core.logic, called conde. I think of conde as a very fancy or. If you think of an or statement in a functional or imperative languages, it finds the first true value, then stops. On the Island of Kanren, there can be many correct answers to a puzzle, and again the Kanren-ites are trying to solve the puzzle every way possible. So in the above, there are two possibilities when using parent according to the defined relation. It tries the father relation first. If that passes, it will count as one answer. It will then come back through, act as if the first condition failed and will run the second statement. In this case, the first and second line are mutually exclusive, so it's pretty similar to a straight or.

(run* [q]
  (fresh [x y z]
    (conde
      ((== x "1st"))
      ((== y "2nd"))
      ((== z "3rd")))
    (== q [x y z])))
= > (["1st" _.0 _.1] [_.0 "2nd" _.1] [_.0 _.1 "3rd"])

The above illustrates this trying of the various clauses. Each of the above three clauses will always pass if executed. The three answers returned are all separate, so the first answer only has a value for x. The y and z are still fresh (and could be any value). The same is true for the second and third answer.

More Relations

These functions can also stack on each other:

(defn grandparent [gparent child]
  (fresh [p]
    (parent gparent p)
    (parent p child)))

(run* [q]
  (grandparent q 'Anthony))
= > (Vito Carmela)

(run* [q]
  (grandparent 'Vito q))
= > (Francesca Frank Vicent Mary Kathryn Santino Anthony)

The definition of grandparent is that the grandparent gparent is the parent of some new person p and that person p is the parent of child. The Kanren-ites can also solve more complex puzzles where the grandparent and child is unknown but the parent is known:

(run* [q]
  (fresh [gparent p child]
    (== p 'Michael)
    (parent p child)
    (grandparent gparent child)
    (== q {:grandparent gparent :parent p :child child})))

= > ({:grandparent Vito, :parent Michael, :child Mary}
     {:grandparent Vito, :parent Michael, :child Anthony}
     {:grandparent Carmela, :parent Michael, :child Mary}
     {:grandparent Carmela, :parent Michael, :child Anthony})

There are a few things interesting about the above example. First no child or grandparent was specified. In this puzzle, we specified the parent (in this case Michael) but nothing else. The Kanren-ites had to use this constrant in trying to find the grandparent(s) and children. The second interesting piece of the above is the usage of the map as the value of q. Since there are several answers and several pieces of information for each answer, I stuffed the results in a map. For the puzzle to be solved, the appropriate values needed to be plugged into the map.

What Next?

There's a lot more to cover in core.logic. Specifically, I was pretty light on the magic and "special-ness" of relation functions, variables etc. I'll cover that in my next post along with doing useful things with lists and matching.

Since the library is fairly new, there's not a ton of resources on it yet. For more information on core.logic specifically, Ambrose's Logic Starter has good information and there's some in the core.logic README. Byrd's dissertation and The Reasoned Schemer are very good. They are written in Scheme, but they translate to Clojure easily.

Comments (6) Trackbacks (0)
  1. Great explanations, perfect level of complexity for beginning logic programming in general (not just for core.logic). And for once, in my opinion, the metaphorical examples were actually helpful.

  2. Thank you, maybe a little graphviz picture of the family structure for a better understanding?
    http://imageshack.us/photo/my-images/836/familyah.png/

  3. I’ve just started learning Clojure, and after slogging through Mark Volkmann’s tutorial (which, although very complete and helpful, does read more like a dictionary than a document), finding your blog was refreshing.

  4. Thanks a lot. Can’t wait for a follow-up!

  5. Noticed a small error as I was working through your examples, the facts “father” and “mother” are missing closing “]” before the last parentheses.

    Thank you for the walk-through.

  6. Thanks! I have made the update.


Leave a comment

(required)

No trackbacks yet.