[plt-scheme] miniKanren: translation from Prolog

From: Marek Kubica (marek at xivilization.net)
Date: Thu May 27 12:06:18 EDT 2010

Hi Lindsey,

Thank you for your help.

On Wed, 26 May 2010 21:43:13 -0400
Lindsey Kuper <lkuper at cs.indiana.edu> wrote:

> I'm not sure that do-insert is conso.  Is this the behavior you want?
> 
> > (run* (q) (do-insert 'a '(f g h i) q))
> ((a f g h i))
> 
> Or is this?
> 
> > (run* (q) (do-insert 'a '(f g h i) q))
> ((a f g h i)
>   (f a g h i)
>   (f g a h i)
>   (f g h a i)
>   (f g h i a))

You're right. I was tricked by my Prolog implementation thinking that
(a f g h i) was the only answer.

> Note that here I'm using "exist", which is what miniKanren uses these
> days instead of "fresh".  You can find a relatively recent version of
> miniKanren at
> http://www.cs.indiana.edu/cgi-pub/lkuper/c311/resources#minikanren-resources .

Ok, I upgraded my miniKanren to that version.

> As for the permute relation: there are some interesting things going
> on here.  You're correct to use caro and cdro instead of car and cdr.
> The "else", however, is unnecessary since every clause of a conde is
> tried regardless of order.  The let bindings shouldn't be necessary,
> either, once you're using caro and cdro.  Again using the original
> Prolog as a guide, I'd do it this way:

The else was from The Reasoned Schemer, they seem to use a version of
conde which is more similar to cond.

> (define permute
>   (lambda (l1 l2)
>     (conde
>       [(exist (x)
>          (conso x '() l1)
>          (conso x '() l2))]
>       [(exist (x y z1)
>          (conso x y l1)
>          (=/= y '())
>          (permute y z1)
>          (do-insert x z1 l2))])))

Ok, I slowly start to see the pattern how to translate Prolog code into
miniKanren.

> Here I'm using a disequality constraint, (=/= y '()), to ensure that
> the two conde clauses don't overlap.  However, this version of permute
> is still problematic.  Running forwards works fine...

Good to know, first I thought that Prolog's =/= is == in miniKanren.

> So, we're damned if we do and damned if we don't.  My understanding is
> that the divergence here comes from the fact that both permute and
> do-insert are recursive.  Usually, in miniKanren programs, not putting
> a recursive goal last is asking for trouble.  Since one of them has to
> come not-last, it's difficult to avoid divergence.  Having said that,
> perhaps someone else will chime in with a better answer.

Hmm, maybe I should come up with a version of permute that does not
need do-insert... Tricky, since I am quite new to logic programming.

I'd be happy if anyone could find a working solution before I do,
though ;)

regards,
Marek


Posted on the users mailing list.