Clojure. Logical difference with mind Schemer

Question

I worked through The Reasoned Schemer (TRS) using Clojure.logic and paying attention to the differences described here . I reached frame 24 of chapter 3, where TRS reports that

(run 5 [x] (lolo '((ab) (cd) . 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 la) (listo a)) (fresh [d] (resto ld) (lolo d))) (s# u#))) 

which gives the following strange results:

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

which basically means that my lolo produces solutions that crowd out fresh variables. If I continue trying to see the pattern, I get

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

but I cannot see clearly enough through the fog and would appreciate any light on that. Is this a mistake in my lolo? Is this a bug in Clojure.logic? Is this a reasonable difference between a solver in TRS and a solver in Clojure.logic? How can I interpret or use the results? How can I mentally predict the results of Clojure.logic?

Answer 1

As mentioned on the main wiki page you link to, core.logic conde is TRS condi . The difference is that TRS conde tries to arrange the order, and condi interleaves the resulting streams. Thus, the core.logic version will display all the results displayed in TRS, but in between, it will return other results that miniKanren never gets around.

One important pattern in your longer answer is that if you take every second result starting with (()) , this subsequence of the seq result looks like the whole seq result with () added to each individual result. This is due to the alternation - in this subsequence () is selected as the first element of the result, then lolo recursively returns the rest.