Who Owns the Fish?
… that is the question. To find the answer will use a logic programming DSL embedded in Racket, named miniKanren.
By the way, if you are in a hurry: the German owns the Fish. Twice.
My copy of The Reasoned Schemer, Second Edition arrived earlier this week and, since I already went through the first edition some years ago, this time I opened it directly to Chapter 10 for the miniKanren implementation. The miniKanren language is very small, just a few hundred lines of Racket code, but the language itself is surprisningly powerfull. To test the implementation, it I decided to solve a logic puzzle, which seems to be well suited for logic programming languages.
The Puzzle
There are many variants of this logic puzzle on the Internet, the original appeared in 1962 and was called the Zebra Puzzle. Since the clues in the original puzzle involve cigarette smoking, which is no longer fashionable, I found another variant which uses sport instead of cigarettes. The puzzle goes like this (here is the source):
There are five houses in a row and in five different colors. In each house lives a person from a different country. Each person drinks a certain drink, plays a certain sport, and keeps a certain pet. No two people drink the same drink, play the same sport, or keep the same pet.
- 1 The Brit lives in a red house
- 2 The Swede keeps dogs
- 3 The Dane drinks tea
- 4 The green house is on the left of the white house
- 5 The green house owner drinks coffee
- 6 The person who plays polo rears birds
- 7 The owner of the yellow house plays hockey
- 8 The man living in the house right in the center drinks milk
- 9 The Norwegian lives in the first house
- 10 The man who plays baseball lives next to the man who keeps cats
- 11 The man who keeps horses lives next to the one who plays hockey
- 12 The man who plays billiards drinks beer
- 13 The German plays soccer
- 14 The Norwegian lives next to the blue house
Who Owns the fish?
Strictly speaking, it is not possible to answer the question and solve the puzzle: since the fish is not mentioned in any of the clues, we don’t know that there even is a fish. However, another possible interpretation is that the question itself offers an additional clue: that someone owns a fish, and this makes the puzzle solvable, so we’ll use the latter interpretation here.
Before we attempt to solve this puzzle, let’s have a brief look at the miniKanren DSL.
The Language
The miniKanren implementation is quite small and the authors of "The Reasoned Schemer" explain its inner workings in one short chapter. There are many implementations you can use, available on the miniKanren website, but the examples below are written using the language defined in the Second Edition of The Reasoned Schemer, which has some differences from the first edition.
You can find the official second edition implementation here, but for this blog post I wrote my own miniKanren implementation, which I used for solving the puzzle. Since this is my implementation, I took the liberty of renaming some operators, as I believe it makes them more readable, in particular, the book uses conde
, here I use cond/e
, the book uses membero
, here I use member/o
.
You can find my version of miniKanren in this GitHub Gist, to start using it, simply copy the racket file in a local folder and start the programs with the following lines:
1 2 |
#lang racket (require "mk.rkt") |
miniKanren is an embedded Domain Specific Language (DSL) for logic programming. The language itself is quite small, with only 4 basic elements:
- The unification operator,
==
which associates two terms, which can be variables or values - A mechanism to introduce new variables, called
fresh
, somewhat analogous tolet
in Racket, - Program control mechanism, called
cond/e
, somewhat analogous tocond
from Racket - A mechanism to define new relations,
defrel
, which are analogous todefine
in Racket.
There are some other underlying elements in the language, such as conj
for conjunction and disj
for disjunction which are useful in user programs, plus there is an interface function which allow running miniKanren programs in Racket, named run
.
Unification using ==
miniKanren works by running queries which are embedded into Racket code. Here is a simple example:
1 2 |
(run #f q (== 'hello q)) '(hello) |
In the program above, we indicate that we want the value of the variable q
and the program (== 'hello q)
simply associates the value 'hello
with q
. The result of the query is always a list, since the program can return multiple results. The #f
argument to run
is the number of answers we want to obtain, #f
means that we want all the possible answers.
For example, the program below returns two values: 'hello
and 'world
, since cond/e
specifies two alternatives:
It is important to understand that ==
means association, not assignment. The order in which these associations are made is not important. In the program below, we create a new variable x
, associate it with q
, which has no value yet, than associate x
with the value 'hello
. Since q
and x
are associated, q
will also be associated with 'hello
:
Another interesting feature of ==
is that it is able to “look into” lists. In the example below, the variable q
is associated with a list of 3 elements, the symbol 'Result
and two variables x
and y
. Later, the two variables are associated with values:
You can also group sequence of logic steps into relations using defrel
, these are analogous to functions in Racket. We will define such relations while solving the puzzle, but one important relation will be useful for our solution, and this is member/o
, which we’ll look at next.
member/o relation
The member/o
relation is the miniKanren equivalent of the Racket member?
function which checks that a value is present in a list, but there are some important differences:
(member? x l)
— returns true ifx
is present in the listl
(member/o x l)
— makes changes to bothx
andl
such thatx
is present inl
, or fail if no such changes are possible.
Below we’ll look at some examples of the most important use cases.
In the simplest case, member/o
can be used like member?
, to check if a value is resent in a list:
1 2 |
(run #f q (member/o 2 '(1 2 3))) '(_.0) |
The result of this query is a single _.0
symbol since the goal succeeded but did not associate any answer with the question q
— an alternative interpretation of this result is that the goal succeeds for any value of q.
A similar query but with a non-existent element, will return an empty list, since there are no valid values for q
that would make the goal succeed.
1 2 |
(run #f q (member/o 4 '(1 2 3))) '() |
When the first variable passed to member/o
has no associated value (i.e. it is fresh), the goal can be used to enumerate all elements in the list. The query below has three answers, one for each element in the input list. We associate the list (Result ,r)
with the query q
, so it is more obvious that the result of this query is not simply the input list (1 2 3)
. The interpretation of this query result is that the query would succeed if r
is ether 1, 2, or 3:
1 2 3 4 |
(run #f q (fresh (r) (== `(Result ,r) q) (member/o r '(1 2 3)))) '((Result 1) (Result 2) (Result 3)) |
Finally, when the second variable passed to member/o
is fresh, the relation can be used to generate all the lists which have 1 as a member. Since there is an infinite number of such lists, we specify the number of answers we want instead of specifying #f
which would attempt to find all the answers, taking an infinite amount of time.
1 2 |
(run 3 q (member/o 1 q)) '((1 . _.0) (_.0 1 . _.1) (_.0 _.1 1 . _.2)) |
Here the values _.0
, _.1
, etc, stand for “any value” and the result (1 . _0)
represents all the lists which have 1 as the first element, since the result is a cons cell and _0
can be replaced with an infinite number of lists.
There are more complex cases, when the x
and l
arguments are partially specified, but we will explore these as we solve the puzzle.
member/o
is not a miniKanren built-in, it can be implemented in just a few lines of code. For how and why this works, you will need to read the miniKanren book, but here is the entire implementation:
The Solution
With the miniKanren introduction done, let’s solve the puzzle. The idea behind the solution is that we will attempt to translate each clue into a relation and we will describe what properties the solution has, not how to build or search for the solution.
We will also add the clues one by one and we’ll check what miniKanren can do with each clue. The first bit of information that we’ll use is that “there are five houses in a row”. look.
The Street
miniKanren only supports lists as data structures, so everything will be represented as a list, but, to differentiate between different types of things that we have to work with, the first element in our list will be a symbol denoting its type — this is not necessary for miniKanren but it makes the results easier to inspect. With this in mind, we will represent the solution, which is a street of five houses, as a list of 6 elements: the symbol 'Street
followed by 5 items. Here is how we can do this in miniKanren:
Here, we create five fresh variables (i.e. variables that have no values) and construct a list out of them, then associate this list with the puzzle result. Note how we define a separate relation, called fish-puzzle
and run that. While this is not necessary at this stage, things will become easier to manage later on. Also note how the fish-puzzle
relation mixes Racket code like let
with miniKanren code like fresh
and ==
, this works because miniKanren is an embedded DSL, so the Racket code is available inside miniKanren programs.
When trying to solve the puzzle, miniKanren comes up with the best possible solution, given the clues we provided so far: that we have a street with five unknown things in it, which are denoted by the symbols _.0
through _.4
.
Clues About Houses
We’ll start with the simplest clues: these specify information about an individual house, and there are several of them.
- 1 The Brit lives in a red house
- 2 The Swede keeps dogs
- 3 The Dane drinks tea
- 5 The green house owner drinks coffee
- 6 The person who plays polo rears birds
- 7 The owner of the yellow house plays hockey
- 12 The man who plays billiards drinks beer
- 13 The German plays soccer
Implementing relations for these clues requires us to represent houses, and just as with the street, we’ll use a list, with the symbol 'House
as the first element followed by the nationality, house color, bet, beverage and sport. Here is the first clue:
1 2 3 4 5 6 7 8 9 10 |
(defrel (brit-lives-in-red-house solution) (fresh (pet beverage sport) (let ([house (list 'House 'Brit 'Red pet beverage sport)]) (member/o house solution)))) (defrel (fish-puzzle solution) (fresh (h1 h2 h3 h4 h5) (let ([street (list 'Street h1 h2 h3 h4 h5)]) (== street solution))) (brit-lives-in-red-house solution)) |
The brit-lives-in-red-house
relation constructs a house with the information we have, 'Brit
and 'Red
and fresh variables for the information we don’t have. It than asserts that such a house must be a member of the street using member/o
. We added the clue to the fish-puzzle
and if we run the program, we now get 5 results:
1 2 3 4 5 6 |
(run #f solution (fish-puzzle solution)) '((Street (House Brit Red _.0 _.1 _.2) _.3 _.4 _.5 _.6) (Street _.0 (House Brit Red _.1 _.2 _.3) _.4 _.5 _.6) (Street _.0 _.1 (House Brit Red _.2 _.3 _.4) _.5 _.6) (Street _.0 _.1 _.2 (House Brit Red _.3 _.4 _.5) _.6) (Street _.0 _.1 _.2 _.3 (House Brit Red _.4 _.5 _.6))) |
Since there are five houses in the street, and we only know the nationality and color of one of one house, there are now five possible solutions, by placing this house in every possible position.
The other clues in this section are represented using the same idea: construct a house with the information we have and asserting that it should be a member of the street.
1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 |
(defrel (swede-keeps-dogs solution) (fresh (color beverage sport) (let ([house (list 'House 'Swede color 'Dogs beverage sport)]) (member/o house solution)))) (defrel (dane-drinks-tea solution) (fresh (color pet sport) (let ([house (list 'House 'Dane color pet 'Tea sport)]) (member/o house solution)))) (defrel (green-house-owner-drinks-coffee solution) (fresh (nationality pet sport) (let ([house (list 'House nationality 'Green pet 'Coffee sport)]) (member/o house solution)))) (defrel (polo-player-rears-birds solution) (fresh (nationality color beverage) (let ([house (list 'House nationality color 'Birds beverage 'Polo)]) (member/o house solution)))) (defrel (yellow-house-owner-plays-hockey solution) (fresh (nationality pet beverage) (let ([house (list 'House nationality 'Yellow pet beverage 'Hockey)]) (member/o house solution)))) (defrel (billiad-player-drinks-beer solution) (fresh (nationality color pet) (let ([house (list 'House nationality color pet 'Beer 'Billiard)]) (member/o house solution)))) (defrel (german-plays-soccer solution) (fresh (color pet beverage) (let ([house (list 'House 'German color pet beverage 'Soccer)]) (member/o house solution)))) |
Running this puzzle produces 2280 solutions containing all possible combinations given the clues we have so far. Note how the houses now have additional information that was not directly specified in the clues, For example, one possible solution is where the Dane lives in the Yellow house, even though this was not explicitly mentioned in any of the clues. Here are the first 3 possibilities:
1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 |
(defrel (fish-puzzle solution) (fresh (h1 h2 h3 h4 h5) (let ([street (list 'Street h1 h2 h3 h4 h5)]) (== street solution))) (brit-lives-in-red-house solution) (swede-keeps-dogs solution) (dane-drinks-tea solution) (green-house-owner-drinks-coffee solution) (polo-player-rears-birds solution) (yellow-house-owner-plays-hockey solution) (billiad-player-drinks-beer solution) (german-plays-soccer solution)) (run 3 solution (fish-puzzle solution)) '((Street (House Dane Yellow _.0 Tea Hockey) (House Brit Red Birds _.1 Polo) (House Swede Green Dogs Coffee _.2) (House German _.3 _.4 _.5 Soccer) (House _.6 _.7 _.8 Beer Billiard)) (Street (House Brit Red _.0 Beer Billiard) (House German Green _.1 Coffee Soccer) (House _.2 Yellow _.3 _.4 Hockey) (House Dane _.5 Birds Tea Polo) (House Swede _.6 Dogs _.7 _.8)) (Street (House Dane Yellow _.0 Tea Hockey) (House Swede Green Dogs Coffee _.1) (House Brit Red Birds _.2 Polo) (House German _.3 _.4 _.5 Soccer) (House _.6 _.7 _.8 Beer Billiard))) |
Clues About House Locations
Two of the clues add information about where a house is placed on the street:
- 8 The man living in the house right in the center drinks milk
- 9 The Norwegian lives in the first house
Clue 8 can simply be expressed as the third house on the street has milk as the beverage:
In the relation above, we had to use conj
to group the two goals inside the Racket let
statement, conj
means that both goals must hold. While it is possible to mix Racket and miniKanren, it is not always obvious how to do so without understanding the inner workings of miniKanren. If you are familiar with the backquote/unquotes in Racket, it is simpler to write the above relation shown below. This approach avoids the pitfalls of mixing Racket and miniKanren code:
The clue that “the Norvegian lives in the first house” can be expressed the same way. There is some ambiguity in this statement, since “first house” can mean either “first from the left” or “first from the right”. We could just use one assumption, but we can also represent this ambiguity as different possibilities, expressed as the disj
statement, which means that either of the goals must hold.
To check that the previous relation works as expected, here is what the solutions look if we leave just this relation in the puzzle: there are two possibilities, one that the Norvegian is in the first house from the left and the second one that the Norvegian is in the first house from the right:
1 2 3 4 5 6 7 8 9 |
(defrel (fish-puzzle solution) (fresh (h1 h2 h3 h4 h5) (let ([street (list 'Street h1 h2 h3 h4 h5)]) (== street solution))) (norvegian-in-first-house solution)) (run #f solution (fish-puzzle solution)) '((Street (House Norvegian _.0 _.1 _.2 _.3) _.4 _.5 _.6 _.7) (Street _.0 _.1 _.2 _.3 (House Norvegian _.4 _.5 _.6 _.7))) |
Adding these two clues to the puzzle reduces the number of possibilities to 336 solutions, since there are now less possibilities to satisfy all of the clues given so far.
“To-The-Left-Of” Relationships
- 4 The green house is on the left of the white house
The fourth clue, that “the green house is on the left of the white house” represents a constraint between two houses. The “to the left of” part of the clue can be represented as a separate relation, and, since there are only 5 houses in the street, it is simpler to just handle every possibility directly:
1 2 3 4 5 6 7 8 9 |
It is important to understand that to-the-left-of/o
will generate the possible solutions given what is known about house-a
, house-b
and puzzle
, plus the additional restrictions specified by the relation itself (that house-a
is to the left of house-b
).
Here is how we can write our clue using the to-the-left-of/o
relation:
1 2 3 4 5 |
(defrel (green-house-left-of-white-house solution) (fresh (nationality1 pet1 beverage1 sport1 nationality2 pet2 beverage2 sport2) (let ([green-house (list 'House nationality1 'Green pet1 beverage1 sport1)] [white-house (list 'House nationality2 'White pet2 beverage2 sport2)]) (to-the-left-of/o green-house white-house solution)))) |
Updating the puzzle with the new relation produces 240 results, further constraining the number of possibilities.
“Next-To” relationships
The remaining clues have a “next to” relationship between the houses:
- 10 The man who plays baseball lives next to the man who keeps cats
- 11 The man who keeps horses lives next to the one who plays hockey
- 14 The Norwegian lives next to the blue house
The “next to” relationship can be expressed in terms of the to-the-left-of/o
relationship: x
is next to y
if either x
is to the left of y
or y
is to the left of x
:
1 2 3 4 |
(defrel (next-to/o x y l) (disj (to-the-left-of/o x y l) (to-the-left-of/o y x l))) |
Using this relationship we can write the final clues in miniKanren:
1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 |
(defrel (baseball-player-lives-next-to-cat-owner solution) (fresh (nationality1 color1 pet1 beverage1 nationality2 color2 beverage2 sport2) (let ([baseball-house (list 'House nationality1 color1 pet1 beverage1 'Baseball)] [cat-house (list 'House nationality2 color2 'Cats beverage2 sport2)]) (next-to/o baseball-house cat-house solution)))) (defrel (hockey-player-lives-next-to-horse-owner solution) (fresh (nationality1 color1 pet1 beverage1 nationality2 color2 beverage2 sport2) (let ([hockey-house (list 'House nationality1 color1 pet1 beverage1 'Hockey)] [horse-house (list 'House nationality2 color2 'Horses beverage2 sport2)]) (next-to/o hockey-house horse-house solution)))) (defrel (norvegian-lives-next-to-blue-house solution) (fresh (color1 pet1 beverage1 sport1 nationality2 pet2 beverage2 sport2) (let ([norvegian-house (list 'House 'Norvegian color1 pet1 beverage1 sport1)] [blue-house (list 'House nationality2 'Blue pet2 beverage2 sport2)]) (next-to/o norvegian-house blue-house solution)))) |
So, Who Owns the Fish?
Here is the puzzle with all the clues added:
1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 |
(defrel (fish-puzzle solution) (fresh (h1 h2 h3 h4 h5) (let ([street (list 'Street h1 h2 h3 h4 h5)]) (== street solution))) ;; Clues about the houses (brit-lives-in-red-house solution) (swede-keeps-dogs solution) (dane-drinks-tea solution) (green-house-owner-drinks-coffee solution) (polo-player-rears-birds solution) (yellow-house-owner-plays-hockey solution) (billiad-player-drinks-beer solution) (german-plays-soccer solution) ;; Clues about house positions on the street (center-house-owner-drinks-milk solution) (norvegian-in-first-house solution) ;; To-the-left-of clues (green-house-left-of-white-house solution) ;; Next-to clues (baseball-player-lives-next-to-cat-owner solution) (hockey-player-lives-next-to-horse-owner solution) (norvegian-lives-next-to-blue-house solution)) |
Running this program produces two solutions — the two solutions correspond to the ambiguity about what “first house” means in clue 9: The Norwegian lives in the first house. The puzzle would have only one solution if we assume that the Norwegian lives in the first house on the left.
1 2 3 4 5 6 7 8 9 10 11 12 13 |
(run #f solution (fish-puzzle solution)) '((Street (House German Green _.0 Coffee Soccer) (House Swede White Dogs Beer Billiard) (House Brit Red Birds Milk Polo) (House Dane Blue Horses Tea Baseball) (House Norvegian Yellow Cats _.1 Hockey)) (Street (House Norvegian Yellow Cats _.0 Hockey) (House Dane Blue Horses Tea Baseball) (House Brit Red Birds Milk Polo) (House German Green _.1 Coffee Soccer) (House Swede White Dogs Beer Billiard))) |
Neither solution has anything to say about a fish, since the fish does not appear anywhere in the clues. However both solutions contain some placeholder symbols, _.0
and _.1
, indicating that we don’t know what pet the German has or what beverage the Norvegian drinks. The _.0
and _.1
have no special meaning except to say that they need to be different from each other. Also, placeholder symbols are specific to one answer only: the _.0
from the first solution is not related to the _.0
from the second solution.
We can how ask the question “who owns the fish?” using the relation below. Note that this relation takes two arguments both the street and a nationality, which can be used as an output argument to determine the owner.
Running the query produces two answers, since there are two solutions, but both answers are the same: the German owns the fish, since the solution does not change even with the ambiguity of clue 9.
1 2 3 4 5 |
(run #f fish-owner (fresh (solution) (fish-puzzle solution) (who-owns-the-fish? solution fish-owner))) '(German German) |
The who-owns-the-fish?
relation not only extracts the owner of the fish, but also updates the puzzle to assign a fish to someone, adding the new knowledge that there is a fish to the solution. This is easy to see if we extract both the fish owner and the final puzzle solution, the German now has an assigned pet.
1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 |
(run #f (fish-owner solution) (fish-puzzle solution) (who-owns-the-fish? solution fish-owner)) '((German (Street (House German Green Fish Coffee Soccer) (House Swede White Dogs Beer Billiard) (House Brit Red Birds Milk Polo) (House Dane Blue Horses Tea Baseball) (House Norvegian Yellow Cats _.0 Hockey))) (German (Street (House Norvegian Yellow Cats _.0 Hockey) (House Dane Blue Horses Tea Baseball) (House Brit Red Birds Milk Polo) (House German Green Fish Coffee Soccer) (House Swede White Dogs Beer Billiard)))) |
The who-owns-the-fish?
can also be used to ask if a specific nationality owns the fish. For example, asking if the Norvegian owns the fish produces zero results, since the Norvegian does not own the fish:
1 2 3 4 5 |
(run #f q (fresh (solution) (fish-puzzle solution) (who-owns-the-fish? solution 'Norvegian))) '() |
Does the German Really Own the Fish?
The Fish does not appear in any of the clues this puzzle, so, technically, we don’t know who owns the Fish. The who-owns-the-fish?
relation shown above will add the Fish to the solution, if the goal would succeed while doing that, so this relation not only queries the solution, but also influences it.
To find out if there really is a fish, one option is to just get the solution out of miniKanren and use Racket code to search for the fish, which will be nowhere to be found. However, the the code we have written so far only involves describing the solution and leaving miniKanren to do the searching, so we’ll try to write another relation that can look for the fish without adding it if it is not already present.
The who-really-owns-this-pet?
relation works by looking at every house in the street, using project
to bind the value of the pet so Racket code can inspect it. The Racket code will check if the pet is the one we are looking for, and use the miniKanren succeed
or fail
goals depending on the test result:
Using the new relation to query the result produces an empty list, meaning the puzzle has no solution:
1 2 3 4 5 |
(run #f q (fresh (solution) (fish-puzzle solution) (who-really-owns-this-pet? solution q 'Fish))) '() |
You may have noticed that, unlike the who-owns-the-fish?
relation, the who-really-owns-this-pet?
has a third argument for the pet we are looking for. This is useful to verify that the relation is working, since it is very easy to write an incorrect miniKanren program which fails, ant it is difficult to distinguish failure because of a program bug from failure to find a result. In this case, we can verify our relation by asking who owns a pet which exists in the solution:
1 2 3 4 5 |
(run #f q (fresh (solution) (fish-puzzle solution) (who-really-owns-this-pet? solution q 'Cats))) '(Norvegian Norvegian) |
The Caveat
Relations in a logic program are interchangeable, that is, we can change the order of the relations in the fish puzzle and still obtain the same result. Unfortunately, there are some caveats in doing this, which show up when the miniKanren implementation “leaks out”. To illustrate the problem, we’ll use the simpler version of the puzzle with the only two relations being “there are 5 houses on the street” and “the Brit owns the Red house”:
Running this puzzle produces five solutions, since there are five houses on the street.
1 2 3 4 5 6 |
(run #f q (fish-puzzle1 q)) '((Street (House Brit Red _.0 _.1 _.2) _.3 _.4 _.5 _.6) (Street _.0 (House Brit Red _.1 _.2 _.3) _.4 _.5 _.6) (Street _.0 _.1 (House Brit Red _.2 _.3 _.4) _.5 _.6) (Street _.0 _.1 _.2 (House Brit Red _.3 _.4 _.5) _.6) (Street _.0 _.1 _.2 _.3 (House Brit Red _.4 _.5 _.6))) |
What happens if we change the order of the relations, asserting that the "Brit owns the Red house" than that there are 5 houses on the street:
This produces the same 5 solutions, but note that we had to ask only for 5 solutions, using (run 5 ...)
, if we as for 6 or more solutions, or for all the solutions using (run #f ...)
, the program will run forever.
1 2 3 4 5 6 |
(run 5 q (fish-puzzle2 q)) '((Street (House Brit Red _.0 _.1 _.2) _.3 _.4 _.5 _.6) (Street _.0 (House Brit Red _.1 _.2 _.3) _.4 _.5 _.6) (Street _.0 _.1 (House Brit Red _.2 _.3 _.4) _.5 _.6) (Street _.0 _.1 _.2 (House Brit Red _.3 _.4 _.5) _.6) (Street _.0 _.1 _.2 _.3 (House Brit Red _.4 _.5 _.6))) |
To understand what is happening, lets add some tracing to the relations. You can see that the first goal produces a street if 5 houses and the next goal starts filling in the solution. Since the first gaol is limited to one solution, the member/o
relation is also limited to placing the house inside a street with a limited number of houses:
1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 |
(defrel (fish-puzzle1 solution) (fresh (h1 h2 h3 h4 h5) (let ([street (list 'Street h1 h2 h3 h4 h5)]) (== street solution))) (show "after 5 houses" solution) (brit-lives-in-red-house solution) (show "after brit-lives-in-red-house" solution)) (run #f q (fish-puzzle1 q)) ;; *** after 5 houses ;; puzzle -> (Street _.0 _.1 _.2 _.3 _.4) ;; *** after brit-lives-in-red-house ;; puzzle -> (Street (House Brit Red _.0 _.1 _.2) _.3 _.4 _.5 _.6) ;; *** after brit-lives-in-red-house ;; puzzle -> (Street _.0 (House Brit Red _.1 _.2 _.3) _.4 _.5 _.6) ;; *** after brit-lives-in-red-house ;; puzzle -> (Street _.0 _.1 (House Brit Red _.2 _.3 _.4) _.5 _.6) ;; *** after brit-lives-in-red-house ;; puzzle -> (Street _.0 _.1 _.2 (House Brit Red _.3 _.4 _.5) _.6) ;; *** after brit-lives-in-red-house ;; puzzle -> (Street _.0 _.1 _.2 _.3 (House Brit Red _.4 _.5 _.6)) '((Street (House Brit Red _.0 _.1 _.2) _.3 _.4 _.5 _.6) (Street _.0 (House Brit Red _.1 _.2 _.3) _.4 _.5 _.6) (Street _.0 _.1 (House Brit Red _.2 _.3 _.4) _.5 _.6) (Street _.0 _.1 _.2 (House Brit Red _.3 _.4 _.5) _.6) (Street _.0 _.1 _.2 _.3 (House Brit Red _.4 _.5 _.6))) |
In the second version of the puzzle, the brit-lives-in-red-house
starts producing an infinite number of lists which would satisfy the relation, and the following goal rejects the first one (since the solution has to start with the symbol 'Street
), than matches the flowing 5 solutions to a street of 5 houses. However, if we were to ask for a 6th solution, brit-lives-in-red-house
will happily produce a candidate, but the next goal will fail since it cannot fit a 5 house street if there are already 6 houses or more, so it will reject this candidate, causing brit-lives-in-red-house
to produce the next candidate which is an even longer list, which will be rejected again, causing an infinite loop. You can try that out yourself by running the program with the added tracing and asking for 6 solutions:
1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 |
(defrel (fish-puzzle2 solution) (brit-lives-in-red-house solution) (show "after brit-lives-in-red-house" solution) (fresh (h1 h2 h3 h4 h5) (let ([street (list 'Street h1 h2 h3 h4 h5)]) (== street solution))) (show "after 5 houses" solution)) (run 5 q (fish-puzzle2 q)) ;; *** after brit-lives-in-red-house ;; puzzle -> ((House Brit Red _.0 _.1 _.2) . _.3) ;; *** after brit-lives-in-red-house ;; puzzle -> (_.0 (House Brit Red _.1 _.2 _.3) . _.4) ;; *** after 5 houses ;; puzzle -> (Street (House Brit Red _.0 _.1 _.2) _.3 _.4 _.5 _.6) ;; *** after brit-lives-in-red-house ;; puzzle -> (_.0 _.1 (House Brit Red _.2 _.3 _.4) . _.5) ;; *** after 5 houses ;; puzzle -> (Street _.0 (House Brit Red _.1 _.2 _.3) _.4 _.5 _.6) ;; *** after brit-lives-in-red-house ;; puzzle -> (_.0 _.1 _.2 (House Brit Red _.3 _.4 _.5) . _.6) ;; *** after 5 houses ;; puzzle -> (Street _.0 _.1 (House Brit Red _.2 _.3 _.4) _.5 _.6) ;; *** after brit-lives-in-red-house ;; puzzle -> (_.0 _.1 _.2 _.3 (House Brit Red _.4 _.5 _.6) . _.7) ;; *** after 5 houses ;; puzzle -> (Street _.0 _.1 _.2 (House Brit Red _.3 _.4 _.5) _.6) ;; *** after brit-lives-in-red-house ;; puzzle -> (_.0 _.1 _.2 _.3 _.4 (House Brit Red _.5 _.6 _.7) . _.8) ;; *** after 5 houses ;; puzzle -> (Street _.0 _.1 _.2 _.3 (House Brit Red _.4 _.5 _.6)) '((Street (House Brit Red _.0 _.1 _.2) _.3 _.4 _.5 _.6) (Street _.0 (House Brit Red _.1 _.2 _.3) _.4 _.5 _.6) (Street _.0 _.1 (House Brit Red _.2 _.3 _.4) _.5 _.6) (Street _.0 _.1 _.2 (House Brit Red _.3 _.4 _.5) _.6) (Street _.0 _.1 _.2 _.3 (House Brit Red _.4 _.5 _.6))) |
Final Thoughts
The miniKanren web site at miniKanren.org has a lot of resources on logic programming, including published papers on various extentions plus videos of talks. Some of the papers provide really interesting extensions to the miniKanren languages and are worth exploring — but not in this blog post…