A Taste of cKanren (via a coding challenge)

[David Nolen]

Larent Petit pointed out this fun challenge: http://beust.com/weblog/2011/10/30/a-new-coding-challenge/

To get a sense of how cool cKanren and constraint logic programming is I recommend reading my post about solving it using cKanren http://dosync.posterous.com/a-taste-of-ckanren.

This is what William Byrd and Dan Friedman will be presenting at the Conj and I'm looking forward to getting their work into core.logic.

David

[Brent Millare]

Looks really cool. Can't wait to see the talk.

[David Nolen]

Heh, as someone pointed out this doesn't actually solve the puzzle since I'm not considering putting stones on either side of the scale. Still I think the idea of what cKanren can do is communicated :)

On Sun, Oct 30, 2011 at 8:34 PM, Brent Millare <brent....@gmail.com> wrote:

Looks really cool. Can't wait to see the talk.

--
You received this message because you are subscribed to the Google
Groups "Clojure" group.
To post to this group, send email to clo...@googlegroups.com
Note that posts from new members are moderated - please be patient with your first post.
To unsubscribe from this group, send email to
clojure+u...@googlegroups.com
For more options, visit this group at
http://groups.google.com/group/clojure?hl=en

[Ambrose Bonnaire-Sergeant]

Wow!

Shows off the advantages of embedding in a language like Scheme too.

I'm planning to join you in the implementation in core.logic after November. Keep me (us) posted :)

Would CLP be more useful for a predicate dispatch implementation than what core.logic provides currently?

Ambrose

--

[David Nolen]

Here's a correct version that solves the puzzle in ~12ms, https://gist.github.com/1329580. A bit longer but it fun to combine constraints w/ search.

Will try to find some time to write a more detailed explanation.

[David Nolen]

A blog post explaining the solution step by step http://dosync.posterous.com/another-taste-of-ckanren.

[Jules]

Here is a Python version (http://pastebin.com/reW5eaCy):

def valid(a,b,c,d):
return set(w*a + x*b + y*c + z*d
for w in [-1,0,1]
for x in [-1,0,1]
for y in [-1,0,1]
for z in [-1,0,1]) > set(range(1,41))

ws = [(a,b,c,d) for a in range(1,41-1-1-1)
for b in range(a,41-a-1-1)
for c in range(b,41-a-b-1)
for d in range(c,41-a-b-c)
if valid(a,b,c,d)]

I wonder if you can make the cKanren version just as declarative as
this one (cKanren's purpose being declarative).

Jules

On 1 nov, 04:48, David Nolen <dnolen.li...@gmail.com> wrote:
> A blog post explaining the solution step by stephttp://dosync.posterous.com/another-taste-of-ckanren.

>
>
>
>
>
>
>
> On Mon, Oct 31, 2011 at 9:36 PM, David Nolen <dnolen.li...@gmail.com> wrote:
> > Here's a correct version that solves the puzzle in ~12ms,
> >https://gist.github.com/1329580. A bit longer but it fun to combine
> > constraints w/ search.
>
> > Will try to find some time to write a more detailed explanation.
>

> > On Sun, Oct 30, 2011 at 9:00 PM, David Nolen <dnolen.li...@gmail.com>wrote:
>
> >> Heh, as someone pointed out this doesn't actually solve the puzzle since
> >> I'm not considering putting stones on either side of the scale. Still I
> >> think the idea of what cKanren can do is communicated :)
>

[Timothy Baldridge]

>I wonder if you can make the cKanren version just as declarative as
>this one (cKanren's purpose being declarative).

I don't think the Python version could be considered declarative. One
of the concepts behind logic
programming (and to some extent declarative programming) is that you
can simply provide the
system with facts, and then the system (as a black box)
decides on the correct way to perform the operation. This Python
example is really
nothing more than syntactic sugar around a imperative brute force
approach to the problem.

Timothy

[Jules]

In the same way the cKanren version is syntactic sugar around
imperative code. Declarative is not a property of a language, it's a
property of code that says how close to a mathematical specification
the code is. My Python code is much more declarative than the given
cKanren code in that regard. Just compare: http://dosync.posterous.com/another-taste-of-ckanren

On 11 nov, 23:47, Timothy Baldridge <tbaldri...@gmail.com> wrote:
> >I wonder if you can make thecKanrenversion just as declarative as
> >this one (cKanren'spurpose being declarative).

[Timothy Baldridge]

> My Python code is much more declarative than the given
> cKanren code in that regard. Just compare: http://dosync.posterous.com/another-taste-of-ckanren

I don't think you understand what declarative programming is at its
core. Declarative programming

To borrow from the ever-present wikipedia:
"declarative programming is a programming paradigm that expresses the
logic of a computation without describing its control flow.[1] Many
languages applying this style attempt to minimize or eliminate side
effects by describing what the program should accomplish, rather than
describing how to go about accomplishing it.[2] This is in contrast
with imperative programming, which requires an explicitly provided
algorithm." (see: Declarative Programming)

This is where the cKanren code succeeds where the Python code fails.
The Python code is all algorithm, and no facts. While the cKanren code
is a direct implementation of the facts about the problem: one stone
must be 1lb all stones should equal 40lb, etc. The cKanren code leaves
the interpretation of these facts up to the logic engine, while the
Python code sets strict guidelines that the compiler must follow. If,
for instance, it was faster for a given computer to count down from
instead of counting up, the Python code would run much slower, by
defining the algorithm (by using range, and for loops), you're
restricting the interpreter to your view of how to solve the problem.
The cKanren compiler/interpreter/whatever is free to solve the problem
in any way it pleases, as long as the requirements (facts) are met.
The original problem states "find 4 numbers that equal 40 but a
combination of any of which can be 1 through 40" it says nothing of
range sequences, for loops, etc.

Timothy

[Jules]

Are we reading the same cKanren code? I'll give you that the matches
definition is declarative, but then read checko and subchecko. They
are all about (recursive) control flow. Where does the specification
say anything remotely close to the checko and subchecko relations? In
contrast to this, the Python set comprehensions have minimal control
flow. Yeah, the standard Python implementation has a certain order of
executing the comprehensions, but so does the cKanren implementation
when executing the predicates. My Python program doesn't depend on
this order: it just uses declarative descriptions of sets as set
comprehensions.

Just being written in cKanren doesn't make a program declarative. If
you write a C interpreter in cKanren and then write your actual
program in a literal string, that doesn't magically make the program
declarative even though it is a cKanren program. Similarly, checko and
subchecko don't describe the problem in a declarative way. Compare
this with the Python valid() function: the set of possible weights you
can make has to be a superset of {1..40}. Again, declarativeness is a
property of programs, not languages. Some languages make writing
declarative programs easier, of course. cKanren is supposed to be such
a language, so it would be neat to see a more declarative cKanren
program for this problem.

Also, I don't see how "one stone should weigh 1lbs" is part of the
specification. Now, it is true that the answer happens to have one
stone equal to 1, but how is that part of or trivially follows from
the specification? We might as well hard-code the whole solution.

Jules

[Jules]

Here is a new program. Perhaps you would consider this declarative:

def valid(a,b,c,d):
weights = set(w*a+x*b+y*c+z*d for (w,x,y,z) in
product([-1,0,1],repeat=4))
return weights >= set(range(1,41))

ws = [(a,b,c,d) for (a,b,c,d) in product(range(1,41),repeat=4)
if a <= b <= c <= d and a+b+c+d == 40 and
valid(a,b,c,d)]

[David Nolen]

Can you reorder your statements without changing the meaning of your program? For example you cannot move the placement of the "return" expression.

David

[David Nolen]

(define (matches n)

  (run #f (q)

    (fresh (a b c d s1 s2)

       (== q `(,a ,b ,c ,d))

       (domfd a b c d s1 s2 (range 1 n)) 

       (all-differentfd `(,a ,b ,c ,d))

       (== a 1)

       (<=fd a b) (<=fd b c) (<=fd c d)

       (plusfd a b s1) (plusfd s1 c s2) (plusfd s2 d n)

       (checko `(,a ,b ,c ,d) () () n))))

Note that the "return" expression here has been moved to the top. It does not change the meaning of the program.

In cKanren you do have to be a little bit careful with recursive goals, but the freedom to rearrange expressions is much greater than in Python.

In declarative programs, the order of expressions should not influence the result.

David

On Fri, Nov 11, 2011 at 8:09 PM, Jules <jules...@gmail.com> wrote:

[Ambrose Bonnaire-Sergeant]

I assume the cKanren version can run backwards with a little tweak?

[David Nolen]

Excellent point Ambrose ;) And here it is:

(define (subchecko w sl r o n)

  (conde

   ((== sl ())

    (fresh (a d)

           (domfd a (range 1 100))

           (conde

            ((conso a d r) (plusfd a 1 w)

             (conso w r o))              

            ((== r '()) (conso w r o)))))

   ((fresh (a b c ro0 ro1 nw nsl)

           (domfd a b c (range 1 100))           

           (conso a nsl sl)

           (plusfd a b w) (plusfd a w c)

           (subchecko b nsl r ro0 n)

           (subchecko w nsl ro0 ro1 n)

           (subchecko c nsl ro1 o n)))))

(define (checko ws sl r n)

  (conde

   ((== ws '())

    (fresh (a) (caro r a) (== a n)))

   ((fresh (w wr nsl nr)

           (conso w wr ws)

           (subchecko w sl r nr n)

           (conso w sl nsl)

           (checko wr nsl nr n)))))

(define (matches a b c d n)

  (fresh (s1 s2)

         (domfd a b c d n s1 s2 (range 1 100)) 

         (all-differentfd `(,a ,b ,c ,d))

         (<fd a b) (<fd b c) (<fd c d)

         (== a 1)

         (plusfd a b s1) (plusfd s1 c s2) (plusfd s2 d n)

         (checko `(,a ,b ,c ,d) () () n)))

(run* (q)

  (matches 1 3 9 27 q)) ;; (40)

(run* (q)

   (fresh (a b c d)

     (== q `(,a ,b ,c ,d))

     (matches a b c d 40))) ;; ((1 3 9 27))

On Sat, Nov 12, 2011 at 12:31 AM, Ambrose Bonnaire-Sergeant <abonnair...@gmail.com> wrote:

I assume the cKanren version can run backwards with a little tweak?

--

[David Nolen]

Also note that even given all this generality over the Python code - the earlier Python implementation takes ~300ms and this implementation takes >900ms on my machine. 

Quite a bit slower than ~12ms. Inferring 40 takes even less time of course - ~8ms.

But really the execution time is just icing on the declarative cake ;)

David

On Fri, Nov 11, 2011 at 8:09 PM, Jules <jules...@gmail.com> wrote:

[Jules]

The time difference is largely due to using the product library
function instead of for comprehensions and the fact that the cKanren
version cheats by hardcoding part of the solution, and hardcoding an
extra constraint alldiff(a,b,c,d). The following code takes ~12ms with
PyPy on my computer:

def valid(a,b,c,d):
weights = set(w*a+x*b+y*c+z*d for w in [-1,0,1]

for x in [-1,0,1]
for y in [-1,0,1]
for z in [-1,0,1])

return weights >= set(range(1,41))


ws = [(a,b,c,d) for a in range(1,40)
for b in range(1,40) if a <= b
for c in range(1,40) if b <= c
for d in range(1,40) if c <= d
if a+b+c+d == 40 and valid(a,b,c,d)]

If you cheat with `for a in [1]` instead of `for a in range(1,40)` and
changing the <= to < (the same cheat as the alldiff), then the
execution time drops to 2ms.

Since we don't seem to be going to agree on the definition of
declarative, lets use another word: nice. Lets define niceness as
understandability and closeness to mathematical specification. I agree
that the matches definition is already nice: it handles the
constraints and symmetry breaking nicely (better than the Python
version if you ignore syntactic issues e.g. a+b+c+d=40 is more
convoluted). But the checko and subchecko leave a lot to be desired.
So my question is: can the cKanren version be improved so that it also
becomes nice?

Jules

[David Nolen]

Write a version in Python that can infer 40 from the inputs then maybe we can talk about declarative. I have no idea what you mean by "cheating" and even less of an idea what you mean by "nice."

[Ambrose Bonnaire-Sergeant]

"Understandability" is subjective. The meaning of the cKanren really jumps out at me, the python program takes a lot more for me to think through.

There is nothing wrong with pruning the search space in this program. As you said, doing so reduced the Python program execution time to 2ms!

Ambrose

[Ambrose Bonnaire-Sergeant]

I'll just clarify, the "matches" function body jumps out at me. "checko" doesn't, but it's role in the problem is still clear, even if its implementation is not. I think that's still an important trait.

Can checko be improved? I'm not sure. What does subchecko do, David?

Ambrose

[David Nolen]

checko and subchecko work together to determine whether an ordered set of weights can produce integers 1 to 40 in reverse. It's more verbose since we are preserving the ability to run our program backwards - which is simply a byproduct of writing a purely relational program.

I'm curious if it can be written more concisely. Not sure. I note that most good solutions in Python and Haskell while fast and neat can only work in one direction.

I would love to see purely relational versions in Haskell, Python etc. even if they involve bringing in a constraint solver (which alone isn't enough as far as I know)

[Jules]

Here is a slight modification of the previous program that can be
executed in two directions:

N = [40]
A = range(1,40)
B = range(1,40)
C = range(1,40)
D = range(1,40)

def valid(a,b,c,d,n):

weights = set(w*a+x*b+y*c+z*d for w in [-1,0,1]
for x in [-1,0,1]
for y in [-1,0,1]
for z in [-1,0,1])

return weights >= set(range(1,n+1))

ws = [(a,b,c,d,n) for n in N
for a in A
for b in B if a <= b
for c in C if b <= c
for d in D if c <= d
if a+b+c+d == n and valid(a,b,c,d,n)]

Change the variable domains to execute it in the other direction:

N = range(1,100)
A = [1]
B = [3]
C = [9]
D = [27]

This produces the single answer (1,3,9,27,40), i.e. the only solution
is with n = 40.

What I mean by cheating is that you hard-code part of the solution.
Would you consider the program `print "1,3,9,27"` a good solution? To
me at least, it's non obvious that the solution would have to have a=1
and would have to have a,b,c,d all different. Sure, for the way you
interpreted the problem originally, a=1 is obvious. But since now you
can subtract weights as well as adding them it is not obvious (to me).
Why couldn't a=3 and b=4 work? Then you can still weigh 1lbs. If you
consider it obvious, can you explain?

> I'm curious if it can be written more concisely. Not sure. I note that most
good solutions in Python and Haskell while fast and neat can only work
in
one direction.

I think that you can use the same technique as the Python program.
What are the weights we can measure with stones that weigh a,b,c,d?
Well, for each stone we can either put it on the left scale (-a) or on
the right scale (+a) or not on the scale at all (0). So the weights we
can measure is the set {w*a + x*b + y*c + z*d | w,x,y,z are -1, 0 or
1}. So for example if w=-1, x=0, y=1, z=1 then stone A is on the left,
stone B is not on the scale and stones C and D are on the right. The
condition we need to satisfy is that this set contains all the weights
{1..40}. With list/set comprehensions you can use this method
directly, but with logic programming you need to do it slightly
differently.

You can define a relation (canmake a b c d x) which checks if a,b,c,d
can make the weight x by creating four new finite domain variables
w,x,y,z each with domain {-1,0,1}. Then you assert w*a+x*b+y*c+z*d ==
x. So now you have a relation that succeeds iff weights a b c d can
make x. Then you just have to assert every (canmake a b c d 1) ...
(canmake a b c d 40). I don't know if cKanren has a library predicate
for that, but something like (forall xs p) that asserts p on all
elements of xs isn't hard to define.

Whether the resulting program is more concise I don't know, but I
think it would at least be easier to understand.

Jules

On Nov 13, 5:17 am, David Nolen <dnolen.li...@gmail.com> wrote:
> checko and subchecko work together to determine whether an ordered set of
> weights can produce integers 1 to 40 in reverse. It's more verbose since we
> are preserving the ability to run our program backwards - which is simply a
> byproduct of writing a purely relational program.
>
> I'm curious if it can be written more concisely. Not sure. I note that most
> good solutions in Python and Haskell while fast and neat can only work in
> one direction.
>
> I would love to see purely relational versions in Haskell, Python etc. even
> if they involve bringing in a constraint solver (which alone isn't enough
> as far as I know)
>

> On Saturday, November 12, 2011, Ambrose Bonnaire-Sergeant <abonnaireserge...@gmail.com> wrote:
> > I'll just clarify, the "matches" function body jumps out at me. "checko"
>
> doesn't, but it's role in the problem is still clear, even if its
> implementation is not. I think that's still an important trait.> Can checko be improved? I'm not sure. What does subchecko do, David?
> > Ambrose
>
> > On Sun, Nov 13, 2011 at 11:37 AM, Ambrose Bonnaire-Sergeant <
> abonnaireserge...@gmail.com> wrote:
>
> > "Understandability" is subjective. The meaning of the cKanren really
>
> jumps out at me, the python program takes a lot more for me to think
> through.> There is nothing wrong with pruning the search space in this program. As
>
> you said, doing so reduced the Python program execution time to 2ms!
>
>
>
>
>
>
>
> > Ambrose
>

[Laurent PETIT]

So, if one stays in the imperative world, why not just the generic problem instead of the specific one ?

This clojure solution can solve the problem for any N (total weight) and any M (any number of parts the stone can be spit into):

https://gist.github.com/1332020

The implementation is a bit longer than I expected, but I wanted to not cheat by hard-wiring mathematical assumptions inside it (thus the intermediate definition for a diff function working on unordered lists of elements to be considered as "bags" - where the same element could appear twice-)

2011/11/13 Jules <jules...@gmail.com>

[David Nolen]

That's very nice! But of you're not providing any sort of generic interface to do declarative programming, which is the whole point of cKanren. Also since you're expressing your constraints with for comprehensions you need to order them correctly, and so on.

What I mean by cheating is that you hard-code part of the solution.
Would you consider the program `print "1,3,9,27"` a good solution? To
me at least, it's non obvious that the solution would have to have a=1
and would have to have a,b,c,d all different. Sure, for the way you
interpreted the problem originally, a=1 is obvious. But since now you
can subtract weights as well as adding them it is not obvious (to me).
Why couldn't a=3 and b=4 work? Then you can still weigh 1lbs. If you
consider it obvious, can you explain?

My line of reasoning

- let's assume we weigh 1 with two stones, neither of which are 1. Imagine we can weigh 40. It's impossible to weigh 39.

- having two stones of the same weight is useless

- we might as well order them by weight to remove useless permutations

David