Reazon is an Emacs implementation of the miniKanren logic programming language. As of version 0.1 it contains just a basic equality relation and no constraints. In particular, it lacks a disequality constraint; while it is possible to say that the value of variable x is 5, it is not possible to say that the value of variable x is not5.
With a little cleverness and some dull labor, it is sometimes possible to circumvent this limitation by expressing a negative in terms of positives. Consider the following logic puzzle1:
Baker, Cooper, Fletcher, Miller, and Smith live on different floors of an apartment house that contains only five floors. Baker does not live on the top floor. Cooper does not live on the bottom floor. Fletcher does not live on either the top or the bottom floor. Miller lives on a higher floor than does Cooper. Smith does not live on a floor adjacent to Fletcher’s. Fletcher does not live on a floor adjacent to Cooper’s. Where does everyone live?
We’re given that the building has exactly five floors, and our goal is to figure out the ordering of the residents in the building. We know immediately that there can only be finitely many solutions, so we can safely use reazon-run* to find all of them. Using q as our query variable, we can start to sketch out a solution. We’ll represent the building as a list with five items, the first of which represents the bottom floor and the last of which represents the top floor.
The next clue is stated as a negative: “Baker does not live on the top floor.” We can’t express negatives, so how can we proceed? Let’s think about it without doing any programming. Where does Baker live? She2 isn’t on the top (fifth) floor, so she must be on the first floor or the second floor or the third floor or the fourth floor. Well, there’s our positive statement right there!
This repetitive list of alternatives is inelegant, and it’s not even correct, as it doesn’t preclude the possibility of Baker’s being on the fifth floor, but for now it’s the best we can do. Note that this clause implies that q is a list of five elements, so we can actually delete our first clause.
The next two clues can be handled similarly.
The next clue is different: “Miller lives on a higher floor than does Cooper.” The general way to handle such a clue would be to write a relation like (precedes x y s), meaning x precedes y in s. Our problem domain is small, though, so we’ll just stick to primitives. This clue adds some new possibilities (if Cooper is on the second floor, Miller could be on floor three, four, or five), but it also removes some (we know Cooper can’t be on the top floor).
The final two clues both mention Fletcher, so we will handle them in the Fletcher disjunction: “Smith does not live on a floor adjacent to Fletcher’s. Fletcher does not live on a floor adjacent to Cooper’s.” Adjancency is a symmetric relation, so we can say that neither Smith nor Cooper live on a floor adjacent to Fletcher. Thus if Fletcher lives on the second floor, neither Smith nor Cooper can live on the the first or third floors, and therefore must live on the fourth and fifth floors. These and the other cases are easy enough to add in:
Putting the pieces together, our solver yields results:
((smith cooper baker fletcher miller))
In fact, it yields exactly one solution. If we trust the language (???), then we can conclude that there are no others.
Suppose we omit the requirement that Smith and Fletcher do not live on adjacent floors. How many solutions are there then?3
((baker cooper miller fletcher smith) (baker cooper smith fletcher miller) (baker fletcher smith cooper miller) (smith cooper baker fletcher miller) (smith fletcher baker cooper miller))
Now, you might say: we basically solved the problem ourselves by explicitly typing out the possibilities, so what’s the point of using miniKanren at all?
First, this was not meant to be an example of good miniKanren programming technique, but rather a demonstration that a certain class of problem is in principle within the grasp of Reazon 0.1. Second, even with just the cases laid out in the final form of the solver, it would still be a pain to have to settle the problem manually, so miniKanren really did help us in the end.
Finally, let’s take a step back and look at the outline of our solver. In general, a query of the form
will attempt to find values for q satisfying all of goal-1 … goal-n. This is equivalent to querying against the single goal that is the conjunction of all those goals.
In our solver, all the goals are disjunctions, so this looks like