Clojure.logic difference with The Reasoned Schemer

I've been working through The Reasoned Schemer (TRS) using Clojure.logic and paying attention to the differences documented here. I reached frame 24 of Chapter 3, where TRS reports that

(run 5 [x]
  (lolo '((a b) (c d) . x)))

should produce

'(()
  (())
  (() ())
  (() () ())
  (() () () ())

Now, I implemented `lolo as

(defn lolo
  "Succeeds if l is a list-of-lists."
  [l]
  (conde
   ((emptyo l) s#)
   ((fresh [a]
           (firsto l a)
           (listo a)) (fresh [d]
                             (resto l d)
                             (lolo d)))
   (s# u#)))

which produces the following strange results:

'(()
  (())
  ((_0))
  (() ())
  ((_0 _1)))

which basically means that my lolo is producing solutions that are leaking out fresh variables. If I keep going, trying to see a pattern, I get

'(()
  (())
  ((_0))
  (() ())
  ((_0 _1))
  (() (_0)
  ((_0) ())
  (() () ())
  ((_0 _1 _2)))

but I can't quite see clearly enough through the fog, and would appreciate any light shed on this. Is it a bug in my lolo? Is it a bug in clojure.logic? Is it a reasonable difference between the solver in TRS and the solver in clojure.logic? How can I interpret or use the results? How can I mentally predict the results of clojure.logic?

As mentioned on the core.logic wiki page you link to, core.logic's conde is TRS's condi. The difference is that TRS's conde tries the clauses in order, while condi interleaves the result streams. So the core.logic version will produce all the results displayed in TRS, but in between them it'll return other results which miniKanren never gets around to.

One relevant pattern in your longer answer is that if you take every second result starting from (()), that subsequence of the result seq looks like the entire result seq with () prepended to each individual result. That's due to interleaving -- on this subsequence, () is chosen as the first element of the result, then lolo recursively produces the rest.

Recommended topics

Hot tags