Hi Tassilo, > I've simplified the code a bit so that I don't need the `cconso` > relation.
That's great. It's easier to understand this way. To simplify a tiny bit more, the `nf` lvar can also be removed: it's unified with `f`, so f can be used instead of nf in `(conso nf nr nl)` > Ok, and now the backwards case: > ... > ... > Well, that loops forever. I found the cause of non-termination. Before the long explanation, you might want to open my full working version from https://gist.github.com/nberger/6b0ad2a68c52a6005c6a When `l` is not ground (the backwards case), there's no constraint that prevents it from being any arbitrary long list, so isorto and inserto are indefinitely tried recursively looking for solutions based on those lists. Arbitrary long `l`s generate arbitrary long `acc`s. I tried avoiding this issue by adding a `(permuteo l sl)` in the 2-arity version of isorto, which one would say it's a relation that must hold between l and sl, but it yielded a similar result. I finally made it work by adding a (non-relational) goal that fails when acc is going to be longer than sl: (project [sl acc] (if (and (not (lvar? sl)) (= (count acc) (count sl))) fail ; acc is already long as sl, let's stop here s#)) We have to first check that sl is ground (not an lvar) so we can take its count. > But why the heck are x and nl always _0? To my best understanding, that > means that x and nl are unified, no? Yes, I understand they are unified, but I'm not sure why. > > Too bad that lazy sequences aren't printed in a readable way. I used this slightly different version of trace-lvar which calls pr-str to help with this: (defn trace-lvar [a lvar] `(println (format "%5s = %s" (str '~lvar) (pr-str (-reify ~a ~lvar))))) A 3-arity version of trace-lvar that takes a transformation fn to apply to the reified value might be handy. > And why are the sorted lists sl of isorto and nl of inserto always (the > same?) > fresh variable _0? I had expected that during the recursion, more > information should be added so that their value builds up like > > sl = (1 2 . some-lvar) > > where some-lvar will eventually during the next recursion be fixed to > the list (3). In the forward case, sl has to always be the same fresh variable because it's our "output" lvar that will get unified with acc when l gets to be empty. That also explains that in the end, nl and sl are unified to the same var. See this: (inserto f acc nacc) ; nacc will be nl in inserto (isorto r nacc sl) ; nacc will be acc in isorto, and it will be unified with sl Before closing, a minor thing: - I had to replace the conda in inserto with conde, because when l is not ground (so x is also not ground) we want to try both branches. That's what I found. Hope it helps :) - Nicolas -- You received this message because you are subscribed to the Google Groups "Clojure" group. To post to this group, send email to clojure@googlegroups.com Note that posts from new members are moderated - please be patient with your first post. To unsubscribe from this group, send email to clojure+unsubscr...@googlegroups.com For more options, visit this group at http://groups.google.com/group/clojure?hl=en --- You received this message because you are subscribed to the Google Groups "Clojure" group. To unsubscribe from this group and stop receiving emails from it, send an email to clojure+unsubscr...@googlegroups.com. For more options, visit https://groups.google.com/d/optout.
