The adventures continue with Core.Logic!

Since the last post I’ve had some more time to dig into the implementation of Core.Logic. I’ve also been spending more time with Ivan Bratko’s excellent Prolog Programming For Artificial Intelligence. Finally, since Core.Logic is an implementation of miniKanren, I’ve discovered that William Byrd’s miniKanren Dissertation is a very helpful resource for understanding Core.Logic.

Chapter 2 of Prolog Programming For Artificial Intelligence introduces a classic AI problem involving a monkey and a banana.

A monkey is in a room that contains a banana and a box. The banana is in the middle of the room and is out of the monkey’s reach if the monkey is standing on the floor. But, if the monkey positions the box properly and stands on it then the monkey will be able to reach the banana. The monkey is allowed to walk around the room, push the box, climb the box, and reach for the banana. They question is, given a particular starting room configuration, can the monkey reach the banana?

The state of monkey-world can be expressed as a 4-tuple. The terms that make it up are:

1. Where the monkey is in the room
2. If the monkey is on the box
3. Where the box is in the room
4. If the monkey has the banana

In Prolog, we express this using a named structure with 4 parameters. For example:

1

state( middle, onbox, middle, hasnot )

In this configuration, the monkey is in the middle of the room and is standing on the box (also in the middle of the room) and it does not have the banana.

In Core.Logic, we don’t really have a concept that maps directly to Prolog’s named structures but we do have full access to Clojure’s rich data-types. A simple array will do what we need. We could tag the array with a name but that information isn’t needed for this example. We’ll just express the state of the world as an unnamed 4-vector of symbols:

1

[ :middle :onbox :middle :hasnot ]

The monkey can interact with the world by:

1. Grabbing the banana
2. Climbing the box
3. Pushing the box
4. Walking around the room

Not all actions are always possible. The available actions depend on the state of the world and applying an action to a world-state produces a new world-state.

In Prolog, we can encode the “grabbing the banana” action as a relation between the initial world-state, the action, and the resulting world-state:

1
2
3
4

move(
 state( middle, onbox, middle, hasnot ),
 grasp,
 state( middle, onbox, middle, has )).

In English: If the monkey is in the middle of the room and on the box (also in the middle of the room) and it doesn’t have the banana and it uses the grasp action then it will have the banana.

Now, let’s teach the monkey to climb:

1
2
3
4

move(
 state( P, onfloor, P, H),
 climb,
 state( P, onbox, P, H )).

This relation introduces the idea of unbound positions in a relation. In Prolog, if a slot in a relation is filled in with a symbol that begins with capital letter then that slot is unbound. Prolog can often apply rules to figure out what the unbound slots in a relationship should be bound to. If the same capitalized symbol fills multiple slots in a relation then those slots should be bound to the same value once Prolog discovers what the value is.

Now box pushing:

1
2
3
4

move(
 state( P1, onfloor, P1, H),
 push( P1, P2 ),
 state( P2, onfloor P2, H )).

The monkey can push the box from one position to another if the monkey and the box are in the same place. Once the monkey is done pushing then the monkey and the box will be in the new place.

Now walking:

1
2
3
4

move(
 state( P1, onfloor, B, H),
 walk( P1, P2 ),
 state( P2, onfloor, B, H )).

This is like box pushing but only the monkey’s position changes in the new world-state.

That’s quite enough Prolog for the moment. It’s time to introduce a new Core.Logic macro: The Mighty “defne” (which I like to pronounce “Daphne”.)

A defne Interlude

defne combines conde style rules with some powerful sugar that saves us from having to explicitly introduce some of our variables with fresh. It’s difficult to grasp until you’ve used it so let’s try getting there through a few examples.

In the my previous post I defined a relation called parent and added facts to that relation. Here’s that again but with defne:

1
2
3
4
5
6
7

(defne parent [elder child]
  ([:pam :bob])
  ([:tom :bob])
  ([:tom :liz])
  ([:bob :ann])
  ([:bob :pat])
  ([:pat :jim]))

The macro-expansion sheds some light on what’s going on here:

1
2
3
4
5
6
7
8
9
10
11
12
13
14

(macroexpand '(defne parent ....))

;; approximately expands to

(defn parent [elder child]
  (conde
    ((== :pam elder)
     (== :bob child))

    ((== :tom elder)
     (== :bob child))

    ;; and so on...
    ))

We’re defining a new function of two variables. This new function uses conde to provide a series of possible relations. Remember, conde is somewhat like a logical OR. Within each option, defne has bound (actually, unified) each slot of the vector with the corresponding slot in the arguments to the function.

defne isn’t very exciting when you put only constants in the binding slots. Let’s introduce some variables also:

1
2
3
4

(defne appendo [x y z]
  ([ () _ y ])
  ([ [ a . d ] _ [ a . r] ]
   (appendo d y r)))

This is quite a leap forward in complexity. Let’s take it apart by looking at the macro-expansion:

1
2
3
4
5
6
7
8
9

(defn appendo [x y z]
  (conde
    ((== () x)
     (== y z))

    ((fresh [a d r]
       (== (llist a d) x)
       (== (llist a r) z)
       (appendo d y r)))))

This has expanded to a conde with two cases. The first case applies when X is the empty list. This case also unifies its result variable Z with Y. In English, the result of appending the empty list X onto Y is the same as just Y.

The next case has introduced some new variables using fresh. These correspond to the variables we used in the first part of the second case. Here we’re unpacking X into its head A and its tail D. We’re also packing something new into our result variable Z and we’re recursively calling ourselves. In English, the result of appending the non-empty list X onto Y is the result of appending the tail of X onto Y and then sticking the head of X in front of that.

appendo is tricky. The big idea to grasp for this post is that defne pattern matches against its input variables and is useful for unpacking things like lists and doing interesting things with their contents.

Solution to Monkey and Banana

Using defne we can encode our monkey movement rules in even less space than Prolog required:

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16

(defne moveo [state move new-state]
  ([[:middle :onbox :middle :hasnot]
    :grasp
    [:middle :onbox :middle :has]])

  ([[p :onfloor p h]
    :climb
    [p :onbox p h]])

  ([[p1 :onfloor p1 h]
    [:push p1 p2]
    [p2 :onfloor p2 h]])

  ([[p1 :onfloor b h]
    [:walk p1 p2]
    [p2 :onfloor b h]]))

We can test our move engine by asking for all the moves possible when the monkey and the box are in the middle of the room:

1
2
3
4
5
6
7
8
9

(run* [q]
  (fresh [m s2]
    (moveo [:middle :onfloor :middle :hasnot] m s2)
    (conso m [s2] q)))

;; result
((:climb [:middle :onbox :middle :hasnot])
 ([:push :middle _.0] [_.0 :onfloor _.0 :hasnot])
 ([:walk :middle _.0] [_.0 :onfloor :middle :hasnot]))

Core.Logic answers that the monkey can climb, push the box from the middle to somewhere, or walk from the middle to somewhere. Grasping the banana isn’t possible from this position.

Now that we’ve encoded how moves affect the world-state we just need to find out if there is a sequence of moves that will let the monkey reach its goal. Can the monkey get the banana?

In Prolog:

1
2
3
4
5

canget( state( _, _, _, has ) ).

canget( State1 ) :-
 move( State1, Move, State2 ),
 canget( State2 ).

Or, the monkey can get the banana if it already has the banana or if it makes a move and then can get the banana.

In Core.Logic:

1
2
3
4
5
6

(defne cangeto [state out]
  ([[_ _ _ :has] true])
  ([_ _] (fresh
          [move state2]
          (moveo state move state2)
          (cangeto state2 out))))

Now, finally, we can ask if our monkey can get to its banana:

1
2
3
4

(run 1 [q] (cangeto [:atdoor :onfloor :atwindow :hasnot] q))

;; result
(true)

A happy ending.

Postlude

Ivan Bratko makes the point that the Prolog version of this program is sensitive to the order of its rules. If you re-arrange the final two expressions in canget then the resulting program will never find a solution:

1
2
3

canget( State1 ) :-
 canget( State2 ),
 move( State1, Move, State2 ).

This is because Prolog does a depth-first search of its solution space. The Prolog version of this program gets stuck recursing into the next call to canget before it ever constrains State2 by applying a new Move.

Happily, Core.Logic isn’t sensitive in this way and will execute its similarly altered program to the correct conclusion:

1
2
3
4
5
6
7
8
9
10
11

(defne cangeto [state out]
  ([[_ _ _ :has] true])
  ([_ _] (fresh
          [move state2]
          (cangeto state2 out)))
          (moveo state move state2))

(run 1 [q] (cangeto [:atdoor :onfloor :atwindow :hasnot] q))

;; result
(true)

Credit:

I got stuck in my first attempt to port the monkey and the banana. Happily, David Nolen had already written an example solution to this problem and I was able to study his example. He has implemented other interesting examples as benchmarks for Core.Logic.