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:
freshintroduces logic variables
==(unify) attempts to unify a logic variable with a value (or two logic vars with each other)
condeexpresses 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
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.)
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
ld: the rest of the items in
ldr: the reverse of
ld. That is, the reverse of the rest of the items in
conde to define a logical OR. The goal succeeds if both
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
If those three goals succeed, then
reverso succeeds, and
r are the reverse of each other.
I should point out that, under the hood,
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
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
"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.