Exploring Logic Programming in Clojure’s core.logic – Overview & Understanding Palindromes

Ever since I saw William Byrd and Dan Friedman present on miniKanren at Clojure/conj a few years ago, I’ve been distantly interested in the topic of logic programming. Recently, my interest has intensified, so I picked up a copy of The Reasoned Schemer and have been working through it.

What is Logic Programming Anyway?

As any intro to miniKanren will tell you, there are only a few basic primitives to the language:

• fresh introduces logic variables
• == (unify) attempts to unify a logic variable with a value (or two logic vars with each other)
• conde expresses a logical disjunction (OR)

And, magically, the entire language is built on these primitives! Despite their apparent simplicity, I did not find it easy to gain a real understanding of them. It reminds me of learning to use higher-order functions as a means for abstraction.

Kicking the Tires

The interesting aspect of relational programming is that once you define a concept, you can “run” it forwards or backwards. If you think of it in mathematical terms, instead of defining how to compute f(x) to get y, you are describing the relationship between x and y. In logic programming, rather than returning a value from a function call, an extra logic var is passed into a function. The “output” is then unified with this extra logic var.

During a recent developer interview, we asked the candidate to write a simple function that would test whether the value provided to it was a palindrome. While the candidate wrote on the whiteboard, I wondered: If I wrote a relational program describing a palindrome, could I use the solution engine to generate palindromes for me?

The definition of a palindrome is actually very simple, and it was easy to translate to Clojure’s core.logic. It’s just a list that is equal to the reverse of itself.

(defn palindromo [v]
  (fresh [r]
    (== v r)
    (reverso v r)))

Translated to regular English, this means the goal palindromo succeeds if the reverse of v is equal to v. (Why are “palindrome” and “reverse” suffixed with a weird vowel? It’s simply a convention that miniKanren uses to differentiate regular functions from logic goals.)

Of course, core.logic doesn’t include a definition of reverso, so to see our concept of a palindrome in action, we must first define reverso. It turned out that this was not quite as straightforward. I figured out that I could define it recursively:

(defn reverso [l r]
  (conde
    [(== l ()) (== r ())]
    [(fresh [la ld ldr]
      (conso la ld l)
      (appendo ldr (list la) r)
      (reverso ld ldr))]))

To break that down, let’s start with these definitions:

• l: the list
• r: the list that is the reverse of l
• la: the first item in l. Think (car l)
• ld: the rest of the items in l. Think (cdr l)
• ldr: the reverse of ld. That is, the reverse of the rest of the items in l.

We use conde to define a logical OR. The goal succeeds if both l and r can be unified with empty lists (this serves as the base case for our recursion). Otherwise, we introduce a few more goals. (conso la ld l) defines the relationship that la is the first of and ld is the rest of l. We then use appendo to say that adding la to the end of ldr must give you r. Finally, we recurse to say that ldr is the reverse of ld.

If those three goals succeed, then reverso succeeds, and l and r are the reverse of each other.

I should point out that, under the hood, conso and appendo do their work by unifying the “output” var with a list containing logic vars. The unifier is doing the real work, and we could define reverso without conso or appendo. Finally, I’m also compelled to mention that, regardless of logic programming, this is not a very efficient way to reverse a linked list, as we end up building our reversed list by appending values to the end.

So, anyway, let’s run it.

user=> (run 10 [q]
         (palindromo q))
(()
 (_0)
 (_0 _0)
 (_0 _1 _0)
 (_0 _1 _1 _0)
 (_0 _1 _2 _1 _0)
 (_0 _1 _2 _2 _1 _0)
 (_0 _1 _2 _3 _2 _1 _0)
 (_0 _1 _2 _3 _3 _2 _1 _0)
 (_0 _1 _2 _3 _4 _3 _2 _1 _0))

We get back ten values that were found for q! The first–an empty list–is not very interesting. The second is a list of _0, which simply indicates a logic var whose value is unspecified and could be anything. It could even be a list containing more logic vars. The number after the underscore is simply used to differentiate it from other logic vars.

We can see that these are all indeed palindromes. And we can also check to see if a list we provide is really a palindrome:

user=> (run 1 [q]
         (palindromo '(1 2 8 3 7 3 8 2 1))
         (== q "hooray!"))
("hooray!")

user=> (run 1 [q]
         (palindromo '(1 1 2))
         (== q "hooray!"))
()

In the first example, palindromo succeeds (as we gave it a real palindrome), and we continue to unify q with "hooray!" Obviously, in the second example, we do not give a valid palindrome. Therefore, no solutions can be found.

Getting a Bit More Useful

Our definition of palindromo is quite concise and small, yet we’re able to leverage it to generate palindromes and verify that an input is actually a palindrome. I think this is why the Clojure community has been so interested in core.logic. It allows for a new level of expressiveness in code.

So, we can generate real palindromes, but they don’t actually mean anything outside of core.logic. Could I be more ambitious, and say, generate palindromes of integers whose sums equal a specific value?

For that, stay tuned for part two of this post, where we’ll take a look at some finite domain constraint logic programming.