[plt-scheme] miniKanren: translation from Prolog

Marek Kubica <marek at xivilization.net> wrote:
> I am trying to translate the n-queen problem solution from here:
> <http://okmij.org/ftp/Prolog/QueensProblem.prl> into miniKanren.

> Currently, though, I am struggling with the definition of permute.
>
> The original source code looks like this:
>
> do_insert(X,Y,[X|Y]).
> do_insert(X,[Y1|Y2],[Y1|Z]) :- do_insert(X,Y2,Z).
>
> permute([X],[X]).
> permute([X|Y],Z) :- permute(Y,Z1), do_insert(X,Z1,Z).
>
> Which I translated into
>
> (define do-insert conso)

Hi Marek,

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))

Assuming you want the second, I'd do something like the following:

(define do-insert
  (lambda (x y out)
    (conde
      [(conso x y out)]
      [(exist (y1 y2 z)
         (conso y1 y2 y)
         (conso y1 z out)
         (do-insert x y2 z))])))

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
.

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:

(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))])))

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...

> (run* (q) (permute '(a b c) q))
((a b c) (b a c) (a c b) (b c a) (c a b) (c b a))

...but running backwards diverges:

> (run* (q) (permute q '(a b c))) ;; infinite loop!

But if we swap the order of the (permute y z1) and (do-insert x z1 l2)
goals to try to avoid the divergence, we get just the opposite:

> (run* (q) (permute q '(a b c)))
((a b c) (a c b) (b a c) (c a b) (b c a) (c b a))

> (run* (q) (permute '(a b c) q)) ;; infinite loop!

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.

Best,
Lindsey