[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